...
| Wiki Markup |
|---|
{html}—{html} |
an illustrative encoding of a behavior that the model should allow or prohibit. Given these inputs, the tool outputs a trace of the program for which the assertions are satisfied or, if no such trace exists, it outputs a minimal subset of the program and memory model constraints that are unsatisfiable.
MemSAT has been applied to several existing memory models and their published litmus tests, including the current Java Memory Model by Manson et al., and a revised version of it by Sevcik and Aspinall. The results revealed subtle discrepancies between what was expected and the actual results of test programs.
...