3 ms·

It seems like weak memory models get short shrift, but if you're going to program without locks it's semi-important to understand what information one gets when

It seems like weak memory models get short shrift, but if you're going to program without locks it's semi-important to understand what information one gets when examining a read-write pair. It's true that (as implied by the article) you can probably get by with just studying/programming with the C/C++ [1][2] "atomic" memory access types and letting the compiler enforce those semantics, though the reasoning behind a lot of these memory orderings is lost without understanding the motivation/arch. models behind them. If you're interested in the C/C++ memory models there's active research into specifying them without bad behavior (thin-air reads [3]). Recent results include a semantics that makes value promises and requires a justifying execution [4] which is not totally dissimilar from those required by the official java memory model [5]. 1. http://en.cppreference.com/w/cpp/atomic/atomic http://en.cppreference.com/w/cpp/atomic/atomic 2. http://en.cppreference.com/w/c/atomic http://en.cppreference.com/w/c/atomic 3. http://www.cl.cam.ac.uk/~pes20/cpp/notes42.html http://www.cl.cam.ac.uk/~pes20/cpp/notes42.html 4. https://people.mpi-sws.org/~dreyer/papers/promising/paper.pdf https://people.mpi-sws.org/~dreyer/papers/promising/paper.pd... 5. http://rsim.cs.uiuc.edu/Pubs/popl05.pdf http://rsim.cs.uiuc.edu/Pubs/popl05.pdf

bshanks 9y ago
I wonder how the memory model in https://people.mpi-sws.org/~dreyer/papers/promising/paper.pdf https://people.mpi-sws.org/~dreyer/papers/promising/paper.pd... compares to the WMM and WMM-S memory models given in https://arxiv.org/pdf/1707.05923.pdf https://arxiv.org/pdf/1707.05923.pdf ; and if there are other research memory models out there that should also be considered?
- johnbender 9y ago
  These papers take forever to read (take it from me, I am doing research in this area, in particular proofs of correctness for lock free programs). I recommend focusing on the C/C++ ones if only for the practical value. As for comparison, the C/C++ memory model is more general and is operational. It is also formalized in coq and has some good theorems (data race free sequential consistency being the most obvious). The RISC memory model is axiomatic and follows the standard axiomatic approach adopted for many other memory models like Java and the current C/C++ standard. That's not a dig, they just don't care as much about rigor. Axiomatic models consider the every possible execution and then weed out bad ones, where as the operational semantics defines the set of all possible executions using a transition relation. If you're into math you might see these vaguely as extensional and intensional respectively.
  - bshanks 9y ago
    thanks! I think the RISC/WMM folks provide an operational model too, using their own "I2E" formalism. The end of the paper seems to have a proof of equivalence between their axiomatic and operational models.

bshanks 9y ago

I wonder how the memory model in https://people.mpi-sws.org/~dreyer/papers/promising/paper.pdf https://people.mpi-sws.org/~dreyer/papers/promising/paper.pd... compares to the WMM and WMM-S memory models given in https://arxiv.org/pdf/1707.05923.pdf https://arxiv.org/pdf/1707.05923.pdf ; and if there are other research memory models out there that should also be considered?

johnbender 9y ago
These papers take forever to read (take it from me, I am doing research in this area, in particular proofs of correctness for lock free programs). I recommend focusing on the C/C++ ones if only for the practical value. As for comparison, the C/C++ memory model is more general and is operational. It is also formalized in coq and has some good theorems (data race free sequential consistency being the most obvious). The RISC memory model is axiomatic and follows the standard axiomatic approach adopted for many other memory models like Java and the current C/C++ standard. That's not a dig, they just don't care as much about rigor. Axiomatic models consider the every possible execution and then weed out bad ones, where as the operational semantics defines the set of all possible executions using a transition relation. If you're into math you might see these vaguely as extensional and intensional respectively.
- bshanks 9y ago
  thanks! I think the RISC/WMM folks provide an operational model too, using their own "I2E" formalism. The end of the paper seems to have a proof of equivalence between their axiomatic and operational models.