projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2de6c82) | patch
model: disabled threads are "future ordered"
authorBrian Norris <banorris@uci.edu>
Sun, 7 Oct 2012 22:04:08 +0000 (15:04 -0700)
committerBrian Norris <banorris@uci.edu>
Sun, 7 Oct 2012 22:26:48 +0000 (15:26 -0700)
commit8669bd6f88178382893b48223498611f2200714a
tree0dfa5e12023020cf08c8eb36506459f5251f95b9tree | snapshot
parent2de6c82d6d7e6af2267636ec55f7e81d2a799a78commit | diff
model: disabled threads are "future ordered"

If a Thread is not currently enabled, then it will synchronize with
another (currently-enabled) Thread if/when it wakes up. Thus, it
qualifies as "future ordered" within the release sequence code: it
cannot contribute future writes that will break current pending release
sequences.
model.cc diff | blob | history
C++11 memory model checker