cwzwarich

6 ms·

1.
by cwzwarich 3d ago
[Disclaimer: I wrote Rosetta 2, so everything I say is biased by that.] Contemporary out-of-order CPUs are incredibly over-provisioned; microarchitects will justify a new feature by another 0.1% gain on some benchmark. The end result is a C
2.
by cwzwarich 3d ago
That may be true at iso-voltage/frequency, but there are definitely places on that curve where it is better to be at a lower voltage (and thus frequency) than to run at a higher voltage just so you can race to idle.
3.
by cwzwarich 2mo ago
`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 you could have an alternate `accumulate_associative` that us
4.
by cwzwarich 6mo ago
https://github.com/coreboot/coreboot/blob/main/src/soc/intel...
5.
by cwzwarich 9mo ago
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 die. Each has functionality that the other does not wit
6.
by cwzwarich 10mo ago
Isn’t the 9000 TFLOP/s number Nvidia’s relatively useless sparse FLOP count that is 2x the actual dense FLOP count?
7.
by cwzwarich 11mo ago
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 existence of a universe as a model of set theory. But then you
8.
by cwzwarich 11mo ago
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 to bounded Zermelo set theory (i.e. ZF without Foundation or
9.
by cwzwarich 11mo ago
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 systems, proposed new language constructs, and it was generally
10.
by cwzwarich 11mo ago
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 as I am aware. There is other work on specifying Rust (e.g.
11.
by cwzwarich 11mo ago
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 with the team and give input on future directions.
12.
by cwzwarich 1y ago
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 would say SSA corresponds most directly to (a first-or
13.
by cwzwarich 1y ago
> 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 with usage of the stack to store activation reco
14.
by cwzwarich 1y ago
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://dl.acm.org/doi/10.1145/372
15.
by cwzwarich 1y ago
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 using the 32-bit architecture to begin with), but that should be
16.
by cwzwarich 1y ago
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/ad1a017949674a947f0...
17.
by cwzwarich 1y ago
Lean’s type theory extends CIC with the (global) axiom of choice, which increases consistency strength over base CIC.
18.
by cwzwarich 1y ago
Interesting! IIRC, the LLVM passes dedicated to dodging this issue were contributed by Intel engineers, so maybe there’s some bias.
19.
by cwzwarich 1y ago
> 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), Intel only allowed a load to forward from a single store, an
20.
by cwzwarich 1y ago
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 a 1 cycle penalty, not an order(s)-of-magnitude p
21.
by cwzwarich 1y ago
> 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 expose this extra bit as a carry bit.
22.
by cwzwarich 2y ago
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 this journal paper: https:/
23.
by cwzwarich 2y ago
Thanks. It means a lot coming from someone with experience in our niche field.
24.
by cwzwarich 2y ago
I did go to Mozilla Research to work on Servo/Rust for a bit in 2015, which didn’t turn out to be the best decision. I always assumed that I would stick around at Apple until some singular event that would motivate me to quit, and that
25.
by cwzwarich 2y ago
I had an interest in programming at an early age. My dad would always bring home the old computer magazines from the IT department at work and I would pore over them. I got a bit obsessed with MIT AI lab myths in books like Levy’s Hackers.
26.
by cwzwarich 2y ago
Well, the first thing to realize about scaling codebases with developers is that an N developer team will usually produce a codebase that requires N developers to maintain. So by starting small and staying small until you reach a certain cr
27.
by cwzwarich 2y ago
> May I ask, what is the path that leads you to the Rosetta 2 project? The member of senior management who was best poised to suggest who should work on it already knew me and thought I would be the best choice. Getting opportunities in
28.
by cwzwarich 2y ago
I don't think there was a single tipping point, just a growing accumulation of factors: - the release of Lean 4 slightly over a year ago, which impressed me both as a proof assistant and a programming language - the rapid progress in f
29.
by cwzwarich 2y ago
I was the only person working on it for ~2 years, and I wrote the majority of the code in the first version that shipped. That said, I’m definitely glad that I eventually found someone else (and later a whole team) to work on it with me, an
30.
by cwzwarich 2y ago
If you’re interested in applications of AI to mathematics, you’re faced with the problem of what to do when the ratio of plausible proofs to humans that can check them radically changes. There are definitely some in the AI world who feel th

More ›