model: add 'set_latest_backtrack()'

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index a5668312a9a6e5fd4abe609b594d08bf17a083ae..d6b84c3ef457ddbaf3c6838d1efe243487f24d16 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -43,7 +43,6 @@ struct model_snapshot_members {
                /* First thread created will have id INITIAL_THREAD_ID */
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),
-               nextThread(NULL),
                next_backtrack(NULL),
                bugs(),
                stats(),
@@ -62,7 +61,6 @@ struct model_snapshot_members {
        ModelAction *current_action;
        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
-       Thread *nextThread;
        ModelAction *next_backtrack;
        std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
        struct execution_stats stats;
@@ -501,7 +499,7 @@ bool ModelChecker::next_execution()
        record_stats();
 
        /* Output */
-       if (DBG_ENABLED() || params.verbose || have_bug_reports())
+       if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
                print_execution(complete);
        else
                clear_program_output();
@@ -648,8 +646,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
                                continue;
                }
                /* Cache the latest backtracking point */
-               if (!priv->next_backtrack || *prev > *priv->next_backtrack)
-                       priv->next_backtrack = prev;
+               set_latest_backtrack(prev);
 
                /* If this is a new backtracking point, mark the tree */
                if (!node->set_backtrack(tid))
@@ -664,6 +661,26 @@ void ModelChecker::set_backtracking(ModelAction *act)
        }
 }
 
+/**
+ * @brief Cache the a backtracking point as the "most recent", if eligible
+ *
+ * Note that this does not prepare the NodeStack for this backtracking
+ * operation, it only caches the action on a per-execution basis
+ *
+ * @param act The operation at which we should explore a different next action
+ * (i.e., backtracking point)
+ * @return True, if this action is now the most recent backtracking point;
+ * false otherwise
+ */
+bool ModelChecker::set_latest_backtrack(ModelAction *act)
+{
+       if (!priv->next_backtrack || *act > *priv->next_backtrack) {
+               priv->next_backtrack = act;
+               return true;
+       }
+       return false;
+}
+
 /**
  * Returns last backtracking point. The model checker will explore a different
  * path for this point in the next execution.
@@ -845,10 +862,9 @@ bool ModelChecker::process_write(ModelAction *curr)
                for (unsigned int i = 0; i < futurevalues->size(); i++) {
                        struct PendingFutureValue pfv = (*futurevalues)[i];
                        //Do more ambitious checks now that mo is more complete
-                       if (mo_may_allow(pfv.writer, pfv.act)&&
-                                       pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
-                                       (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
-                               priv->next_backtrack = pfv.act;
+                       if (mo_may_allow(pfv.writer, pfv.act) &&
+                                       pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
+                               set_latest_backtrack(pfv.act);
                }
                futurevalues->resize(0);
        }
@@ -1279,15 +1295,13 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
 
-       if ((!parnode->backtrack_empty() ||
+       if (!parnode->backtrack_empty() ||
                         !currnode->misc_empty() ||
                         !currnode->read_from_empty() ||
                         !currnode->future_value_empty() ||
                         !currnode->promise_empty() ||
-                        !currnode->relseq_break_empty())
-                       && (!priv->next_backtrack ||
-                                       *curr > *priv->next_backtrack)) {
-               priv->next_backtrack = curr;
+                        !currnode->relseq_break_empty()) {
+               set_latest_backtrack(curr);
        }
 }
 
@@ -1805,13 +1819,13 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 
-                       if (!reader->happens_before(act))
+                       /* Don't disallow due to act == reader */
+                       if (!reader->happens_before(act) || reader == act)
                                break;
                        else if (act->is_write())
                                write_after_read = act;
-                       else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
+                       else if (act->is_read() && act->get_reads_from() != NULL)
                                write_after_read = act->get_reads_from();
-                       }
                }
 
                if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
@@ -2565,7 +2579,8 @@ static void print_list(action_list_t *list, int exec_num = -1)
 }
 
 #if SUPPORT_MOD_ORDER_DUMP
-void ModelChecker::dumpGraph(char *filename) {
+void ModelChecker::dumpGraph(char *filename) const
+{
        char buffer[200];
        sprintf(buffer, "%s.dot",filename);
        FILE *file = fopen(buffer, "w");
@@ -2707,12 +2722,12 @@ bool ModelChecker::take_step(ModelAction *curr)
        Thread *curr_thrd = get_thread(curr);
        ASSERT(curr_thrd->get_state() == THREAD_READY);
 
-       priv->nextThread = check_current_action(curr);
+       Thread *next_thrd = check_current_action(curr);
 
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())
                scheduler->remove_thread(curr_thrd);
 
-       Thread *next_thrd = scheduler->next_thread(priv->nextThread);
+       next_thrd = scheduler->next_thread(next_thrd);
 
        /* Infeasible -> don't take any more steps */
        if (is_infeasible())