Tools to experiment with weakly ordered concurrenc

2019-05-28 17:10发布

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

2条回答
Melony?
2楼-- · 2019-05-28 17:36

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.

查看更多
三岁会撩人
3楼-- · 2019-05-28 17:42

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.

查看更多
登录 后发表回答