projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86e0aa7) | patch
model: force THREAD_START to immediately follow THREAD_CREATE
authorBrian Norris <banorris@uci.edu>
Fri, 7 Sep 2012 18:25:25 +0000 (11:25 -0700)
committerBrian Norris <banorris@uci.edu>
Fri, 7 Sep 2012 18:29:16 +0000 (11:29 -0700)
commit8c83f796d2930427478e603d64e8410707011007
tree564fc1e1d3102f98885da7fe2ef39edb62d50a33tree | snapshot
parent86e0aa7f0ea574f58afb0109b1e02a578a429eb1commit | diff
model: force THREAD_START to immediately follow THREAD_CREATE

Note that on the current userprog.c test case, this change causes more
infeasible executions to appear. This is somewhat unexpected but probably just
a result of sub-optimal scheduling.
model.cc diff | blob | history
C++11 memory model checker