From b5518c866ccd232fa79a2911ce5c6bcaa2110076 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 19 Jul 2012 12:18:25 -0700
Subject: [PATCH] small changes (things still work) towards support RMW
Reserve value field only for writes. Using it for reads will only make thinks
weird for RMW operations.
[Amended by Brian Norris]
---
action.cc | 18 ++++++++++++++----
action.h | 5 +++--
model.cc | 22 ++++++++++++++++++++++
model.h | 1 +
4 files changed, 40 insertions(+), 6 deletions(-)
diff --git a/action.cc b/action.cc
index b5c72c02..c617f0d7 100644
--- a/action.cc
+++ b/action.cc
@@ -28,12 +28,12 @@ ModelAction::~ModelAction()
bool ModelAction::is_read() const
{
- return type == ATOMIC_READ;
+ return type == ATOMIC_READ || type == ATOMIC_RMW;
}
bool ModelAction::is_write() const
{
- return type == ATOMIC_WRITE || type == ATOMIC_INIT;
+ return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT;
}
bool ModelAction::is_rmw() const
@@ -85,6 +85,15 @@ bool ModelAction::same_thread(const ModelAction *act) const
return tid == act->tid;
}
+void ModelAction::upgrade_rmw(ModelAction * act) {
+ ASSERT(is_read());
+ ASSERT(act->is_rmw());
+ //Upgrade our type to the act's type
+ this->type=act->type;
+ this->order=act->order;
+ this->value=act->value;
+}
+
/** 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.
@@ -136,7 +145,6 @@ void ModelAction::read_from(const ModelAction *act)
if (act->is_release() && this->is_acquire())
cv->merge(act->cv);
reads_from = act;
- value = act->value;
}
/**
@@ -182,8 +190,10 @@ void ModelAction::print(void) const
type_str = "unknown type";
}
+ uint64_t valuetoprint=type==ATOMIC_READ?reads_from->value:value;
+
printf("(%3d) Thread: %-2d Action: %-13s MO: %d Loc: %14p Value: %-12" PRIu64,
- seq_number, id_to_int(tid), type_str, order, location, value);
+ seq_number, id_to_int(tid), type_str, order, location, valuetoprint);
if (reads_from)
printf(" Rf: %d", reads_from->get_seq_number());
if (cv) {
diff --git a/action.h b/action.h
index 36c72079..fff6bc82 100644
--- a/action.h
+++ b/action.h
@@ -80,6 +80,8 @@ public:
return get_seq_number() > act.get_seq_number();
}
+ void upgrade_rmw(ModelAction * act);
+
MEMALLOC
private:
@@ -95,8 +97,7 @@ private:
/** The thread id that performed this action. */
thread_id_t tid;
- /** The value read or written (if RMW, then the value written). This
- * should probably be something longer. */
+ /** The value written (for write or RMW; undefined for read) */
uint64_t value;
/** The action that this action reads from. Only valid for reads */
diff --git a/model.cc b/model.cc
index cf845ecd..1b379000 100644
--- a/model.cc
+++ b/model.cc
@@ -252,6 +252,15 @@ void ModelChecker::check_current_action(void)
return;
}
+ if (curr->is_rmw()) {
+ //We have a RMW action
+ process_rmw(curr);
+ //Force the current thread to continue since the RMW should be atomic
+ nextThread = thread_current()->get_id();
+ delete curr;
+ return;
+ }
+
tmp = node_stack->explore_action(curr);
if (tmp) {
/* Discard duplicate ModelAction; use action from NodeStack */
@@ -274,6 +283,10 @@ void ModelChecker::check_current_action(void)
th->set_creation(curr);
}
+ /* Is there a better interface for setting the next thread rather
+ than this field/convoluted approach? Perhaps like just returning
+ it or something? */
+
nextThread = get_next_replay_thread();
Node *currnode = curr->get_node();
@@ -310,6 +323,15 @@ bool ModelChecker::isfeasible() {
return !cyclegraph->checkForCycles();
}
+/** Process a RMW by converting previous read into a RMW. */
+void ModelChecker::process_rmw(ModelAction * act) {
+ int tid = id_to_int(act->get_tid());
+ std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
+ ASSERT(tid < (int) vec->size());
+ ModelAction *lastread=(*vec)[tid].back();
+ lastread->upgrade_rmw(act);
+}
+
void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
unsigned int i;
diff --git a/model.h b/model.h
index 4c0af0af..a4751099 100644
--- a/model.h
+++ b/model.h
@@ -83,6 +83,7 @@ private:
ModelAction * get_parent_action(thread_id_t tid);
ModelAction * get_last_seq_cst(const void *location);
void build_reads_from_past(ModelAction *curr);
+ void process_rmw(ModelAction * curr);
void r_modification_order(ModelAction * curr, const ModelAction *rf);
void w_modification_order(ModelAction * curr);
--
2.34.1