1) Add more comments.
authorBrian Demsky <bdemsky@uci.edu>
Wed, 6 Jun 2012 08:46:49 +0000 (01:46 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Wed, 6 Jun 2012 08:46:49 +0000 (01:46 -0700)
2) Change is_dependent to is_synchronizing and make it capture actual synchronizing behavior...
3) Add more support for RMW operations.

12 files changed:
action.cc
action.h
clockvector.h
common.h
libatomic.h
librace.h
libthreads.h
model.cc
model.h
nodestack.h
schedule.h
threads.h

index ec50807..6ae1d86 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;
 }
 
index 53107ea..bf5e6c3 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);
index eb70862..e9ffb2b 100644 (file)
@@ -1,3 +1,7 @@
+/** @file clockvector.h
+ *  @brief Implements a clock vector.
+ */
+
 #ifndef __CLOCKVECTOR_H__
 #define __CLOCKVECTOR_H__
 
index a950f79..0db1cfe 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__
 
index 1806f21..f24b5fb 100644 (file)
@@ -1,3 +1,7 @@
+/** @file libatomic.h
+ *  @brief Basic atomic operations to be exposed to user program.
+ */
+
 #ifndef __LIBATOMIC_H__
 #define __LIBATOMIC_H__
 
index a8af686..591b292 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__
 
index f6de95b..0c02971 100644 (file)
@@ -1,3 +1,7 @@
+/** @file libthreads.h
+ *  @brief Basic Thread Library Functionality.
+ */
+
 #ifndef __LIBTHREADS_H__
 #define __LIBTHREADS_H__
 
index 51891d0..3716d78 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 d89a8a2..0f93920 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__
 
index 59da8a1..d3eab13 100644 (file)
@@ -1,3 +1,7 @@
+/** @file nodestack.h
+ *  @brief Stack of operations for use in backtracking.
+*/
+
 #ifndef __NODESTACK_H__
 #define __NODESTACK_H__
 
index f496536..9b34e82 100644 (file)
@@ -1,3 +1,7 @@
+/** @file schedule.h
+ *     @brief Thread scheduler.
+ */
+
 #ifndef __SCHEDULE_H__
 #define __SCHEDULE_H__
 
index 7d2189b..0e0293a 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__