From c767868da49992a09ee482bbd666e080c6d43177 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 23 Aug 2012 17:47:31 -0700
Subject: [PATCH] model: report 'updates' when adding mo_graph edges
The rest of the model checker would like to know if any edges were added. Add a
boolean return value to report this.
---
model.cc | 24 ++++++++++++++++++++----
model.h | 4 ++--
2 files changed, 22 insertions(+), 6 deletions(-)
diff --git a/model.cc b/model.cc
index bd4496b..fc93296 100644
--- a/model.cc
+++ b/model.cc
@@ -387,10 +387,13 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
* Updates the mo_graph with the constraints imposed from the current read.
* @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
*/
-void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
+bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
+{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
unsigned int i;
+ bool added = false;
ASSERT(curr->is_read());
/* Iterate over all threads */
@@ -405,15 +408,20 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r
if (act->happens_before(curr)) {
if (act->is_read()) {
const ModelAction *prevreadfrom = act->get_reads_from();
- if (prevreadfrom != NULL && rf != prevreadfrom)
+ if (prevreadfrom != NULL && rf != prevreadfrom) {
mo_graph->addEdge(prevreadfrom, rf);
+ added = true;
+ }
} else if (rf != act) {
mo_graph->addEdge(act, rf);
+ added = true;
}
break;
}
}
}
+
+ return added;
}
/** Updates the mo_graph with the constraints imposed from the current read. */
@@ -456,18 +464,23 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
/**
* Updates the mo_graph with the constraints imposed from the current write.
* @param curr The current action. Must be a write.
+ * @return True if modification order edges were added; false otherwise
*/
-void ModelChecker::w_modification_order(ModelAction * curr) {
+bool ModelChecker::w_modification_order(ModelAction *curr)
+{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
unsigned int i;
+ bool added = false;
ASSERT(curr->is_write());
if (curr->is_seqcst()) {
/* We have to at least see the last sequentially consistent write,
so we are initialized. */
ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location());
- if (last_seq_cst != NULL)
+ if (last_seq_cst != NULL) {
mo_graph->addEdge(last_seq_cst, curr);
+ added = true;
+ }
}
/* Iterate over all threads */
@@ -484,6 +497,7 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
mo_graph->addEdge(act->get_reads_from(), curr);
else
mo_graph->addEdge(act, curr);
+ added = true;
break;
} else if (act->is_read() && !act->is_synchronizing(curr) &&
!act->same_thread(curr)) {
@@ -501,6 +515,8 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
}
}
}
+
+ return added;
}
/**
diff --git a/model.h b/model.h
index 0666472..7dc6ed6 100644
--- a/model.h
+++ b/model.h
@@ -103,8 +103,8 @@ private:
void build_reads_from_past(ModelAction *curr);
ModelAction * process_rmw(ModelAction *curr);
void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
- void r_modification_order(ModelAction *curr, const ModelAction *rf);
- void w_modification_order(ModelAction *curr);
+ bool r_modification_order(ModelAction *curr, const ModelAction *rf);
+ bool w_modification_order(ModelAction *curr);
bool release_seq_head(const ModelAction *rf,
std::vector<const ModelAction *> *release_heads) const;
--
2.34.1