projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8f379cb) | patch
test: add "double release sequence" test
authorBrian Norris <banorris@uci.edu>
Mon, 8 Oct 2012 06:30:48 +0000 (23:30 -0700)
committerBrian Norris <banorris@uci.edu>
Mon, 8 Oct 2012 06:34:45 +0000 (23:34 -0700)
commit07d9e344693c6d2b85f821447be80deaee118b65
tree942d4e8b56431eb33c898b2b996246219d103e78tree | snapshot
parent8f379cb70822bfd5498da9997ad4f7c3b37a18edcommit | diff
test: add "double release sequence" test

This test uses two separate load-acquire's to establish the same release
sequence. This can cause problems with the current release sequence
fixups, so that we find an execution where one synchronizes and the
other doesn't, even when reading from the same sequence.
test/double-relseq.c [new file with mode: 0644] blob
C++11 memory model checker