projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 89bcfc7) | patch
check_recency: only allow newer stores to "overwrite"
authorBrian Norris <banorris@uci.edu>
Sat, 2 Mar 2013 08:04:44 +0000 (00:04 -0800)
committerBrian Norris <banorris@uci.edu>
Sat, 2 Mar 2013 08:04:44 +0000 (00:04 -0800)
commit284151d644be0946f887561a03344866f0665c03
tree1cf4158396f671c8b360f55ba62fbcf217f3d08dtree | snapshot
parent89bcfc74c2999b15984759e5b0eab4a9c46feaf3commit | diff
check_recency: only allow newer stores to "overwrite"

For a "live" memory system, we only want to force a store to appear if
it is modification-ordered after the store we're reading from.

Also, delete my old comment about reads-from feasibility.
model.cc diff | blob | history
C++11 memory model checker