`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…
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 die. Each has functionality that the…
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 existence of a universe as a model of set…
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…
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,…
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…
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…
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…
> 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…
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/3720507
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…
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...
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), Intel only allowed a load to forward from…
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…
> 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.
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:…
Thanks. It means a lot coming from someone with experience in our niche field.
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…
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…
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…
> 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…
`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…
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 die. Each has functionality that the…
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 existence of a universe as a model of set…
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…
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,…
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…
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…
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…
> 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…
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/3720507
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…
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...
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), Intel only allowed a load to forward from…
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…
> 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.
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:…
Thanks. It means a lot coming from someone with experience in our niche field.
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…
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…
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…
> 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…