(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 5d726a2a0514f1c63c66fc3604ec8409fe0ba8cb..1e28264fbcedf171c673bace33be6f41c3aa3f35 100644 (file)
--- 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 3e590aae7f34a115cefb9fafed941a91d3bc5f92..12771f2bed8c73f926d5d4906fa18beb531207d3 100644 (file)
--- 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 8919041be4589670d228ad3e3e7b00b7132a5f2b..228c40f9ec8d02b1a7b9c599a6cf69fc1c4ebf78 100644 (file)
--- 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 c23c061221c7dfc3f8254fa99acacc3eb3c539b8..232648cd588ef8c4c69a752b3899d5a1572b510e 100644 (file)
--- 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 ab54e3abe68e12e8199976dfb415d188dff54258..16a41d7a1f49ede60cbdc3ac94d09ccfa30c7581 100644 (file)
--- 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 c7bb69b990d801dc026765420e918e35a31f1b0d..ecf8a781c2770ebd09766cff47030e3e094bd2d7 100644 (file)
--- 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 a69ba7860342ed34568a00930ed6b451a8663cee..2fde095ee67e6ce5498c4a8dd61d62c0779f2fec 100644 (file)
--- 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 1712a60a9dd3990efeef26f257467f5bff7d6bb0..096ebe450e5db5221afe80f55ae0aa498da2021e 100644 (file)
--- 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;