This commit makes the code a bit more compact by using ERROR_ON()
whenever possible. It also renames a particularly verbose variable
used in ERROR's condition.
GenMC has a single API that was handled in a collection of different
files. This commit collects all API wrappers to Exploration.cpp.
(The Setup.cpp file remains intact as it contains setting translation
and setup functions.)
When GenMC says that an execution should not be explored further,
Miri needs to know why (e.g., so that it returns an appropriate
exit value). Until now, some (erroneous) heuristics were used
for that.
This commit changes the Miri/GenMC API to check the scheduling
result of GenMC (that now reflects the "stop type").
The new error-reporting mechanism of GenMC changed its public API.
This commit adjusts the Miri interface accordingly (all driver
calls need an extra argument that represents possible debugging
information).
GenMC v0.14.1 does not throw an error internally if the config
is invalid, but rather returns an appropriate error value.
This commit has setup code in Miri check the returned value,
and exit if there are any errors.
- Implement support for 'assume' statements.
- Improve scheduling and next instruction type determination.
- Improve GenMC mode documentation.
Co-authored-by: Ralf Jung <post@ralfj.de>
- Handling Compare-Exchange operations.
- Limitation: Compare-Exchange currently ignores possibility of spurious failures.
- Limitation: Compare-Exchange failure memory ordering is ignored.
- Upgrade compare-exchange success ordering to avoid reporting non-existent bugs.
- Add warnings for GenMC mode for unsupported features.
- Add a lot of tests, including translation of GenMC litmus tests and Loom tests.
- Cleanup
- Support for atomic fences.
- Support for atomic read-modify-write (RMW).
- Add tests using RMW and fences.
- Add options:
- to disable weak memory effects in GenMC mode.
- to print GenMC execution graphs.
- to print GenMC output message.
- Fix GenMC full rebuild issue and run configure step when commit changes.
- Do cleanup.
Co-authored-by: Ralf Jung <post@ralfj.de>
- Implement memory allocation compatible with GenMC.
- Extract address generator struct from Miri's allocator.
- Support thread creation and joining.
- Support atomic load and store.
- Support scheduling through GenMC.
- Add tests for GenMC mode.
- Add clang-format file for C++ code in Miri.
- Update genmc-sys crate license to MIT/Apache to match GenMC dependency.
- Add documentation for GenMC mode.
Note: this commit depends on changes to GenMC not yet upstreamed to its official repository.
Co-authored-by: Ralf Jung <post@ralfj.de>
