From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 14 Sep 2012 08:31:09 +0000 (-0700)
Subject: (1) add actions for the fence
X-Git-Tag: pldi2013~195
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=5485feb8f53f4fe816b08d854fc3e82b00c33b0b

(1) add actions for the fence
(2) a little more support for cyclegraph -- show rmw edges
(3) add extra documentation for norris
---

diff --git a/action.cc b/action.cc
index 5d726a2..1e28264 100644
--- a/action.cc
+++ b/action.cc
@@ -52,6 +52,11 @@ bool ModelAction::is_rmwc() const
 	return type == ATOMIC_RMWC;
 }
 
+bool ModelAction::is_fence() const 
+{
+	return type == ATOMIC_FENCE;
+}
+
 bool ModelAction::is_initialization() const
 {
 	return type == ATOMIC_INIT;
@@ -230,6 +235,9 @@ void ModelAction::print(void) const
 	case ATOMIC_RMW:
 		type_str = "atomic rmw";
 		break;
+	case ATOMIC_FENCE:
+		type_str = "fence";
+		break;
 	case ATOMIC_RMWR:
 		type_str = "atomic rmwr";
 		break;
diff --git a/action.h b/action.h
index 3e590aa..12771f2 100644
--- a/action.h
+++ b/action.h
@@ -38,8 +38,9 @@ typedef enum action_type {
 	ATOMIC_RMWR,          /**< The read part of an atomic RMW action */
 	ATOMIC_RMW,           /**< The write part of an atomic RMW action */
 	ATOMIC_RMWC,          /**< Convert an atomic RMW action into a READ */
-	ATOMIC_INIT           /**< Initialization of an atomic object (e.g.,
+	ATOMIC_INIT,          /**< Initialization of an atomic object (e.g.,
 	                       *   atomic_init()) */
+	ATOMIC_FENCE
 } action_type_t;
 
 /* Forward declaration */
@@ -71,6 +72,7 @@ public:
 	bool is_rmwr() const;
 	bool is_rmwc() const;
 	bool is_rmw() const;
+  bool is_fence() const;
 	bool is_initialization() const;
 	bool is_acquire() const;
 	bool is_release() const;
diff --git a/cmodelint.cc b/cmodelint.cc
index 8919041..228c40f 100644
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -36,3 +36,8 @@ void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
 void model_rmwc_action(void *obj, memory_order ord) {
 	model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
 }
+
+/** Issues a fence operation. */
+void model_fence_action(memory_order ord) {
+	model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, NULL));
+}
diff --git a/cmodelint.h b/cmodelint.h
index c23c061..232648c 100644
--- a/cmodelint.h
+++ b/cmodelint.h
@@ -17,6 +17,7 @@ void model_init_action(void * obj, uint64_t val);
 uint64_t model_rmwr_action(void *obj, memory_order ord);
 void model_rmw_action(void *obj, memory_order ord, uint64_t val);
 void model_rmwc_action(void *obj, memory_order ord);
+void model_fence_action(memory_order ord);
 
 
 #if __cplusplus
diff --git a/config.h b/config.h
index ab54e3a..16a41d7 100644
--- a/config.h
+++ b/config.h
@@ -13,7 +13,7 @@
 
 /** Turn on support for dumping cyclegraphs as dot files at each
  *  printed summary.*/
-#define SUPPORT_MOD_ORDER_DUMP 0
+#define SUPPORT_MOD_ORDER_DUMP 1
 
 /** Do we have a 48 bit virtual address (64 bit machine) or 32 bit addresses.
  * Set to 1 for 48-bit, 0 for 32-bit. */
diff --git a/cyclegraph.cc b/cyclegraph.cc
index c7bb69b..ecf8a78 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -130,6 +130,9 @@ void CycleGraph::dumpGraphToFile(const char *filename) {
 		std::vector<CycleNode *> * edges=cn->getEdges();
 		const ModelAction *action=cn->getAction();
 		fprintf(file, "N%u [label=\"%u, T%u\"];\n",action->get_seq_number(),action->get_seq_number(), action->get_tid());
+		if (cn->getRMW()!=NULL) {
+			fprintf(file, "N%u -> N%u[style=dotted];\n", action->get_seq_number(), cn->getRMW()->getAction()->get_seq_number());
+		}
 		for(unsigned int j=0;j<edges->size();j++) {
 		  CycleNode *dst=(*edges)[j];
 			const ModelAction *dstaction=dst->getAction();
diff --git a/include/impatomic.h b/include/impatomic.h
index a69ba78..2fde095 100644
--- a/include/impatomic.h
+++ b/include/impatomic.h
@@ -110,10 +110,9 @@ inline void atomic_flag::fence( memory_order __x__ ) const volatile
                 else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
                 __r__; })
 
-//TODO
 #define _ATOMIC_FENCE_( __a__, __x__ ) \
-({ ;})
-
+	({ model_fence_action(__x__);})
+ 
 
 #define ATOMIC_CHAR_LOCK_FREE 1
 #define ATOMIC_CHAR16_T_LOCK_FREE 1
diff --git a/model.cc b/model.cc
index 1712a60..096ebe4 100644
--- a/model.cc
+++ b/model.cc
@@ -586,7 +586,18 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
 }
 
 /**
- * Updates the mo_graph with the constraints imposed from the current read.
+ * Updates the mo_graph with the constraints imposed from the current
+ * read.  
+ *
+ * Basic idea is the following: Go through each other thread and find
+ * the lastest action that happened before our read.  Two cases:
+ *
+ * (1) The action is a write => that write must either occur before
+ * the write we read from or be the write we read from.
+ *
+ * (2) The action is a read => the write that that action read from
+ * must occur before the write we read from or be the same write.
+ *
  * @param curr The current action. Must be a read.
  * @param rf The action that curr reads from. Must be a write.
  * @return True if modification order edges were added; false otherwise
@@ -629,7 +640,22 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 	return added;
 }
 
-/** Updates the mo_graph with the constraints imposed from the current read. */
+/** This method fixes up the modification order when we resolve a
+ *  promises.  The basic problem is that actions that occur after the
+ *  read curr could not property add items to the modification order
+ *  for our read.
+ *  
+ *  So for each thread, we find the earliest item that happens after
+ *  the read curr.  This is the item we have to fix up with additional
+ *  constraints.  If that action is write, we add a MO edge between
+ *  the Action rf and that action.  If the action is a read, we add a
+ *  MO edge between the Action rf, and whatever the read accessed.
+ *
+ * @param curr is the read ModelAction that we are fixing up MO edges for.
+ * @param rf is the write ModelAction that curr reads from.
+ *
+ */
+
 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
 {
 	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
@@ -668,6 +694,23 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
 
 /**
  * Updates the mo_graph with the constraints imposed from the current write.
+ *
+ * Basic idea is the following: Go through each other thread and find
+ * the lastest action that happened before our write.  Two cases:
+ *
+ * (1) The action is a write => that write must occur before
+ * the current write
+ *
+ * (2) The action is a read => the write that that action read from
+ * must occur before the current write.
+ *
+ * This method also handles two other issues:
+ *
+ * (I) Sequential Consistency: Making sure that if the current write is
+ * seq_cst, that it occurs after the previous seq_cst write.
+ *
+ * (II) Sending the write back to non-synchronizing reads.
+ *
  * @param curr The current action. Must be a write.
  * @return True if modification order edges were added; false otherwise
  */
@@ -1043,7 +1086,11 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			if (read->is_rmw()) {
 				mo_graph->addRMWEdge(write, read);
 			}
+			//First fix up the modification order for actions that happened
+			//before the read
 			r_modification_order(read, write);
+			//Next fix up the modification order for actions that happened
+			//after the read.
 			post_r_modification_order(read, write);
 			promises->erase(promises->begin() + promise_index);
 			resolved = true;