projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d7ef8a4) | patch
promise: add 'same_value' helper, force value-checking in CycleGraph
authorBrian Norris <banorris@uci.edu>
Fri, 1 Mar 2013 21:11:27 +0000 (13:11 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 1 Mar 2013 21:19:19 +0000 (13:19 -0800)
commit875ebf8e11b4bdd702604785837b6b91b748900d
treebe3fa2911ce7e063792529ee7d63bb4ecb7a9b23tree | snapshot
parentd7ef8a452c36e2ab3e56a8c43639006dc64d5d18commit | diff
promise: add 'same_value' helper, force value-checking in CycleGraph

This fixes a potential bug, in which a write could merge with a
different promised value. It's unclear whether this ever manifested
itself, since I believe we had some implicit logic that would ensure
that this did not happen.
cyclegraph.cc diff | blob | history
model.cc diff | blob | history
promise.cc diff | blob | history
promise.h diff | blob | history
C++11 memory model checker