From 57f11820dd7dc4c3b95459a8de99305ac31f88bf Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sat, 2 Mar 2013 12:17:02 -0800 Subject: [PATCH] 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 | 11 +++++++---- model.h | 7 ++++--- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/model.cc b/model.cc index b0ca05e..5a1f399 100644 --- a/model.cc +++ b/model.cc @@ -887,6 +887,8 @@ bool ModelChecker::process_read(ModelAction *curr) value = promise->get_value(); curr->set_read_from_promise(promise); mo_graph->startChanges(); + if (!check_recency(curr, promise)) + priv->too_many_reads = true; updated = r_modification_order(curr, promise); mo_graph->commitChanges(); break; @@ -1642,8 +1644,8 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { return lastread; } -template -bool ModelChecker::should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const +template +bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const { /* Need a different write/promise */ if (other_rf->equals(rf)) @@ -1681,10 +1683,11 @@ bool ModelChecker::should_read_instead(const ModelAction *curr, const ModelActio * If so, we decide that the execution is no longer feasible. * * @param curr The current action. Must be a read. - * @param rf The store from which we might read. + * @param rf The ModelAction/Promise from which we might read. * @return True if the read should succeed; false otherwise */ -bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const +template +bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const { if (!params.maxreads) return true; diff --git a/model.h b/model.h index 3f4ca00..d8c1be4 100644 --- a/model.h +++ b/model.h @@ -167,10 +167,11 @@ private: Thread * take_step(ModelAction *curr); - bool check_recency(ModelAction *curr, const ModelAction *rf) const; - template - bool should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const; + bool check_recency(ModelAction *curr, const T *rf) const; + + template + bool should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const; ModelAction * get_last_fence_conflict(ModelAction *act) const; ModelAction * get_last_conflict(ModelAction *act) const; -- 2.34.1