Viewing profile — cwzwarich

`std::accumulate` is defined to have sequential semantics, so the analysis required to make it parallel is probably not that different than starting from the loop version. I guess …

https://github.com/coreboot/coreboot/blob/main/src/soc/intel...

Nvidia doesn't share dies between their high-end datacenter products like B200 and consumer products. The high-end consumer dies have many more SMs than a corresponding datacenter …

Isn’t the 9000 TFLOP/s number Nvidia’s relatively useless sparse FLOP count that is 2x the actual dense FLOP count?

Adding axioms to simple type theory is more awkward than adding them to a set theory like ZFC. One approach to universes I’ve seen in Isabelle/HOL world is to postulate the existen…

The bigger problem with HOL (or simple type theory) is not the lack of dependencies, but rather the lack of logical strength. Simple type theory is equivalent in logical strength t…

The original purpose of the C standard was to solve the problems created by the diversity of increasingly divergent implementations of C. They studied existing behavior across syst…

The Rust specification you link is performative and only intended to satisfy requirements of certification processes. No one is actually using it to implement the language, as far …

My reasons for leaving Apple had nothing to do with this decision. I was already no longer working on Rosetta 2 in a day-to-day capacity, although I would still frequently chat wit…

CPS is fairly dead as an IR, but the (local) CPS transform seems more popular than ever with languages implementing "stackless" control effects. As far as functional IRs go, I woul…

> Call/ret instructions work really well with branch predictors. Lots of jumps (to continuations) might not work quite as well. On x86, the use of paired call/return is conflated w…

There's an OOPSLA paper (referred to from the link starting that thread) from this year with 2 of the same authors that goes into more detail about using it as a compiler IR: https…

It shouldn’t be difficult to write a binary translator to run 32-bit executables on a 64-bit userspace. You will take a small performance hit (on top of the performance hit of usin…

Yes, in fact Lean proves the law of the excluded middle using Diaconescu's theorem rather than assuming it as an independent axiom: https://github.com/leanprover/lean4/blob/ad1a017…

Lean’s type theory extends CIC with the (global) axiom of choice, which increases consistency strength over base CIC.

Interesting! IIRC, the LLVM passes dedicated to dodging this issue were contributed by Intel engineers, so maybe there’s some bias.

> This is a significant problem on AMD; Intel and Apple seems to be better. When did this change? In my testing years ago (while I was writing Rosetta 2, so Icelake-era Intel), Int…

Intel has always had terrible subnormal performance. It's not that difficult to implement in HW, and even if you still want to optimize for the normalized case, we're talking about…

> it's the natural implementation in hardware The natural implementation in hardware is that addition of two N-bit numbers produces an N+1-bit number. Most architectures even expos…

Cyclone had borrowing. See Section 4.4 (Temporary Aliasing) in the paper https://homes.cs.washington.edu/~djg/papers/cyclone_memory.p... or the more detailed discussion throughout …

Thanks. It means a lot coming from someone with experience in our niche field.