pthariensflame

{-# OPTIONS --cubical-compatible --safe --postfix-projections #-}
module Fumula where
open import Level renaming (suc to ℓsuc; zero to ℓzero)
open import Function using (id)
open import Data.Product
open import Algebra
open import Algebra.Morphism
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
import Algebra.Properties.Ring as RingProperties

asahilina

AGX coherency, caching, and TLBs

These are just some notes on my current understanding of the subtleties of the AGX memory model and the TLB/caching issues I'm seeing.

Hypervisor shenanigans

TLBI instructions do not broadcast to the GPU from EL1 with stage 2 translation enabled. That's it. That's what the bug was.

GPU side

Gabriella439

As I come out as trans to people, most are supportive, but a few people remain skeptical and question my feelings and experiences. I try to field their concerns to the best of my ability, but one particular concern they raise is so common and so far off the mark that I feel compelled to share my thoughts on this. My intention is not to shame them, but rather to use this as an opportunity to share my own experiences.

Their concern typically goes like this: they believe that many people who transition do so because they are too easily suggestible and that they have been over-exposed to trans role models (either friends or people on social media).

Gabriella439

I'm writing this post to publicly come out as trans (specifically: I wish to transition to become a woman).

This post won't be as polished or edited as my usual posts, because that's kind of the point: I'm tired of having to edit myself to make myself acceptable to others.

I'm a bit scared to let people know that I'm trans, especially because I'm not yet in a position where I can transition (for reasons I don't want to share, at least not in public) and it's really shameful. However, I'm getting really

erincandescent

Foreward

This document was originally written several years ago. At the time I was working as an execution core verification engineer at Arm. The following points are coloured heavily by working in and around the execution cores of various processors. Apply a pinch of salt; points contain varying degrees of opinion.

It is still my opinion that RISC-V could be much better designed; though I will also say that if I was building a 32 or 64-bit CPU today I'd likely implement the architecture to benefit from the existing tooling.

Mostly based upon the RISC-V ISA spec v2.0. Some updates have been made for v2.2

Original Foreword: Some Opinion

The RISC-V ISA has pursued minimalism to a fault. There is a large emphasis on minimizing instruction count, normalizing encoding, etc. This pursuit of minimalism has resulted in false orthogonalities (such as reusing the same instruction for branches, calls and returns) and a requirement for superfluous instructions which impacts code density both in terms of size and

pthariensflame

impl Trait is Always Existential

Recently, Rust 1.26 was released, and with it came stable access to a heavily desired feature: impl Trait. For those unfamiliar, impl Trait lets you write something like this:

fn foo<'a, A, B>(x: &'a mut A) -> impl Bar<'a, B> { ... }

and have it be translated to something like this:

cartazio

directions to do a release quality build of GHC == 8.0.* with the Make based build system with all the docs

context: this is a draft for planned edits / cleanups to the current mac build directions

getting setup

1. have apple command line tools installed, as well as mactex, and your favorite OS X package manager (which for the rest of these directions we assume is brew)

2. since we assume we're using brew, install it!

mmhelloworld

{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE JavaScriptFFI #-}
{-# LANGUAGE UnliftedFFITypes #-}
{-# LANGUAGE GHCForeignImportPrim #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TypeFamilies #-}

georg

IT'S SHOWTIME

HEY CHRISTMAS TREE isLessThan100
YOU SET US UP @NO PROBLEMO
HEY CHRISTMAS TREE n
YOU SET US UP 0
HEY CHRISTMAS TREE multiple
YOU SET US UP @NO PROBLEMO

STICK AROUND isLessThan100

pthariensflame

module Lens where
open import Level
open import Function
open import Relation.Binary
open import Data.Product
open import Relation.Binary.Product.Pointwise
open import Data.Sum
open import Relation.Binary.Sum
open import Data.Empty
open import Function.Inverse