projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
9bbf98a
)
model: record last fence-release from each thread
author
Brian Norris
<banorris@uci.edu>
Tue, 4 Dec 2012 00:51:43 +0000
(16:51 -0800)
committer
Brian Norris
<banorris@uci.edu>
Tue, 4 Dec 2012 02:26:48 +0000
(18:26 -0800)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 82b90601048845f32a9af77d57e938e8fb11450f..f96249fcb9cf9ceeb9eb0b97b5a13c9b74b96b60 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-91,6
+91,7
@@
ModelChecker::ModelChecker(struct model_params params) :
futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
+ thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
node_stack(new NodeStack()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
node_stack(new NodeStack()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
@@
-120,6
+121,7
@@
ModelChecker::~ModelChecker()
delete pending_rel_seqs;
delete thrd_last_action;
delete pending_rel_seqs;
delete thrd_last_action;
+ delete thrd_last_fence_release;
delete node_stack;
delete scheduler;
delete mo_graph;
delete node_stack;
delete scheduler;
delete mo_graph;
@@
-1024,6
+1026,10
@@
bool ModelChecker::initialize_curr_action(ModelAction **curr)
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ /* Assign most recent release fence */
+ newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
+
/*
* Perform one-time actions when pushing new ModelAction onto
* NodeStack
/*
* Perform one-time actions when pushing new ModelAction onto
* NodeStack
@@
-1998,6
+2004,12
@@
void ModelChecker::add_action_to_lists(ModelAction *act)
thrd_last_action->resize(get_num_threads());
(*thrd_last_action)[tid] = act;
thrd_last_action->resize(get_num_threads());
(*thrd_last_action)[tid] = act;
+ if (act->is_fence() && act->is_release()) {
+ if ((int)thrd_last_fence_release->size() <= tid)
+ thrd_last_fence_release->resize(get_num_threads());
+ (*thrd_last_fence_release)[tid] = act;
+ }
+
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
@@
-2023,6
+2035,20
@@
ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
return NULL;
}
return NULL;
}
+/**
+ * @brief Get the last fence release performed by a particular Thread
+ * @param tid The thread ID of the Thread in question
+ * @return The last fence release in the thread, if one exists; NULL otherwise
+ */
+ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
+{
+ int threadid = id_to_int(tid);
+ if (threadid < (int)thrd_last_fence_release->size())
+ return (*thrd_last_fence_release)[id_to_int(tid)];
+ else
+ return NULL;
+}
+
/**
* Gets the last memory_order_seq_cst write (in the total global sequence)
* performed on a particular object (i.e., memory location), not including the
/**
* Gets the last memory_order_seq_cst write (in the total global sequence)
* performed on a particular object (i.e., memory location), not including the
diff --git
a/model.h
b/model.h
index 11afba9f66129eb18f85ec34cd29160c4c751622..fd99700a01c35f77ff2d87445ee228b71ae69de5 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-170,6
+170,7
@@
private:
void check_curr_backtracking(ModelAction * curr);
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid) const;
void check_curr_backtracking(ModelAction * curr);
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid) const;
+ ModelAction * get_last_fence_release(thread_id_t tid) const;
ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const;
ModelAction * get_last_unlock(ModelAction *curr) const;
ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const;
ModelAction * get_last_unlock(ModelAction *curr) const;
@@
-213,6
+214,7
@@
private:
std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> > *pending_rel_seqs;
std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > *thrd_last_action;
std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> > *pending_rel_seqs;
std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > *thrd_last_action;
+ std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > *thrd_last_fence_release;
NodeStack *node_stack;
/** Private data members that should be snapshotted. They are grouped
NodeStack *node_stack;
/** Private data members that should be snapshotted. They are grouped