projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2099424) | patch
model: bugfix - missing SC mo_graph edge
authorBrian Norris <banorris@uci.edu>
Tue, 12 Mar 2013 17:47:41 +0000 (10:47 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 12 Mar 2013 17:54:15 +0000 (10:54 -0700)
commit34aa82864b18e6f11d806ef77e4b992c2e19f370
tree86a35c2d6c9758edf0bf26211b0494e92b903516tree | snapshot
parent20994240335ce1d54fb6c4b2c8df684182f0a3f9commit | diff
model: bugfix - missing SC mo_graph edge

We must enforce a rule such as the following, derived from C++ Section
29.3, statement 3 (second subpoint):

if is_store(X) && is_seq_cst(X) && is_store(Y) && is_load(Z) &&
   is_seq_cst(Z) &&
   X --sc-> Z && Y --rf-> Z && X != Y
then
   X --mo-> Y

This has been checked (via manual test-case) to fix a bug which allowed
an inconsistent mo/sc/rf relationship.
model.cc diff | blob | history
C++11 memory model checker