projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 502c702) | patch
action: THREAD_JOIN can synchronize against execution order
authorBrian Norris <banorris@uci.edu>
Wed, 19 Sep 2012 01:37:22 +0000 (18:37 -0700)
committerBrian Norris <banorris@uci.edu>
Wed, 19 Sep 2012 01:37:22 +0000 (18:37 -0700)
commitca6361d9a70f1336c65956f049167135c2a417a8
tree955e14ad3cc96809b4d712bc3848bac0fedeef46tree | snapshot
parent502c7029755b194e52526fe26c2e7327b5d64101commit | diff
action: THREAD_JOIN can synchronize against execution order

synchronize_with() had an assertion to ensure that synchronization never
occurred opposite the execution trace ordering. But THREAD_JOIN is a special
case, where this ordering won't break the rest of the model-checker.
action.cc diff | blob | history
C++11 memory model checker