Relaxed memory models must be rigorous

[kimo]

This interesting 2009 deep dive into the memory models for current processors finds problems with them all.  Are any of these issues problems for algorithms discussed here?

"Relaxed memory models must be rigorous"

http://moscova.inria.fr/~zappa/readings/positionec2.pdf

[Michael Oksenenko]

http://research.sun.com/scalable/pubs/index.html

[Dmitriy V'jukov]

When I provide algorithms for relaxed memory model it's usually C++0x
memory model. Then, I usually use (or it's possible to use) Relacy
Race Detector for complete enough verification.
(Note that frequently I provide implementations only for strong enough
x86/Windows, and sometimes algorithms are not tested, i.e. just
sketches)

- precise
Not applicable. C++0x is precise enough for practical reasons.

- testable
Not applicable. C++0x is testable enough.

- accurate with respect to implementations
Do not understand. Probably not applicable.

- loose enough for future implementations
I am not developing memory model nor future hardware, so not
applicable.

- should be strong enough for programmers
Bullshit.

- should be integrated with the semantics of the rest of the system
Not applicable. C++0x memory model is enough integrated with the rest
of the system.

- should be accessible
Not applicable. I already have understood C++0x memory model, not
matter how it's described.


If you take a look at their "C++ section", they actually do not reveal
anything real bad about it.
The whole paragraph with insignificant technical ambiguities and vague
epithets can be skipped ("At a first glance the non-expert...").
The paragraph about low-level atomics only states that (1) they are
complex, and (2) they are described informally. (1) is not the problem
of a description, it's a problem of the domain. You can't explain
rocket science to schoolboy with simple words. They can't solve that
with mathematical formulas. And (2) is plain bullshit, it's described
not on a mathematical language, but it's formal. I've implemented
precise C++ memory model in Relacy Race Detector, and I would be
unable to implement something blurry. In general it's described in
such a way that you are able to get formal answer as to whether some
program has races or not (has required behavior or not, etc).


Well, I think that the only problem that is fully applicable to
algorithms discussed here is the problem that relaxed memory models
are complex. Yes, they are inherently complex, and algorithms based on
them are complex.


--
Dmitriy V'jukov