#include "model.h"
#include "execution.h"
#include "action.h"
-#include "nodestack.h"
#include "schedule.h"
#include "common.h"
#include "clockvector.h"
#include "datarace.h"
#include "threads-model.h"
#include "bugmessage.h"
+#include "history.h"
#include "fuzzer.h"
#define INITIAL_THREAD_ID 0
};
/** @brief Constructor */
-ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) :
+ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
model(m),
params(NULL),
scheduler(scheduler),
mutex_map(),
thrd_last_action(1),
thrd_last_fence_release(),
- node_stack(node_stack),
priv(new struct model_snapshot_members ()),
mo_graph(new CycleGraph()),
- fuzzer(new Fuzzer())
+ fuzzer(new Fuzzer()),
+ thrd_func_list(),
+ thrd_func_act_lists(),
+ isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
add_thread(model_thread);
scheduler->register_engine(this);
- node_stack->register_engine(this);
}
/** @brief Destructor */
return tmp;
}
-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<
const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
{
SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
return true;
}
+ if (asleep->is_sleep()) {
+ if (fuzzer->shouldWake(asleep))
+ return true;
+ }
+
return false;
}
return priv->bugs.size() != 0;
}
+/** @return True, if any fatal bugs have been reported for this execution.
+ * Any bug other than a data race is considered a fatal bug. Data races
+ * are not considered fatal unless the number of races is exceeds
+ * a threshold (temporarily set as 15).
+ */
+bool ModelExecution::have_fatal_bug_reports() const
+{
+ return priv->bugs.size() != 0;
+}
+
SnapVector<bug_message *> * ModelExecution::get_bugs() const
{
return &priv->bugs;
return true;
}
+ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
+ uint64_t value = *((const uint64_t *) location);
+ modelclock_t storeclock;
+ thread_id_t storethread;
+ getStoreThreadAndClock(location, &storethread, &storeclock);
+ setAtomicStoreFlag(location);
+ ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
+ act->set_seq_number(storeclock);
+ add_normal_write_to_lists(act);
+ add_write_to_lists(act);
+ w_modification_order(act);
+ return act;
+}
/**
* Processes a read model action.
* @param rf_set is the set of model actions we can possibly read from
* @return True if processing this read updates the mo_graph.
*/
-void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set)
+void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
{
SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
- while(true) {
+ bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
+ if (hasnonatomicstore) {
+ ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
+ rf_set->push_back(nonatomicstore);
+ }
+ while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
- const ModelAction *rf = (*rf_set)[index];
+ ModelAction *rf = (*rf_set)[index];
ASSERT(rf);
}
//otherwise fall into the lock case
case ATOMIC_LOCK: {
- if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
- assert_bug("Lock access before initialization");
+ //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
+ //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+ // assert_bug("Lock access before initialization");
state->locked = get_thread(curr);
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
case ATOMIC_NOTIFY_ALL: {
action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
//activate all the waiting threads
- for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
- scheduler->wake(get_thread(*rit));
+ for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
+ scheduler->wake(get_thread(rit->getVal()));
}
waiters->clear();
break;
*/
void ModelExecution::process_write(ModelAction *curr)
{
-
w_modification_order(curr);
-
-
get_thread(curr)->set_return_value(VALUE_NONE);
}
bool updated = false;
if (curr->is_acquire()) {
action_list_t *list = &action_trace;
- action_list_t::reverse_iterator rit;
+ sllnode<ModelAction *> * rit;
/* Find X : is_read(X) && X --sb-> curr */
- for (rit = list->rbegin();rit != list->rend();rit++) {
- ModelAction *act = *rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
if (act == curr)
continue;
if (act->get_tid() != curr->get_tid())
continue;
/* Establish hypothetical release sequences */
- rel_heads_list_t release_heads;
- get_release_seq_heads(curr, act, &release_heads);
- for (unsigned int i = 0;i < release_heads.size();i++)
- synchronize(release_heads[i], curr);
- if (release_heads.size() != 0)
+ ClockVector *cv = get_hb_from_write(act->get_reads_from());
+ if (cv != NULL && curr->get_cv()->merge(cv))
updated = true;
}
}
* @param curr The current action
* @return True if synchronization was updated or a thread completed
*/
-bool ModelExecution::process_thread_action(ModelAction *curr)
+void ModelExecution::process_thread_action(ModelAction *curr)
{
- bool updated = false;
-
switch (curr->get_type()) {
case THREAD_CREATE: {
thrd_t *thrd = (thrd_t *)curr->get_location();
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
synchronize(act, curr);
- updated = true; /* trigger rel-seq checks */
break;
}
case PTHREAD_JOIN: {
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
synchronize(act, curr);
- updated = true; /* trigger rel-seq checks */
break; // WL: to be add (modified)
}
+ case THREADONLY_FINISH:
case THREAD_FINISH: {
Thread *th = get_thread(curr);
+ if (curr->get_type() == THREAD_FINISH &&
+ th == model->getInitThread()) {
+ th->complete();
+ setFinished();
+ break;
+ }
+
/* Wake up any joining threads */
for (unsigned int i = 0;i < get_num_threads();i++) {
Thread *waiting = get_thread(int_to_id(i));
scheduler->wake(waiting);
}
th->complete();
- updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
default:
break;
}
-
- return updated;
}
/**
* Initialize the current action by performing one or more of the following
- * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
- * in the NodeStack, manipulating backtracking sets, allocating and
+ * actions, as appropriate: merging RMWR and RMWC/RMW actions,
+ * manipulating backtracking sets, allocating and
* initializing clock vectors, and computing the promises to fulfill.
*
* @param curr The current action, as passed from the user context; may be
*/
bool ModelExecution::initialize_curr_action(ModelAction **curr)
{
- ModelAction *newcurr;
-
if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
- newcurr = process_rmw(*curr);
+ ModelAction *newcurr = process_rmw(*curr);
delete *curr;
*curr = newcurr;
return false;
- }
-
- (*curr)->set_seq_number(get_next_seq_num());
-
- newcurr = node_stack->explore_action(*curr);
- if (newcurr) {
- /* First restore type and order in case of RMW operation */
- if ((*curr)->is_rmwr())
- newcurr->copy_typeandorder(*curr);
-
- ASSERT((*curr)->get_location() == newcurr->get_location());
- newcurr->copy_from_new(*curr);
-
- /* Discard duplicate ModelAction; use action from NodeStack */
- delete *curr;
-
- /* Always compute new clock vector */
- newcurr->create_cv(get_parent_action(newcurr->get_tid()));
-
- *curr = newcurr;
- return false; /* Action was explored previously */
} else {
- newcurr = *curr;
+ ModelAction *newcurr = *curr;
+ newcurr->set_seq_number(get_next_seq_num());
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
* @return True if this read established synchronization
*/
-bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
+void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
{
ASSERT(rf);
ASSERT(rf->is_write());
act->set_read_from(rf);
if (act->is_acquire()) {
- rel_heads_list_t release_heads;
- get_release_seq_heads(act, act, &release_heads);
- int num_heads = release_heads.size();
- for (unsigned int i = 0;i < release_heads.size();i++)
- if (!synchronize(release_heads[i], act))
- num_heads--;
- return num_heads > 0;
+ ClockVector *cv = get_hb_from_write(rf);
+ if (cv == NULL)
+ return;
+ act->get_cv()->merge(cv);
}
- return false;
}
/**
if (!blocking->is_complete()) {
return false;
}
+ } else if (curr->is_sleep()) {
+ if (!fuzzer->shouldSleep(curr))
+ return false;
}
return true;
if (!second_part_of_rmw && curr->get_type() != NOOP)
add_action_to_lists(curr);
- SnapVector<const ModelAction *> * rf_set = NULL;
+ if (curr->is_write())
+ add_write_to_lists(curr);
+
+ SnapVector<ModelAction *> * rf_set = NULL;
/* Build may_read_from set for newly-created actions */
if (newly_explored && curr->is_read())
rf_set = build_may_read_from(curr);
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[tid];
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin();rit != list->rend();rit++) {
- ModelAction *act = *rit;
+ sllnode<ModelAction *> * rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
/* Skip curr */
if (act == curr)
if (act->happens_before(curr)) {
if (i==0) {
if (last_sc_fence_local == NULL ||
- (*last_sc_fence_local < *prev_same_thread)) {
+ (*last_sc_fence_local < *act)) {
prev_same_thread = act;
}
}
unsigned int i;
ASSERT(curr->is_write());
+ SnapList<ModelAction *> edgeset;
+
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_write(curr);
if (last_seq_cst != NULL) {
- mo_graph->addEdge(last_seq_cst, curr);
+ edgeset.push_back(last_seq_cst);
}
+ //update map for next query
+ obj_last_sc_map.put(curr->get_location(), curr);
}
/* Last SC fence in the current thread */
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- bool force_edge = false;
- for (rit = list->rbegin();rit != list->rend();rit++) {
- ModelAction *act = *rit;
+ sllnode<ModelAction*>* rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
if (act == curr) {
/*
* 1) If RMW and it actually read from something, then we
* 3) If normal write, we need to look at earlier actions, so
* continue processing list.
*/
- force_edge = true;
if (curr->is_rmw()) {
if (curr->get_reads_from() != NULL)
break;
/* C++, Section 29.3 statement 7 */
if (last_sc_fence_thread_before && act->is_write() &&
*act < *last_sc_fence_thread_before) {
- mo_graph->addEdge(act, curr, force_edge);
+ edgeset.push_back(act);
break;
}
* readfrom(act) --mo--> act
*/
if (act->is_write())
- mo_graph->addEdge(act, curr, force_edge);
+ edgeset.push_back(act);
else if (act->is_read()) {
//if previous read accessed a null, just keep going
- mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
+ edgeset.push_back(act->get_reads_from());
}
break;
- } else if (act->is_read() && !act->could_synchronize_with(curr) &&
- !act->same_thread(curr)) {
- /* We have an action that:
- (1) did not happen before us
- (2) is a read and we are a write
- (3) cannot synchronize with us
- (4) is in a different thread
- =>
- that read could potentially read from our write. Note that
- these checks are overly conservative at this point, we'll
- do more checks before actually removing the
- pendingfuturevalue.
-
- */
-
}
}
}
+ mo_graph->addEdges(&edgeset, curr);
+
}
/**
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin();rit != list->rend();rit++) {
- ModelAction *act = *rit;
+ sllnode<ModelAction *>* rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
/* Don't disallow due to act == reader */
if (!reader->happens_before(act) || reader == act)
}
/**
- * Finds the head(s) of the release sequence(s) containing a given ModelAction.
- * The ModelAction under consideration is expected to be taking part in
- * release/acquire synchronization as an object of the "reads from" relation.
- * Note that this can only provide release sequence support for RMW chains
- * which do not read from the future, as those actions cannot be traced until
- * their "promise" is fulfilled. Similarly, we may not even establish the
- * presence of a release sequence with certainty, as some modification order
- * constraints may be decided further in the future. Thus, this function
- * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
- * and a boolean representing certainty.
+ * Computes the clock vector that happens before propagates from this write.
*
* @param rf The action that might be part of a release sequence. Must be a
* write.
- * @param release_heads A pass-by-reference style return parameter. After
- * execution of this function, release_heads will contain the heads of all the
- * relevant release sequences, if any exists with certainty
- * @return true, if the ModelExecution is certain that release_heads is complete;
- * false otherwise
+ * @return ClockVector of happens before relation.
*/
-bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
-{
+ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
+ SnapVector<ModelAction *> * processset = NULL;
for ( ;rf != NULL;rf = rf->get_reads_from()) {
ASSERT(rf->is_write());
+ if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
+ break;
+ if (processset == NULL)
+ processset = new SnapVector<ModelAction *>();
+ processset->push_back(rf);
+ }
- if (rf->is_release())
- release_heads->push_back(rf);
- else if (rf->get_last_fence_release())
- release_heads->push_back(rf->get_last_fence_release());
- if (!rf->is_rmw())
- break;/* End of RMW chain */
-
- /** @todo Need to be smarter here... In the linux lock
- * example, this will run to the beginning of the program for
- * every acquire. */
- /** @todo The way to be smarter here is to keep going until 1
- * thread has a release preceded by an acquire and you've seen
- * both. */
-
- /* acq_rel RMW is a sufficient stopping condition */
- if (rf->is_acquire() && rf->is_release())
- return true;/* complete */
- };
- ASSERT(rf); // Needs to be real write
-
- if (rf->is_release())
- return true;/* complete */
-
- /* else relaxed write
- * - check for fence-release in the same thread (29.8, stmt. 3)
- * - check modification order for contiguous subsequence
- * -> rf must be same thread as release */
-
- const ModelAction *fence_release = rf->get_last_fence_release();
- /* Synchronize with a fence-release unconditionally; we don't need to
- * find any more "contiguous subsequence..." for it */
- if (fence_release)
- release_heads->push_back(fence_release);
-
- return true; /* complete */
-}
+ int i = (processset == NULL) ? 0 : processset->size();
-/**
- * An interface for getting the release sequence head(s) with which a
- * given ModelAction must synchronize. This function only returns a non-empty
- * result when it can locate a release sequence head with certainty. Otherwise,
- * it may mark the internal state of the ModelExecution so that it will handle
- * the release sequence at a later time, causing @a acquire to update its
- * synchronization at some later point in execution.
- *
- * @param acquire The 'acquire' action that may synchronize with a release
- * sequence
- * @param read The read action that may read from a release sequence; this may
- * be the same as acquire, or else an earlier action in the same thread (i.e.,
- * when 'acquire' is a fence-acquire)
- * @param release_heads A pass-by-reference return parameter. Will be filled
- * with the head(s) of the release sequence(s), if they exists with certainty.
- * @see ModelExecution::release_seq_heads
- */
-void ModelExecution::get_release_seq_heads(ModelAction *acquire,
- ModelAction *read, rel_heads_list_t *release_heads)
-{
- const ModelAction *rf = read->get_reads_from();
-
- release_seq_heads(rf, release_heads);
+ ClockVector * vec = NULL;
+ while(true) {
+ if (rf->get_rfcv() != NULL) {
+ vec = rf->get_rfcv();
+ } else if (rf->is_acquire() && rf->is_release()) {
+ vec = rf->get_cv();
+ } else if (rf->is_release() && !rf->is_rmw()) {
+ vec = rf->get_cv();
+ } else if (rf->is_release()) {
+ //have rmw that is release and doesn't have a rfcv
+ (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
+ rf->set_rfcv(vec);
+ } else {
+ //operation that isn't release
+ if (rf->get_last_fence_release()) {
+ if (vec == NULL)
+ vec = rf->get_last_fence_release()->get_cv();
+ else
+ (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
+ }
+ rf->set_rfcv(vec);
+ }
+ i--;
+ if (i >= 0) {
+ rf = (*processset)[i];
+ } else
+ break;
+ }
+ if (processset != NULL)
+ delete processset;
+ return vec;
}
/**
uninit = get_uninitialized_action(act);
uninit_id = id_to_int(uninit->get_tid());
list->push_front(uninit);
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+ if (uninit_id >= (int)vec->size()) {
+ int oldsize = (int) vec->size();
+ vec->resize(uninit_id + 1);
+ for(int i=oldsize;i<uninit_id+1;i++) {
+ new(&(*vec)[i]) action_list_t();
+ }
+ }
+ (*vec)[uninit_id].push_front(uninit);
}
list->push_back(act);
+ // Update action trace, a total order of all actions
action_trace.push_back(act);
if (uninit)
action_trace.push_front(uninit);
+ // Update obj_thrd_map, a per location, per thread, order of actions
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
- if (tid >= (int)vec->size())
+ if (tid >= (int)vec->size()) {
+ uint oldsize =vec->size();
vec->resize(priv->next_thread_id);
+ for(uint i=oldsize;i<priv->next_thread_id;i++)
+ new (&(*vec)[i]) action_list_t();
+ }
(*vec)[tid].push_back(act);
if (uninit)
(*vec)[uninit_id].push_front(uninit);
+ // Update thrd_last_action, the last action taken by each thrad
if ((int)thrd_last_action.size() <= tid)
thrd_last_action.resize(get_num_threads());
thrd_last_action[tid] = act;
if (uninit)
thrd_last_action[uninit_id] = uninit;
+ // Update thrd_last_fence_release, the last release fence taken by each thread
if (act->is_fence() && act->is_release()) {
if ((int)thrd_last_fence_release.size() <= tid)
thrd_last_fence_release.resize(get_num_threads());
get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
- if (tid >= (int)vec->size())
+ if (tid >= (int)vec->size()) {
+ uint oldsize = vec->size();
vec->resize(priv->next_thread_id);
+ for(uint i=oldsize;i<priv->next_thread_id;i++)
+ new (&(*vec)[i]) action_list_t();
+ }
(*vec)[tid].push_back(act);
}
}
+void insertIntoActionList(action_list_t *list, ModelAction *act) {
+ sllnode<ModelAction*> * rit = list->end();
+ modelclock_t next_seq = act->get_seq_number();
+ if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
+ list->push_back(act);
+ else {
+ for(;rit != NULL;rit=rit->getPrev()) {
+ if (rit->getVal()->get_seq_number() == next_seq) {
+ list->insertAfter(rit, act);
+ break;
+ }
+ }
+ }
+}
+
+void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+ sllnode<ModelAction*> * rit = list->end();
+ modelclock_t next_seq = act->get_seq_number();
+ if (rit == NULL) {
+ act->create_cv(NULL);
+ } else if (rit->getVal()->get_seq_number() == next_seq) {
+ act->create_cv(rit->getVal());
+ list->push_back(act);
+ } else {
+ for(;rit != NULL;rit=rit->getPrev()) {
+ if (rit->getVal()->get_seq_number() == next_seq) {
+ act->create_cv(rit->getVal());
+ list->insertAfter(rit, act);
+ break;
+ }
+ }
+ }
+}
+
+/**
+ * Performs various bookkeeping operations for a normal write. The
+ * complication is that we are typically inserting a normal write
+ * lazily, so we need to insert it into the middle of lists.
+ *
+ * @param act is the ModelAction to add.
+ */
+
+void ModelExecution::add_normal_write_to_lists(ModelAction *act)
+{
+ int tid = id_to_int(act->get_tid());
+ insertIntoActionListAndSetCV(&action_trace, act);
+
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ insertIntoActionList(list, act);
+
+ // Update obj_thrd_map, a per location, per thread, order of actions
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ if (tid >= (int)vec->size()) {
+ uint oldsize =vec->size();
+ vec->resize(priv->next_thread_id);
+ for(uint i=oldsize;i<priv->next_thread_id;i++)
+ new (&(*vec)[i]) action_list_t();
+ }
+ insertIntoActionList(&(*vec)[tid],act);
+
+ // Update thrd_last_action, the last action taken by each thrad
+ if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
+ thrd_last_action[tid] = act;
+}
+
+
+void ModelExecution::add_write_to_lists(ModelAction *write) {
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
+ int tid = id_to_int(write->get_tid());
+ if (tid >= (int)vec->size()) {
+ uint oldsize =vec->size();
+ vec->resize(priv->next_thread_id);
+ for(uint i=oldsize;i<priv->next_thread_id;i++)
+ new (&(*vec)[i]) action_list_t();
+ }
+ (*vec)[tid].push_back(write);
+}
+
/**
* @brief Get the last action performed by a particular Thread
* @param tid The thread ID of the Thread in question
ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list = obj_map.get(location);
- /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin();(*rit) != curr;rit++)
- ;
- rit++; /* Skip past curr */
- for ( ;rit != list->rend();rit++)
- if ((*rit)->is_write() && (*rit)->is_seqcst())
- return *rit;
- return NULL;
+ return obj_last_sc_map.get(location);
}
/**
if (!list)
return NULL;
- action_list_t::reverse_iterator rit = list->rbegin();
+ sllnode<ModelAction*>* rit = list->end();
if (before_fence) {
- for (;rit != list->rend();rit++)
- if (*rit == before_fence)
+ for (;rit != NULL;rit=rit->getPrev())
+ if (rit->getVal() == before_fence)
break;
- ASSERT(*rit == before_fence);
- rit++;
+ ASSERT(rit->getVal() == before_fence);
+ rit=rit->getPrev();
}
- for (;rit != list->rend();rit++)
- if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
- return *rit;
+ for (;rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
+ if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
+ return act;
+ }
return NULL;
}
action_list_t *list = obj_map.get(location);
/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin();rit != list->rend();rit++)
- if ((*rit)->is_unlock() || (*rit)->is_wait())
- return *rit;
+ sllnode<ModelAction*>* rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev())
+ if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
+ return rit->getVal();
return NULL;
}
* @param curr is the current ModelAction that we are exploring; it must be a
* 'read' operation.
*/
-SnapVector<const ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
+SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
{
- SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
+ SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
if (curr->is_seqcst())
last_sc_write = get_last_seq_cst_write(curr);
- SnapVector<const ModelAction *> * rf_set = new SnapVector<const ModelAction *>();
+ SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
/* Iterate over all threads */
for (i = 0;i < thrd_lists->size();i++) {
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin();rit != list->rend();rit++) {
- const ModelAction *act = *rit;
-
- /* Only consider 'write' actions */
- if (!act->is_write()) {
- if (act != curr && act->is_read() && act->happens_before(curr)) {
- const ModelAction *tmp = act->get_reads_from();
- if (((unsigned int) id_to_int(tmp->get_tid()))==i)
- act = tmp;
- else
- break;
- } else
- continue;
- }
+ sllnode<ModelAction *> * rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
if (act == curr)
continue;
/**
* @brief Get an action representing an uninitialized atomic
*
- * This function may create a new one or try to retrieve one from the NodeStack
+ * This function may create a new one.
*
* @param curr The current action, which prompts the creation of an UNINIT action
* @return A pointer to the UNINIT ModelAction
*/
-ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
+ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
{
- Node *node = curr->get_node();
- ModelAction *act = node->get_uninit_action();
+ ModelAction *act = curr->get_uninit_action();
if (!act) {
act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
- node->set_uninit_action(act);
+ curr->set_uninit_action(act);
}
act->create_cv(NULL);
return act;
}
-static void print_list(const action_list_t *list)
+static void print_list(action_list_t *list)
{
- action_list_t::const_iterator it;
+ sllnode<ModelAction*> *it;
model_print("------------------------------------------------------------------------------------\n");
model_print("# t Action type MO Location Value Rf CV\n");
unsigned int hash = 0;
- for (it = list->begin();it != list->end();it++) {
- const ModelAction *act = *it;
+ for (it = list->begin();it != NULL;it=it->getNext()) {
+ const ModelAction *act = it->getVal();
if (act->get_seq_number() > 0)
act->print();
- hash = hash^(hash<<3)^((*it)->hash());
+ hash = hash^(hash<<3)^(it->getVal()->hash());
}
model_print("HASH %u\n", hash);
model_print("------------------------------------------------------------------------------------\n");
}
#if SUPPORT_MOD_ORDER_DUMP
-void ModelExecution::dumpGraph(char *filename) const
+void ModelExecution::dumpGraph(char *filename)
{
char buffer[200];
sprintf(buffer, "%s.dot", filename);
mo_graph->dumpNodes(file);
ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
- for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
- ModelAction *act = *it;
+ for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
+ ModelAction *act = it->getVal();
if (act->is_read()) {
mo_graph->dot_print_node(file, act);
mo_graph->dot_print_edge(file,
#endif
/** @brief Prints an execution trace summary. */
-void ModelExecution::print_summary() const
+void ModelExecution::print_summary()
{
#if SUPPORT_MOD_ORDER_DUMP
char buffername[100];
curr = check_current_action(curr);
ASSERT(curr);
+ /* Process this action in ModelHistory for records */
+ model->get_history()->process_action( curr, curr->get_tid() );
+
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
projects / c11tester.git / blobdiff