promise: add 'same_value' helper, force value-checking in CycleGraph

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 38d63a2fcb9f0a45f850fc1b7bf718d1579bd234..7048096ca25e0cbe0ad9928504802de4231c5a18 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -483,8 +483,10 @@ void ModelChecker::record_stats()
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
-       else
+       else if (scheduler->all_threads_sleeping())
                stats.num_redundant++;
+       else
+               ASSERT(false);
 }
 
 /** @brief Print execution stats */
@@ -1020,7 +1022,7 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
                        write_thread = write_thread->get_parent();
 
                struct future_value fv = {
-                       writer->get_value(),
+                       writer->get_write_value(),
                        writer->get_seq_number() + params.maxfuturedelay,
                        write_thread->get_id(),
                };
@@ -1322,8 +1324,9 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
  */
 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 {
+       ASSERT(rf);
        act->set_read_from(rf);
-       if (rf != NULL && act->is_acquire()) {
+       if (act->is_acquire()) {
                rel_heads_list_t release_heads;
                get_release_seq_heads(act, act, &release_heads);
                int num_heads = release_heads.size();
@@ -2502,7 +2505,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
 {
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
-               if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value())
+               if (!promise->is_compatible(curr) || !promise->same_value(curr))
                        continue;
 
                bool satisfy = true;
@@ -2573,7 +2576,7 @@ void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
                Promise *promise = (*promises)[i];
 
                // Is this promise on the same location?
-               if (promise->get_value() != write->get_value())
+               if (!promise->same_location(write))
                        continue;
 
                for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
@@ -2762,17 +2765,28 @@ void ModelChecker::dumpGraph(char *filename) const
        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;
-               if (action->is_read()) {
-                       fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
-                       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());
+               ModelAction *act = *it;
+               if (act->is_read()) {
+                       mo_graph->dot_print_node(file, act);
+                       if (act->get_reads_from())
+                               mo_graph->dot_print_edge(file,
+                                               act->get_reads_from(),
+                                               act,
+                                               "label=\"rf\", color=red, weight=2");
+                       else
+                               mo_graph->dot_print_edge(file,
+                                               act->get_reads_from_promise(),
+                                               act,
+                                               "label=\"rf\", color=red");
                }
-               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());
+               if (thread_array[act->get_tid()]) {
+                       mo_graph->dot_print_edge(file,
+                                       thread_array[id_to_int(act->get_tid())],
+                                       act,
+                                       "label=\"sb\", color=blue, weight=400");
                }
 
-               thread_array[action->get_tid()] = action;
+               thread_array[act->get_tid()] = act;
        }
        fprintf(file, "}\n");
        model_free(thread_array);
@@ -2792,9 +2806,11 @@ void ModelChecker::print_summary() const
 #endif
 
        model_print("Execution %d:", stats.num_total);
-       if (isfeasibleprefix())
+       if (isfeasibleprefix()) {
+               if (scheduler->all_threads_sleeping())
+                       model_print(" SLEEP-SET REDUNDANT");
                model_print("\n");
-       else
+       } else
                print_infeasibility(" INFEASIBLE");
        print_list(action_trace);
        model_print("\n");
@@ -2840,6 +2856,26 @@ Thread * ModelChecker::get_thread(const ModelAction *act) const
        return get_thread(act->get_tid());
 }
 
+/**
+ * @brief Get a Promise's "promise number"
+ *
+ * A "promise number" is an index number that is unique to a promise, valid
+ * only for a specific snapshot of an execution trace. Promises may come and go
+ * as they are generated an resolved, so an index only retains meaning for the
+ * current snapshot.
+ *
+ * @param promise The Promise to check
+ * @return The promise index, if the promise still is valid; otherwise -1
+ */
+int ModelChecker::get_promise_number(const Promise *promise) const
+{
+       for (unsigned int i = 0; i < promises->size(); i++)
+               if ((*promises)[i] == promise)
+                       return i;
+       /* Not found */
+       return -1;
+}
+
 /**
  * @brief Check if a Thread is currently enabled
  * @param t The Thread to check