back

by raphlinus·2y ago·view on hn ↗
I'm not sure how I feel about this. Are there nontrivial programs that depend on the (1, 1) outcome of the LB litmus test being forbidden? (See section 2.3 of the Lahav paper[1] for definitions and context)

If so, then these programs are at significant risk of miscompilation on compilers today. Strengthening the standard would mean that this risk continues until compilers are updated.

If not, then the proposal is asking for an (admittedly modest) performance regression to address what might not be a real problem.

Rust doesn't have a formal memory model yet, but the loom tool reports the (1, 1) outcome as not allowed[2]. I also ran it as normal threaded Rust code (not using a model checker) on M1 Max (which in theory is subject to the same miscompilation), and was not able to reproduce the failures as reported in the linked paper[3], but that doesn't mean much, as it's notoriously tricky to observe memory model violations.

In GPU-land, the (1, 1) outcome is allowed, as can be verified in the Vulkan memory model by the Alloy test in the second file of [2]. Neither HLSL nor Metal Shading Language have proper memory models, so it's hard to say, but in general it's fair to expect that anything allowed by the Vulkan memory model can be observed in other GPU implementations.

Perhaps what is called for is a finer gradation of strength, where the author explicitly asks for the guarantees needed, and the compiler inserts the BAL when it's needed, and skips it if not. Already I can see a lot of value in an explicit "unordered" value for ordering, which would be even weaker than relaxed (allowing more compiler optimization).

[1]: https://plv.mpi-sws.org/scfix/paper.pdf

[2]: https://gist.github.com/raphlinus/41d78d04d117ab0ba3b77065b9...

[3]: https://arxiv.org/pdf/2310.12337.pdf