1) Add more comments.

2) Change is_dependent to is_synchronizing and make it capture actual synchronizing behavior...
3) Add more support for RMW operations.

diff --git a/action.cc b/action.cc
index ec50807422cc4a8e6c9864e65c561896df579000..6ae1d861150151133b7b878525705aac9fa5e910 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -36,6 +36,11 @@ bool ModelAction::is_write()
        return type == ATOMIC_WRITE;
 }
 
+bool ModelAction::is_rmw()
+{
+       return type == ATOMIC_RMW;
+}
+
 bool ModelAction::is_acquire()
 {
        switch (order) {
@@ -60,6 +65,11 @@ bool ModelAction::is_release()
        }
 }
 
+bool ModelAction::is_seqcst()
+{
+       return order==memory_order_seq_cst;
+}
+
 bool ModelAction::same_var(ModelAction *act)
 {
        return location == act->location;
@@ -70,15 +80,38 @@ bool ModelAction::same_thread(ModelAction *act)
        return tid == act->tid;
 }
 
-bool ModelAction::is_dependent(ModelAction *act)
+/** The is_synchronizing method should only explore interleavings if:
+ *  (1) the operations are seq_cst and don't commute or
+ *  (2) the reordering may establish or break a synchronization relation.
+ *  Other memory operations will be dealt with by using the reads_from
+ *  relation.
+ *
+ *  @param act is the action to consider exploring a reordering.
+ *  @return tells whether we have to explore a reordering.
+ */
+
+bool ModelAction::is_synchronizing(ModelAction *act)
 {
-       if (!is_read() && !is_write())
+       //Same thread can't be reordered
+       if (same_thread(act))
                return false;
-       if (!act->is_read() && !act->is_write())
+
+       // Different locations commute
+       if (!same_var(act))
                return false;
-       if (same_var(act) && !same_thread(act) &&
-                       (is_write() || act->is_write()))
+       
+       // Explore interleavings of seqcst writes to guarantee total order
+       // of seq_cst operations that don't commute
+       if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst())
+               return true;
+
+       // Explore synchronizing read/write pairs
+       if (is_read() && is_acquire() && act->is_write() && act->is_release())
                return true;
+       if (is_write() && is_release() && act->is_read() && act->is_acquire())
+               return true;
+
+       // Otherwise handle by reads_from relation
        return false;
 }
 

diff --git a/action.h b/action.h
index 53107ea81762d33ab6a63ef2fa7e69176b379b1c..bf5e6c35476693808b301ec6b4f5b9879e39214b 100644 (file)
--- a/action.h
+++ b/action.h
@@ -1,3 +1,7 @@
+/** @file action.h
+ *  @brief Models actions taken by threads.
+ */
+
 #ifndef __ACTION_H__
 #define __ACTION_H__
 
@@ -42,11 +46,13 @@ public:
 
        bool is_read();
        bool is_write();
+       bool is_rmw();
        bool is_acquire();
        bool is_release();
+       bool is_seqcst();
        bool same_var(ModelAction *act);
        bool same_thread(ModelAction *act);
-       bool is_dependent(ModelAction *act);
+       bool is_synchronizing(ModelAction *act);
 
        void create_cv(ModelAction *parent = NULL);
        void read_from(ModelAction *act);

diff --git a/clockvector.h b/clockvector.h
index eb7086253d7f97e79b0f1d1ce41ef7b4e988e561..e9ffb2bf5c4997452bbddb0f8d650e319ce7f777 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -1,3 +1,7 @@
+/** @file clockvector.h
+ *  @brief Implements a clock vector.
+ */
+
 #ifndef __CLOCKVECTOR_H__
 #define __CLOCKVECTOR_H__
 

diff --git a/common.h b/common.h
index a950f79194c55d849fe82da5d18e35cef2675464..0db1cfe15f722dd8bd487aa98cdb3d16b7cfb79f 100644 (file)
--- a/common.h
+++ b/common.h
@@ -1,3 +1,7 @@
+/** @file common.h
+ *  @brief General purpose macros.
+ */
+
 #ifndef __COMMON_H__
 #define __COMMON_H__
 

diff --git a/libatomic.h b/libatomic.h
index 1806f21968b75405c1675a9456b4e79afa6f421f..f24b5fbff35a10a3dcc2c88beca108ecb9093e75 100644 (file)
--- a/libatomic.h
+++ b/libatomic.h
@@ -1,3 +1,7 @@
+/** @file libatomic.h
+ *  @brief Basic atomic operations to be exposed to user program.
+ */
+
 #ifndef __LIBATOMIC_H__
 #define __LIBATOMIC_H__
 

diff --git a/librace.h b/librace.h
index a8af6864da2e483a14a58f2571ae36d7a0b62319..591b2925473b9ef608d533d70f2b3d2cf6a928a6 100644 (file)
--- a/librace.h
+++ b/librace.h
@@ -1,3 +1,7 @@
+/** @file librace.h
+ *  @brief Interface to check normal memory operations for data races.
+ */
+
 #ifndef __LIBRACE_H__
 #define __LIBRACE_H__
 

diff --git a/libthreads.h b/libthreads.h
index f6de95bb9fa4f3614f07658b2abe05f8217ec6fa..0c02971342d06ffa903feb01b2d4daadc08754d4 100644 (file)
--- a/libthreads.h
+++ b/libthreads.h
@@ -1,3 +1,7 @@
+/** @file libthreads.h
+ *  @brief Basic Thread Library Functionality.
+ */
+
 #ifndef __LIBTHREADS_H__
 #define __LIBTHREADS_H__
 

diff --git a/model.cc b/model.cc
index 51891d08e09ddcb964b6dc7e95fb039680514ec1..3716d78838ba26ab694ef6faca6d66aa283b1b04 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -154,7 +154,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
        action_list_t::reverse_iterator rit;
        for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
                ModelAction *prev = *rit;
-               if (act->is_dependent(prev))
+               if (act->is_synchronizing(prev))
                        return prev;
        }
        return NULL;

diff --git a/model.h b/model.h
index d89a8a2b123b1743c58f3c5d7c883c87263b45b9..0f93920fc83bc5cb29ffc7da618923b8f5a266c9 100644 (file)
--- a/model.h
+++ b/model.h
@@ -1,3 +1,7 @@
+/** @file model.h
+ *  @brief Core model checker. 
+ */
+
 #ifndef __MODEL_H__
 #define __MODEL_H__
 

diff --git a/nodestack.h b/nodestack.h
index 59da8a1f1f04971f709cfe0dd7b79d187ed4593b..d3eab13561149cb6ca89da2d1928332ead695e4a 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -1,3 +1,7 @@
+/** @file nodestack.h
+ *  @brief Stack of operations for use in backtracking.
+*/
+
 #ifndef __NODESTACK_H__
 #define __NODESTACK_H__
 

diff --git a/schedule.h b/schedule.h
index f4965369b2a62be67a124ae29a44b4172c28f0eb..9b34e8287ba1c5dd22a71664eae83850bab5a208 100644 (file)
--- a/schedule.h
+++ b/schedule.h
@@ -1,3 +1,7 @@
+/** @file schedule.h
+ *     @brief Thread scheduler.
+ */
+
 #ifndef __SCHEDULE_H__
 #define __SCHEDULE_H__
 

diff --git a/threads.h b/threads.h
index 7d2189b49d9f098a775b1cc158390cf76f49cbf4..0e0293ad817332e867db1e7b92c490da3c3f9b19 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -1,3 +1,7 @@
+/** @file threads.h
+ *  @brief Model Checker Thread class.
+ */
+
 #ifndef __THREADS_H__
 #define __THREADS_H__