cwzwarich

I don't think any other architecture ever supported it.

As my sibling comment from jcranmer points out, it was only `memory_order_consume` that failed outright. The other aspects of the C++ memory model mostly worked out, at least after revision.

I believe the last attempt to come up with a comprehensive new proposal was P0190 (https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p01...), which reduced the ordering-imposing dependencies in the model to essentially just be pointer dependencies (which does eliminate some legitimately useful cases, e.g. stealing bits from pointers). The paper mentions the unresolved problem of control dependencies from compiler knowledge of pointer equality, which is intertwined with the pointer provenance discussions from around the same time.

I would like to see the basic concept realized in another language some day.

Fun fact: ARM actually has relaxed address dependencies for non-temporal loads, although I don't know if too many implementations of ARM take advantage of this relaxation.

I think it is an interesting question. During the Alpha's lifetime as a non-hobbyist architecture, this decision was pretty much universally derided, but this was in the prehistoric eras of concurrent memory models, where people were just trying their best with a mix of C code, intrinsics, uses of `volatile` sprinkled around to hopefully disable optimizations, and inline assembly. When the C++11 memory model came around, they tried to integrate dependency ordering with `memory_order_consume`, and this famously failed, along with every attempt to fix it. I believe the plan is now for C++ (and later C?) to add special-cased RCU primitives.

The relaxation makes sense in the abstract. As evidenced from the `memory_order_consume` saga, compiler optimizations regularly violate dependency ordering anyways, so in the strictest sense you can't really rely on it. Of course, that doesn't stop people from "knowing" what their compilers will do in such a situation, but that strategy has become a worse one as the years have passed. I would feel better about the whole situation if there was a good greenfield design for a low-level PL that incorporates explicit dependency ordering.

I think it's less clear where the potential HW benefit is in a contemporary CPU. The obvious answer is value prediction, but any CPU performing value prediction has to deal with so many other microarchitectural conditions that can invalidate its speculation decisions that it's not clear this minor one is a huge burden. Of course, people who love TSO might make the same argument, i.e. that it's not a huge burden to snoop cache traffic and invalidate loads (although this is only the load half of TSO, not the store half). I know an Alpha architect who argued that Alpha was right for this decision. I even knew a Transmeta architect who argued for implementing sequential consistency in HW (as Transmeta and derived CPUs actually did).

In practice, microarchitectural structures have capacity/throughput limitations, and there are implementations and complexities that only come up in a real design, so everything needs to be evaluated in the context of a real project. I personally think the sweet spot falls to the weaker side of TSO, which also happens to be near the memory consistency model of the low-level languages we're using anyways.

Probably different teams. Plus you can not underestimate the role that momentum plays in semiconductor engineering teams. If some respected person determined that subnormals are either Hard (tm) or not a Real Problem (tm), it will take a long time to correct this mistaken belief. I believe there have been some recent academic papers on FP implementation from the Intel E-Core team, which is a sign that they are a bit more with the times.

[Disclaimer: I wrote Rosetta 2 and determined the spec for Apple's TSO mode, so I am obviously biased.]

Giesen's article comes off as well-meaning cope from an x86 fan. A relaxed memory model really does give you some performance. Another memory model flaw here in x86 is more architectural, which is that every instruction with the LOCK prefix is essentially a full barrier (of course, x86 could have provided different instructions while still being under TSO). In programs that make heavy usage of atomic reference counting, this actually helps quite a bit.

I would probably put that performance benefit in the single digit percentage range like my sibling comment, which may not seem like much to a SW engineer but is actually pretty serious in CPU microarchitecture. It also helps to be stacked with other architectural advantages over x86, e.g. fixed-length instructions, 32 GPRs (which Intel copied in APX), LDP/STP (which Intel also copied in APX), etc.

One of the old arguments from TSO enjoyers was that TSO helps avoid concurrency bugs that people would accidentally introduce, but this was before the C++ memory model propagated throughout the programming world. Nowadays, I think people generally conceptualize memory consistency in terms of acquire/release anyways, so why not use a CPU architecture that uses the same model?

[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 CPU that's pretty decent at handling the sort of code bloat that comes from a binary translator.

There's also a big tradeoff in adding more optimizations to a binary translator. You would like to be able to precisely handle exceptions (especially ones caused by invalid memory accesses) while presenting a userspace exception handler with an architecturally valid state for the source program. There are some optimizations that would be easy to do in principle but are painful for maintaining this mapping between source program states and translated program states. The complexity burden combined with the difficulty of debugging that added complexity (or exhaustively verifying it up-front) shapes many of your decisions when writing a production binary translator. You should always have more Cool (tm) ideas than you actually use in practice.

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.

`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 uses the same interface but assumes the reduction is associative and has unspecified evaluation order?

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 within an SM/TPC, nevermind the very different fabric and memory subsystem (with much higher bandwidth/SM on the datacenter parts). They run at very different clock frequencies. It just wouldn't make sense to share the dies under these constraints, especially when GPUs already present a fairly obvious yield recovery strategy.

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 theory. But then you’re stuck reasoning semantically about a model of set theory. Nobody has scaled this up to a large pluralist math library like Mathlib.

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 Replacement, and with Separation restricted to formulas with bounded quantifiers). This is unfortunately too weak to formalize post-WW2 mathematics in the same style as is done by ordinary mathematicians. Similarly, it does not offer a great way to deal with the size issues that arise in e.g. category theory.

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 a success (look at the proliferation of C in the 90s across many different systems and architectures).

The actual informal semantics in the standard and its successors is written in an axiomatic (as opposed to operational or denotational) style, and is subject to the usual problem of axiomatic semantics: one rule you forgot to read can completely change the meaning of the other rules you did read. There are a number of areas known to be ill-specified in the standard, with the worst probably being the implications of the typed memory model. There have since been formalized semantics of C, which are generally less general than the informal version in the standard and make some additional assumptions.

C++ tried to follow the same model, but C++ is orders of magnitude more complex than C and thus the standard is overall less well specified than the C++ standard (e.g. there is still no normative list of all the undefined behavior in C++). It is likely practically impossible to write a formal specification for C++. Still, essentially all of the work on memory models for low-level programming languages originates in the context of C++ (and then ported back to C and Rust).

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. the Unsafe Code Guidelines Working Group), but nothing approaching a real spec for the whole language. Honestly, it is probably impossible at this point; Rust has many layers of implementation-defined hidden complexities.

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.

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-order restriction of) ANF w/ join points. The main difference being the use of dominance-based scoping rules, which is certainly more convenient than juggling binders when writing transformations. The first-order restriction isn't even essential, e.g. https://compilers.cs.uni-saarland.de/papers/lkh15_cgo.pdf.

If you're interested in an IR that can express continuations (or evaluation contexts) in a first-class way, a much better choice than CPS is an IR based on the sequent calculus. As I'm sure you know (since you work with one of the coauthors), this was first experimented with in a practical way in GHC (https://pauldownen.com/publications/scfp_ext.pdf), but there is a paper in this year's OOPSLA (https://dl.acm.org/doi/10.1145/3720507) that explores this more fundamentally, without the architectural constraint of being compatible with all of the other decisions already made in GHC. Of course, one could add dominance scoping etc. to make an extension of SSA with more symmetry between producers and consumers like the classical sequent calculus.

> 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 records. On AArch64, indirect branches can be marked with a hint bit indicating that they are a call or return, so branch prediction can work exactly the same with activation records elsewhere.

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 with), but that should be fine for anything old enough to not be recompiled.

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 a single store, and no partial forwarding (i.e. mixed cache/register) without a huge penalty, whereas AMD at least allowed partial forwarding (or had a considerably lower penalty than Intel).

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 penalty.

> 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:

https://homes.cs.washington.edu/~djg/papers/cyclone_scp.pdf

As their citations indicate, the idea of borrowing appeared immediately in the application of subtructural logics to programming languages, back to Wadler's "Linear types can change the world!". It's just too painful without it.

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 to quit, and that would be it. I have been so lucky at Apple to have been in the right place at the right time for several projects: relatively early iPhone team, original iPad team, involved in the GCC -> Clang transition, involved in the 64-bit ARM transition, involved in early Apple Watch development, first engineer working full-time on the Apple silicon transition for the Mac, etc. Obviously I was doing something right if I kept getting these chances, but if I went to another FAANG I wouldn’t have the same history, and I don’t think it would be the same experience.

My projected path to parting ways with Apple didn’t really take place, since I’m now working at a non-profit dedicated to developing an interactive theorem prover and left Apple without any animosity in either direction.

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. In a stroke of luck, I found a copy of SICP at the local bookstore in middle school and kept struggling through it.

I originally wasn’t going to go to university, but my parents suggested I go for CS. I transferred into Pure Math in my first term after the intro Java programming course asked us to implement tic-tac-toe without using arrays.

Basically all of the low-level programming and systems stuff was learned on the job, but it helped that my first job at Apple was working on WebKit’s interpreter (and later JIT), coming out of a Google Summer of Code doing the same thing. One of my coworkers on that project was an alumnus of the original Rosetta from Transitive, and he later ended up managing the group doing the transition to Apple silicon on the SWE side (I was part of HW Technologies). An interesting example of how things loop back in the industry.