model: add 'set_latest_backtrack()'
[model-checker.git] / model.cc
index e4b6431336050c89043f45851214c632b2e943ce..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;
@@ -228,7 +226,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 
        if (next == diverge) {
                if (earliest_diverge == NULL || *diverge < *earliest_diverge)
-                       earliest_diverge=diverge;
+                       earliest_diverge = diverge;
 
                Node *nextnode = next->get_node();
                Node *prevnode = nextnode->get_parent();
@@ -261,8 +259,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        tid = prevnode->get_next_backtrack();
                        /* Make sure the backtracked thread isn't sleeping. */
                        node_stack->pop_restofstack(1);
-                       if (diverge==earliest_diverge) {
-                               earliest_diverge=prevnode->get_action();
+                       if (diverge == earliest_diverge) {
+                               earliest_diverge = prevnode->get_action();
                        }
                }
                /* The correct sleep set is in the parent node. */
@@ -298,7 +296,6 @@ void ModelChecker::execute_sleep_set()
                        thr->set_pending(priv->current_action);
                }
        }
-       priv->current_action = NULL;
 }
 
 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
@@ -502,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();
@@ -614,7 +611,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
        int low_tid, high_tid;
        if (node->is_enabled(t)) {
                low_tid = id_to_int(act->get_tid());
-               high_tid = low_tid+1;
+               high_tid = low_tid + 1;
        } else {
                low_tid = 0;
                high_tid = get_num_threads();
@@ -628,7 +625,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
                        break;
 
                /* Don't backtrack into a point where the thread is disabled or sleeping. */
-               if (node->enabled_status(tid)!=THREAD_ENABLED)
+               if (node->enabled_status(tid) != THREAD_ENABLED)
                        continue;
 
                /* Check if this has been explored already */
@@ -637,11 +634,11 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
                /* See if fairness allows */
                if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
-                       bool unfair=false;
-                       for(int t=0;t<node->get_num_threads();t++) {
-                               thread_id_t tother=int_to_id(t);
+                       bool unfair = false;
+                       for (int t = 0; t < node->get_num_threads(); t++) {
+                               thread_id_t tother = int_to_id(t);
                                if (node->is_enabled(tother) && node->has_priority(tother)) {
-                                       unfair=true;
+                                       unfair = true;
                                        break;
                                }
                        }
@@ -649,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))
@@ -665,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.
@@ -741,9 +757,10 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
  *
  * @return True if synchronization was updated; false otherwise
  */
-bool ModelChecker::process_mutex(ModelAction *curr) {
-       std::mutex *mutex=NULL;
-       struct std::mutex_state *state=NULL;
+bool ModelChecker::process_mutex(ModelAction *curr)
+{
+       std::mutex *mutex = NULL;
+       struct std::mutex_state *state = NULL;
 
        if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
                mutex = (std::mutex *)curr->get_location();
@@ -799,7 +816,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
                }
                waiters->clear();
                //check whether we should go to sleep or not...simulate spurious failures
-               if (curr->get_node()->get_misc()==0) {
+               if (curr->get_node()->get_misc() == 0) {
                        get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
                        //disable us
                        scheduler->sleep(get_current_thread());
@@ -817,7 +834,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
        }
        case ATOMIC_NOTIFY_ONE: {
                action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
-               int wakeupthread=curr->get_node()->get_misc();
+               int wakeupthread = curr->get_node()->get_misc();
                action_list_t::iterator it = waiters->begin();
                advance(it, wakeupthread);
                scheduler->wake(get_thread(*it));
@@ -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,25 +1295,22 @@ 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);
        }
 }
 
 bool ModelChecker::promises_expired() const
 {
-       for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
-               Promise *promise = (*promises)[promise_index];
-               if (promise->get_expiration()<priv->used_sequence_numbers) {
+       for (unsigned int i = 0; i < promises->size(); i++) {
+               Promise *promise = (*promises)[i];
+               if (promise->get_expiration() < priv->used_sequence_numbers)
                        return true;
-               }
        }
        return false;
 }
@@ -1369,7 +1382,7 @@ bool ModelChecker::is_infeasible_ignoreRMW() const
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
        ModelAction *lastread = get_last_action(act->get_tid());
        lastread->process_rmw(act);
-       if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
+       if (act->is_rmw() && lastread->get_reads_from() != NULL) {
                mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
                mo_graph->commitChanges();
        }
@@ -1451,7 +1464,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
                                ModelAction *act = *rit;
                                bool foundvalue = false;
                                for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
-                                       if (act->get_node()->get_read_from_at(j)==write) {
+                                       if (act->get_node()->get_read_from_at(j) == write) {
                                                foundvalue = true;
                                                break;
                                        }
@@ -1606,7 +1619,7 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
 
                        /* Include at most one act per-thread that "happens before" curr */
                if (lastact != NULL) {
-                       if (lastact==curr) {
+                       if (lastact== curr) {
                                //Case 1: The resolved read is a RMW, and we need to make sure
                                //that the write portion of the RMW mod order after rf
 
@@ -1617,13 +1630,13 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
                                //is mod ordered after rf
 
                                const ModelAction *postreadfrom = lastact->get_reads_from();
-                               if (postreadfrom != NULL&&rf != postreadfrom)
+                               if (postreadfrom != NULL && rf != postreadfrom)
                                        mo_graph->addEdge(rf, postreadfrom);
                        } else {
                                //Case 3: The resolved read is a normal read and the next
                                //operation is a write, and we need to make sure that the
                                //write is mod ordered after rf
-                               if (lastact!=rf)
+                               if (lastact != rf)
                                        mo_graph->addEdge(rf, lastact);
                        }
                        break;
@@ -1698,7 +1711,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                 * continue processing list.
                                 */
                                if (curr->is_rmw()) {
-                                       if (curr->get_reads_from()!=NULL)
+                                       if (curr->get_reads_from() != NULL)
                                                break;
                                        else
                                                continue;
@@ -1806,16 +1819,16 @@ 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))
+               if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
                        return false;
        }
        return true;
@@ -2141,7 +2154,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        }
 
        if (act->is_wait()) {
-               void *mutex_loc=(void *) act->get_value();
+               void *mutex_loc = (void *) act->get_value();
                get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
 
                std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
@@ -2306,7 +2319,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
        //Check whether reading these writes has made threads unable to
        //resolve promises
 
-       for(unsigned int i=0;i<threads_to_check.size();i++)
+       for (unsigned int i = 0; i < threads_to_check.size(); i++)
                mo_check_promises(threads_to_check[i], write);
 
        return resolved;
@@ -2399,7 +2412,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
                        continue;
 
                //same thread as the promise
-               if ( act->get_tid()==tid ) {
+               if ( act->get_tid() == tid ) {
 
                        //do we have a pwrite for the promise, if not, set it
                        if (promise->get_write() == NULL ) {
@@ -2530,7 +2543,7 @@ bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *wri
                }
                if (write->get_reads_from() == NULL)
                        return true;
-               write=write->get_reads_from();
+               write = write->get_reads_from();
        }
 }
 
@@ -2555,37 +2568,38 @@ static void print_list(action_list_t *list, int exec_num = -1)
        if (exec_num >= 0)
                model_print("Execution %d:\n", exec_num);
 
-       unsigned int hash=0;
+       unsigned int hash = 0;
 
        for (it = list->begin(); it != list->end(); it++) {
                (*it)->print();
-               hash=hash^(hash<<3)^((*it)->hash());
+               hash = hash^(hash<<3)^((*it)->hash());
        }
        model_print("HASH %u\n", hash);
        model_print("---------------------------------------------------------------------\n");
 }
 
 #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");
+       FILE *file = fopen(buffer, "w");
        fprintf(file, "digraph %s {\n",filename);
        mo_graph->dumpNodes(file);
-       ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
+       ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
 
        for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
-               ModelAction *action=*it;
+               ModelAction *action = *it;
                if (action->is_read()) {
                        fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
-                       if (action->get_reads_from()!=NULL)
+                       if (action->get_reads_from() != NULL)
                                fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
                }
                if (thread_array[action->get_tid()] != NULL) {
                        fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
                }
 
-               thread_array[action->get_tid()]=action;
+               thread_array[action->get_tid()] = action;
        }
        fprintf(file,"}\n");
        model_free(thread_array);
@@ -2680,40 +2694,40 @@ bool ModelChecker::is_enabled(thread_id_t tid) const
  * @param act The current action that will be explored. May be NULL only if
  * trace is exiting via an assertion (see ModelChecker::set_assert and
  * ModelChecker::has_asserted).
- * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
+ * @return Return the value returned by the current action
  */
-int ModelChecker::switch_to_master(ModelAction *act)
+uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
        DBG();
        Thread *old = thread_current();
        set_current_action(act);
        old->set_state(THREAD_READY);
-       return Thread::swap(old, &system_context);
+       if (Thread::swap(old, &system_context) < 0) {
+               perror("swap threads");
+               exit(EXIT_FAILURE);
+       }
+       return old->get_return_value();
 }
 
 /**
  * Takes the next step in the execution, if possible.
+ * @param curr The current step to take
  * @return Returns true (success) if a step was taken and false otherwise.
  */
-bool ModelChecker::take_step() {
+bool ModelChecker::take_step(ModelAction *curr)
+{
        if (has_asserted())
                return false;
 
-       Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
-       if (curr) {
-               if (curr->get_state() == THREAD_READY) {
-                       ASSERT(priv->current_action);
+       Thread *curr_thrd = get_thread(curr);
+       ASSERT(curr_thrd->get_state() == THREAD_READY);
 
-                       priv->nextThread = check_current_action(priv->current_action);
-                       priv->current_action = NULL;
+       Thread *next_thrd = check_current_action(curr);
 
-                       if (curr->is_blocked() || curr->is_complete())
-                               scheduler->remove_thread(curr);
-               } else {
-                       ASSERT(false);
-               }
-       }
-       Thread *next = scheduler->next_thread(priv->nextThread);
+       if (curr_thrd->is_blocked() || curr_thrd->is_complete())
+               scheduler->remove_thread(curr_thrd);
+
+       next_thrd = scheduler->next_thread(next_thrd);
 
        /* Infeasible -> don't take any more steps */
        if (is_infeasible())
@@ -2729,8 +2743,8 @@ bool ModelChecker::take_step() {
                }
        }
 
-       DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
-                       next ? id_to_int(next->get_id()) : -1);
+       DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
+                       next_thrd ? id_to_int(next_thrd->get_id()) : -1);
 
        /*
         * Launch end-of-execution release sequence fixups only when there are:
@@ -2741,7 +2755,7 @@ bool ModelChecker::take_step() {
         * (3) pending assertions (i.e., data races)
         * (4) no pending promises
         */
-       if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
+       if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
                        is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
                model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
                                pending_rel_seqs->size());
@@ -2752,22 +2766,22 @@ bool ModelChecker::take_step() {
                return true;
        }
 
-       /* next == NULL -> don't take any more steps */
-       if (!next)
+       /* next_thrd == NULL -> don't take any more steps */
+       if (!next_thrd)
                return false;
 
-       next->set_state(THREAD_RUNNING);
+       next_thrd->set_state(THREAD_RUNNING);
 
-       if (next->get_pending() != NULL) {
+       if (next_thrd->get_pending() != NULL) {
                /* restart a pending action */
-               set_current_action(next->get_pending());
-               next->set_pending(NULL);
-               next->set_state(THREAD_READY);
+               set_current_action(next_thrd->get_pending());
+               next_thrd->set_pending(NULL);
+               next_thrd->set_state(THREAD_READY);
                return true;
        }
 
        /* Return false only if swap fails with an error */
-       return (Thread::swap(&system_context, next) == 0);
+       return (Thread::swap(&system_context, next_thrd) == 0);
 }
 
 /** Wrapper to run the user's main function, with appropriate arguments */
@@ -2781,12 +2795,16 @@ void ModelChecker::run()
 {
        do {
                thrd_t user_thread;
+               Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
+
+               add_thread(t);
 
-               /* Start user program */
-               add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
+               /* Run user thread up to its first action */
+               scheduler->next_thread(t);
+               Thread::swap(&system_context, t);
 
                /* Wait for all threads to complete */
-               while (take_step());
+               while (take_step(priv->current_action));
        } while (next_execution());
 
        print_stats();