check_recency: improve templates, use when reading from Promise
authorBrian Norris <banorris@uci.edu>
Sat, 2 Mar 2013 20:17:02 +0000 (12:17 -0800)
committerBrian Norris <banorris@uci.edu>
Sat, 2 Mar 2013 20:17:02 +0000 (12:17 -0800)
commit57f11820dd7dc4c3b95459a8de99305ac31f88bf
tree060edf6d280d9ee1116884367181b950b381d72c
parent745b71256a4b96ddf4843c7f66b11d0cb3daa3cb
check_recency: improve templates, use when reading from Promise

This completes (?) the improvements to check_recency, such that it now
can force new writes to be "seen" if we are reading from an "old"
Promise too many times in a row.

mpmc-queue-noinit now runs to completion (with ASSERT() enabled):

  $ time ./run.sh mpmc-queue/mpmc-queue-noinit -f 10 -m 2
  + mpmc-queue/mpmc-queue-noinit -f 10 -m 2
  ******* Model-checking complete: *******
  Number of complete, bug-free executions: 119828
  Number of redundant executions: 38743
  Number of buggy executions: 0
  Number of infeasible executions: 344469
  Total executions: 503040
  Total nodes created: 7585797

  real 2m29.674s
  user 2m18.269s
  sys 0m10.929s
model.cc
model.h