From 6d7624344faab763eb30f3a6424f51538b7292a5 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 6 Jun 2012 01:46:49 -0700
Subject: [PATCH] 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.

---
 action.cc     | 43 ++++++++++++++++++++++++++++++++++++++-----
 action.h      |  8 +++++++-
 clockvector.h |  4 ++++
 common.h      |  4 ++++
 libatomic.h   |  4 ++++
 librace.h     |  4 ++++
 libthreads.h  |  4 ++++
 model.cc      |  2 +-
 model.h       |  4 ++++
 nodestack.h   |  4 ++++
 schedule.h    |  4 ++++
 threads.h     |  4 ++++
 12 files changed, 82 insertions(+), 7 deletions(-)

diff --git a/action.cc b/action.cc
index ec508074..6ae1d861 100644
--- 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 53107ea8..bf5e6c35 100644
--- 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 eb708625..e9ffb2bf 100644
--- 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 a950f791..0db1cfe1 100644
--- 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 1806f219..f24b5fbf 100644
--- 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 a8af6864..591b2925 100644
--- 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 f6de95bb..0c029713 100644
--- 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 51891d08..3716d788 100644
--- 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 d89a8a2b..0f93920f 100644
--- 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 59da8a1f..d3eab135 100644
--- 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 f4965369..9b34e828 100644
--- 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 7d2189b4..0e0293ad 100644
--- a/threads.h
+++ b/threads.h
@@ -1,3 +1,7 @@
+/** @file threads.h
+ *  @brief Model Checker Thread class.
+ */
+
 #ifndef __THREADS_H__
 #define __THREADS_H__
 
-- 
2.34.1