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
value = promise->get_value();
curr->set_read_from_promise(promise);
mo_graph->startChanges();
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;
updated = r_modification_order(curr, promise);
mo_graph->commitChanges();
break;
-template <typename T>
-bool ModelChecker::should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const
+template <typename T, typename U>
+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))
{
/* Need a different write/promise */
if (other_rf->equals(rf))
* If so, we decide that the execution is no longer feasible.
*
* @param curr The current action. Must be a read.
* 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
*/
* @return True if the read should succeed; false otherwise
*/
-bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const
+template <typename T>
+bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
{
if (!params.maxreads)
return true;
{
if (!params.maxreads)
return true;
Thread * take_step(ModelAction *curr);
Thread * take_step(ModelAction *curr);
- bool check_recency(ModelAction *curr, const ModelAction *rf) const;
-
- 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 <typename T, typename U>
+ 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;
ModelAction * get_last_fence_conflict(ModelAction *act) const;
ModelAction * get_last_conflict(ModelAction *act) const;