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

diff --git a/execution.cc b/execution.cc
index 01a5fa4..2a7e0da 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),
                too_many_reads(false),
                no_valid_reads(false),
                bad_synchronization(false),

+               bad_sc_read(false),

                asserted(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 no_valid_reads;
        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;

+       bool bad_sc_read;

        bool asserted;
 
        SNAPSHOTALLOC
        bool asserted;
 
        SNAPSHOTALLOC


@@ -202,6 +204,13 @@ void ModelExecution::set_bad_synchronization()
        priv->bad_synchronization = true;
 }
 
        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));
 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 (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;
                                } 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]");
                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)
        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->no_valid_reads ||
                priv->too_many_reads ||
                priv->bad_synchronization ||

+               priv->bad_sc_read ||

                priv->hard_failed_promise ||
                promises_expired();
 }
                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
                        /*
                         * Include at most one act per-thread that "happens
                         * before" curr

diff --git a/execution.h b/execution.h
index 2ca2513..3635657 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -132,6 +132,7 @@ private:
        bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
        bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        void set_bad_synchronization();
        bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
        bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        void set_bad_synchronization();

+       void set_bad_sc_read();

        bool promises_expired() const;
        bool should_wake_up(const ModelAction *curr, const Thread *thread) const;
        void wake_up_sleeping_actions(ModelAction *curr);
        bool promises_expired() const;
        bool should_wake_up(const ModelAction *curr, const Thread *thread) const;
        void wake_up_sleeping_actions(ModelAction *curr);