SC Reads can read from things mo'd before the last sc write, they just can't happen...

[model-checker.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 3a630d777f060cb22598858278044d6e140cfed3..2a7e0dadd1e0918ac21b5f43dd4e3608935b8f18 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -34,6 +34,7 @@ struct model_snapshot_members {
                too_many_reads(false),
                no_valid_reads(false),
                bad_synchronization(false),
+               bad_sc_read(false),
                asserted(false)
        { }
 
@@ -53,6 +54,7 @@ struct model_snapshot_members {
        bool no_valid_reads;
        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;
+       bool bad_sc_read;
        bool asserted;
 
        SNAPSHOTALLOC
@@ -202,6 +204,13 @@ void ModelExecution::set_bad_synchronization()
        priv->bad_synchronization = true;
 }
 
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelExecution::set_bad_sc_read()
+{
+       priv->bad_sc_read = true;
+}
+
 bool ModelExecution::assert_bug(const char *msg)
 {
        priv->bugs.push_back(new bug_message(msg));
@@ -1306,6 +1315,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                                if (rf) {
                                        if (r_modification_order(act, rf))
                                                updated = true;
+                                       if (act->is_seqcst()) {
+                                               ModelAction *last_sc_write = get_last_seq_cst_write(act);
+                                               if (last_sc_write != NULL && rf->happens_before(last_sc_write)) {
+                                                       set_bad_sc_read();
+                                               }
+                                       }
                                } else if (promise) {
                                        if (r_modification_order(act, promise))
                                                updated = true;
@@ -1385,6 +1400,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const
                ptr += sprintf(ptr, "[no valid reads-from]");
        if (priv->bad_synchronization)
                ptr += sprintf(ptr, "[bad sw ordering]");
+       if (priv->bad_sc_read)
+               ptr += sprintf(ptr, "[bad sc read]");
        if (promises_expired())
                ptr += sprintf(ptr, "[promise expired]");
        if (promises.size() != 0)
@@ -1415,6 +1432,7 @@ bool ModelExecution::is_infeasible() const
                priv->no_valid_reads ||
                priv->too_many_reads ||
                priv->bad_synchronization ||
+               priv->bad_sc_read ||
                priv->hard_failed_promise ||
                promises_expired();
 }
@@ -1616,12 +1634,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
                                }
                        }
 
-                       /* C++, Section 29.3 statement 3 (second subpoint) */
-                       if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
-                               added = mo_graph->addEdge(act, rf) || added;
-                               break;
-                       }
-
                        /*
                         * Include at most one act per-thread that "happens
                         * before" curr
@@ -1753,9 +1765,10 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAc
                                        added = mo_graph->addEdge(act, curr) || added;
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
-                                       if (act->get_reads_from() == NULL)
-                                               continue;
-                                       added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
+                                       if (act->get_reads_from() == NULL) {
+                                               added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added;
+                                       } else
+                                               added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
                                }
                                break;
                        } else if (act->is_read() && !act->could_synchronize_with(curr) &&