create memory model litmus tests - Githubissues

chapel-lang / chapel

a Productive Parallel Programming Language

https://chapel-lang.org

Other

1.77k stars 417 forks source link

create memory model litmus tests #11275

Open mppf opened 5 years ago

mppf commented 5 years ago

Create a set of small example Chapel programs that can serve as litmus tests. These examples can be studied by model checkers / formal verifiers to check that the behaviors allowed by Chapel's memory consistency model are understood and expected.

mppf commented 5 years ago

Some papers for inspiration of what a "litmus test" is:

seems to be a starting paper for "litmus tests" in this context https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/
about how many litmus tests are needed / how long http://www.cis.upenn.edu/acg/papers/dac11_litmus.pdf
tasks through several common litmus tests https://people.mpi-inf.mpg.de/~jblanche/ppdp2011-cpp-mem.pdf
interesting approach to generate them https://research.nvidia.com/sites/default/files/pubs/2017-04_Automated-Synthesis-of//ASPLOS_2017_Memory_Model_Verification.pdf
appendix lists some C++ memory model litmus tests https://arxiv.org/pdf/1606.01400.pdf

mppf commented 5 years ago

Tricky bits in C++ memory consistency model:

Out of Thin Air Reads: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/n4375.html
restricting SC reads: https://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf