From 5485feb8f53f4fe816b08d854fc3e82b00c33b0b Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 14 Sep 2012 01:31:09 -0700
Subject: [PATCH] (1) add actions for the fence (2) a little more support for
cyclegraph -- show rmw edges (3) add extra documentation for norris
---
action.cc | 8 +++++++
action.h | 4 +++-
cmodelint.cc | 5 +++++
cmodelint.h | 1 +
config.h | 2 +-
cyclegraph.cc | 3 +++
include/impatomic.h | 5 ++---
model.cc | 51 +++++++++++++++++++++++++++++++++++++++++++--
8 files changed, 72 insertions(+), 7 deletions(-)
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;
--
2.34.1