c4-project / c4f

The C4 Concurrent C Fuzzer
MIT License
14 stars 1 forks source link

Add full support for the `litmus7` tool #53

Closed MattWindsor91 closed 5 years ago

MattWindsor91 commented 5 years ago

Like herd7, litmus7 checks memory-model behaviour of assembly programs; unlike herd7, it does so by running the program a very large number of times on an actual machine. This means that its results are not guaranteed to be complete.

Supporting it is useful for three use cases:

It is not useful for getting a C11-compliant execution set from C, since it'll just compile the C down to assembly!

At time of writing, act has very rudimentary support for litmus in its litmusify mode. This issue tracks completing that support.

MattWindsor91 commented 5 years ago

See #81 for a possible bug related to litmus7.

MattWindsor91 commented 5 years ago

I think this is, more or less, done now.