#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),
action_trace(),
thread_map(2), /* We'll always need at least 2 threads */
pthread_map(0),
- pthread_counter(0),
+ pthread_counter(1),
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
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())
+ mo_graph(new CycleGraph()),
+ fuzzer(new Fuzzer()),
+ thrd_func_list(),
+ thrd_func_inst_lists()
{
/* 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) {
return tmp;
}
-action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
-{
- SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
- if (wrv==NULL)
- return NULL;
- unsigned int thread=id_to_int(tid);
- if (thread < wrv->size())
- return &(*wrv)[thread];
- else
- return NULL;
-}
-
/** @return a thread ID for a new Thread */
thread_id_t ModelExecution::get_next_id()
{
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.
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);
-
- if (r_modification_order(curr, rf, priorset)) {
+ bool canprune = false;
+ if (r_modification_order(curr, rf, priorset, &canprune)) {
for(unsigned int i=0;i<priorset->size();i++) {
mo_graph->addEdge((*priorset)[i], rf);
}
read_from(curr, rf);
get_thread(curr)->set_return_value(curr->get_return_value());
delete priorset;
+ if (canprune && curr->get_type() == ATOMIC_READ) {
+ int tid = id_to_int(curr->get_tid());
+ (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
+ }
return;
}
priorset->clear();
}
//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_WAIT:
case ATOMIC_UNLOCK: {
+ //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
+
/* wake up the other threads */
for (unsigned int i = 0;i < get_num_threads();i++) {
Thread *t = get_thread(int_to_id(i));
}
case ATOMIC_NOTIFY_ONE: {
action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
- Thread * thread = fuzzer->selectNotify(waiters);
- scheduler->wake(thread);
+ if (waiters->size() != 0) {
+ Thread * thread = fuzzer->selectNotify(waiters);
+ scheduler->wake(thread);
+ }
break;
}
*/
void ModelExecution::process_write(ModelAction *curr)
{
-
w_modification_order(curr);
-
-
get_thread(curr)->set_return_value(VALUE_NONE);
}
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;
}
}
/**
* 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;
}
/**
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
- if (!second_part_of_rmw)
+ if (!second_part_of_rmw && curr->get_type() != NOOP)
add_action_to_lists(curr);
+ 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())
* @return True if modification order edges were added; false otherwise
*/
-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset)
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
- ModelAction *last_sc_write = NULL;
- if (curr->is_seqcst())
- last_sc_write = get_last_seq_cst_write(curr);
+ int tid = curr->get_tid();
+ ModelAction *prev_same_thread = NULL;
/* Iterate over all threads */
- for (i = 0;i < thrd_lists->size();i++) {
- /* Last SC fence in thread i */
+ for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
+ /* Last SC fence in thread tid */
ModelAction *last_sc_fence_thread_local = NULL;
- if (int_to_id((int)i) != curr->get_tid())
- last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
+ if (i != 0)
+ last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
- /* Last SC fence in thread i, before last SC fence in current thread */
+ /* Last SC fence in thread tid, before last SC fence in current thread */
ModelAction *last_sc_fence_thread_before = NULL;
if (last_sc_fence_local)
- last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+ last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
+
+ //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
+ if (prev_same_thread != NULL &&
+ (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
+ (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
+ continue;
+ }
/* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
+ action_list_t *list = &(*thrd_lists)[tid];
action_list_t::reverse_iterator rit;
for (rit = list->rbegin();rit != list->rend();rit++) {
ModelAction *act = *rit;
* before" curr
*/
if (act->happens_before(curr)) {
+ if (i==0) {
+ if (last_sc_fence_local == NULL ||
+ (*last_sc_fence_local < *act)) {
+ prev_same_thread = act;
+ }
+ }
if (act->is_write()) {
if (mo_graph->checkReachable(rf, act))
return false;
if (mo_graph->checkReachable(rf, prevrf))
return false;
priorset->push_back(prevrf);
+ } else {
+ if (act->get_tid() == curr->get_tid()) {
+ //Can prune curr from obj list
+ *canprune = true;
+ }
}
}
break;
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;
if (act == curr) {
* 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);
+
}
/**
}
/**
- * 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 */
-}
-
-/**
- * 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();
+ int i = (processset == NULL) ? 0 : processset->size();
- 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())
+ vec->resize(uninit_id + 1);
+ (*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())
vec->resize(priv->next_thread_id);
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());
}
}
+void insertIntoActionList(action_list_t *list, ModelAction *act) {
+ action_list_t::reverse_iterator rit = list->rbegin();
+ modelclock_t next_seq = act->get_seq_number();
+ if (rit == list->rend() || (*rit)->get_seq_number() == next_seq)
+ list->push_back(act);
+ else {
+ for(;rit != list->rend();rit++) {
+ if ((*rit)->get_seq_number() == next_seq) {
+ action_list_t::iterator it = rit.base();
+ list->insert(it, act);
+ break;
+ }
+ }
+ }
+}
+
+void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+ action_list_t::reverse_iterator rit = list->rbegin();
+ modelclock_t next_seq = act->get_seq_number();
+ if (rit == list->rend()) {
+ act->create_cv(NULL);
+ } else if ((*rit)->get_seq_number() == next_seq) {
+ act->create_cv((*rit));
+ list->push_back(act);
+ } else {
+ for(;rit != list->rend();rit++) {
+ if ((*rit)->get_seq_number() == next_seq) {
+ act->create_cv((*rit));
+ action_list_t::iterator it = rit.base();
+ list->insert(it, 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())
+ vec->resize(priv->next_thread_id);
+ 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())
+ vec->resize(priv->next_thread_id);
+ (*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);
}
/**
*/
ClockVector * ModelExecution::get_cv(thread_id_t tid) const
{
- return get_parent_action(tid)->get_cv();
+ ModelAction *firstaction=get_parent_action(tid);
+ return firstaction != NULL ? firstaction->get_cv() : NULL;
}
bool valequals(uint64_t val1, uint64_t val2, int size) {
*/
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());
for (rit = list->rbegin();rit != list->rend();rit++) {
ModelAction *act = *rit;
- /* Only consider 'write' actions */
- if (!act->is_write() || act == curr)
+ if (act == curr)
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
/**
* @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;
/* Do not split atomic RMW */
if (curr->is_rmwr())
return get_thread(curr);
- if (curr->is_write()) {
- std::memory_order order = curr->get_mo();
- switch(order) {
- case std::memory_order_relaxed:
- return get_thread(curr);
- case std::memory_order_release:
- return get_thread(curr);
- default:
- return NULL;
- }
- }
-
/* Follow CREATE with the created thread */
/* which is not needed, because model.cc takes care of this */
if (curr->get_type() == THREAD_CREATE)
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