Tools to experiment with weakly ordered concurrenc

问题:

What tools exist to help one to experiment with weakly ordered concurrency? That is, in what sandbox can one play while teaching oneself about partial fences, weak atomics, acquire/consume/release semantics, lock-free algorithms and the like?

The tool or sandbox one wants would exercise and stress one's weakly ordered, threaded algorithm, exposing the various ways in which the algorithm might theoretically fail. Physically running on an x86, for example, the tool would nevertheless be able to expose ARM-type failures.

An open-source tool would be preferable. Please advise.

References:

• the C++11 draft standard (PDF, see clauses 1, 29 and 30);
• Hans-J. Boehm's overview of the subject;
• McKenney, Boehm and Crowl on the subject;
• GCC's developmental notes on the subject;
• the Linux kernel's notes on the subject;
• a related question with answers here on Stackoverflow
• another question, this one comparing fences against atomics;
• Cppmem (on the advice of @KerrekSB);
• Cppmem's help page;
• Spin (a tool for analyzing the logical consistency of concurrent systems, on the advice of @JohnZwinck).

(The references are oriented toward C++11 because this is how I happen to have approached the subject. However, for all I know, a non-C++ answer might be best, so feel free to extend your answer beyond C++ as you see fit.)

回答1:

This is quite a bit more general than what your question directly asks, but take a look at "Spin," a "model checker" for concurrent systems. An online manual is here: http://spinroot.com/spin/Man/Manual.html

You will probably find it to be a bit "old school" in feel, but I see no reason why it wouldn't be suitable for the jobs you're interested in. Since it is quite general, however, you may need to do a bit of work to teach the tool about the problem space. The good news is that it is platform-independent. The bad news is you'd probably need to model each computer architecture explicitly (Spin doesn't intrinsically know about the guarantees of ARM vs. x86, for example). But maybe some of that work has been done elsewhere (I didn't check), and/or you could share pieces of what you do so others may benefit. The tool is open-source, after all.

回答2:

You might be interested in having a look at http://www.cprover.org/wmm/ and follow the links there leading to tools and corresponding papers about weak memory, in particular the CAV 2013 paper Partial Orders for Efficient BMC of Concurrent Software and the CAV 2014 paper Don't sit on the fence: A static analysis approach to automatic fence insertion might be good starting points. You will also find lots of real-world example code and benchmarks there.