model(m),
params(NULL),
scheduler(scheduler),
- action_trace(),
thread_map(2), /* We'll always need at least 2 threads */
pthread_map(0),
pthread_counter(1),
+ action_trace(),
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
priv(new struct model_snapshot_members ()),
mo_graph(new CycleGraph()),
fuzzer(new NewFuzzer()),
- thrd_func_list(),
- thrd_func_act_lists(),
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
add_thread(model_thread);
fuzzer->register_engine(m->get_history(), this);
scheduler->register_engine(this);
+#ifdef TLS
+ pthread_key_create(&pthreadkey, tlsdestructor);
+#endif
}
/** @brief Destructor */
*/
bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
{
- SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
+ SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
if (hasnonatomicstore) {
ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
- if (index == -1)// no feasible write exists
- return false;
ModelAction *rf = (*rf_set)[index];
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();
+ curr->setThrdMapRef(NULL);
}
return true;
}
ASSERT(false);
- /* Following code not needed anymore */
+ /* TODO: Following code not needed anymore */
priorset->clear();
(*rf_set)[index] = rf_set->back();
rf_set->pop_back();
wake_up_sleeping_actions(curr);
- /* Add uninitialized actions to lists */
- if (!second_part_of_rmw)
- add_uninit_action_to_lists(curr);
-
SnapVector<ModelAction *> * rf_set = NULL;
/* Build may_read_from set for newly-created actions */
if (newly_explored && curr->is_read())
if (curr->is_read() && !second_part_of_rmw) {
process_read(curr, rf_set);
delete rf_set;
-
-/* bool success = process_read(curr, rf_set);
- delete rf_set;
- if (!success)
- return curr; // Do not add action to lists
- */
} else
ASSERT(rf_set == NULL);
*/
bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
- SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
+ SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
if (!check_only)
priorset->push_back(act);
} else {
- const ModelAction *prevrf = act->get_reads_from();
+ ModelAction *prevrf = act->get_reads_from();
if (!prevrf->equals(rf)) {
if (mo_graph->checkReachable(rf, prevrf))
return false;
return vec;
}
-/**
- * Performs various bookkeeping operations for the current ModelAction when it is
- * the first atomic action occurred at its memory location.
- *
- * For instance, adds uninitialized action to the per-object, per-thread action vector
- * and to the action trace list of all thread actions.
- *
- * @param act is the ModelAction to process.
- */
-void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
-{
- int tid = id_to_int(act->get_tid());
- ModelAction *uninit = NULL;
- int uninit_id = -1;
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- if (list->empty() && act->is_atomic_var()) {
- 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 ((int)vec->size() <= uninit_id) {
- 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);
- }
-
- // Update action trace, a total order of all actions
- 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 ((int)vec->size() <= tid) {
- 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();
- }
- 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());
- if (uninit)
- thrd_last_action[uninit_id] = uninit;
-}
-
-
/**
* Performs various bookkeeping operations for the current ModelAction. For
* instance, adds action to the per-object, per-thread action vector and to the
void ModelExecution::add_action_to_lists(ModelAction *act)
{
int tid = id_to_int(act->get_tid());
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- list->push_back(act);
+ if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ act->setActionRef(list->add_back(act));
+ }
// Update action trace, a total order of all actions
- action_trace.push_back(act);
+ act->setTraceRef(action_trace.add_back(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());
for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- (*vec)[tid].push_back(act);
+ act->setThrdMapRef((*vec)[tid].add_back(act));
- // Update thrd_last_action, the last action taken by each thrad
+ // Update thrd_last_action, the last action taken by each thread
if ((int)thrd_last_action.size() <= tid)
thrd_last_action.resize(get_num_threads());
thrd_last_action[tid] = act;
if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
- get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
+ act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
if ((int)vec->size() <= tid) {
for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- (*vec)[tid].push_back(act);
+ act->setThrdMapRef((*vec)[tid].add_back(act));
}
}
-void insertIntoActionList(action_list_t *list, ModelAction *act) {
+sllnode<ModelAction *>* 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);
+ return list->add_back(act);
else {
for(;rit != NULL;rit=rit->getPrev()) {
if (rit->getVal()->get_seq_number() == next_seq) {
- list->insertAfter(rit, act);
- break;
+ return list->insertAfter(rit, act);
}
}
+ return NULL;
}
}
-void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+sllnode<ModelAction *>* 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);
+ return NULL;
} else if (rit->getVal()->get_seq_number() == next_seq) {
act->create_cv(rit->getVal());
- list->push_back(act);
+ return list->add_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;
+ return list->insertAfter(rit, act);
}
}
+ return NULL;
}
}
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);
+ act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, 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());
for(uint i=oldsize;i<priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- insertIntoActionList(&(*vec)[tid],act);
+ act->setThrdMapRef(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())
for(uint i=oldsize;i<priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- (*vec)[tid].push_back(write);
+ write->setActionRef((*vec)[tid].add_back(write));
}
/**
void *location = curr->get_location();
action_list_t *list = obj_map.get(location);
+ if (list == NULL)
+ return NULL;
+
/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
sllnode<ModelAction*>* rit;
for (rit = list->end();rit != NULL;rit=rit->getPrev())
return rf_set;
}
-/**
- * @brief Get an action representing an uninitialized atomic
- *
- * 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(ModelAction *curr) const
-{
- ModelAction *act = curr->get_uninit_action();
- if (!act) {
- act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
- curr->set_uninit_action(act);
- }
- act->create_cv(NULL);
- return act;
-}
-
static void print_list(action_list_t *list)
{
sllnode<ModelAction*> *it;
return action_select_next_thread(curr);
}
+void ModelExecution::removeAction(ModelAction *act) {
+ {
+ sllnode<ModelAction *> * listref = act->getTraceRef();
+ if (listref != NULL) {
+ action_trace.erase(listref);
+ }
+ }
+ {
+ sllnode<ModelAction *> * listref = act->getThrdMapRef();
+ if (listref != NULL) {
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ (*vec)[act->get_tid()].erase(listref);
+ }
+ }
+ if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
+ sllnode<ModelAction *> * listref = act->getActionRef();
+ if (listref != NULL) {
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ list->erase(listref);
+ }
+ } else if (act->is_wait()) {
+ sllnode<ModelAction *> * listref = act->getActionRef();
+ if (listref != NULL) {
+ void *mutex_loc = (void *) act->get_value();
+ get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
+ }
+ } else if (act->is_write()) {
+ sllnode<ModelAction *> * listref = act->getActionRef();
+ if (listref != NULL) {
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+ (*vec)[act->get_tid()].erase(listref);
+ }
+ //Remove from Cyclegraph
+ mo_graph->freeAction(act);
+ }
+}
+
+ClockVector * ModelExecution::computeMinimalCV() {
+ ClockVector *cvmin = NULL;
+ for(unsigned int i = 0;i < thread_map.size();i++) {
+ Thread * t = thread_map[i];
+ if (t->get_state() == THREAD_COMPLETED)
+ continue;
+ thread_id_t tid = int_to_id(i);
+ ClockVector * cv = get_cv(tid);
+ if (cvmin == NULL)
+ cvmin = new ClockVector(cv, NULL);
+ else
+ cvmin->minmerge(cv);
+ }
+ return cvmin;
+}
+
+void ModelExecution::collectActions() {
+ //Compute minimal clock vector for all live threads
+ ClockVector *cvmin = computeMinimalCV();
+ SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
+ //walk action trace... When we hit an action, see if it is
+ //invisible (e.g., earlier than the first before the minimum
+ //clock for the thread... if so erase it and all previous
+ //actions in cyclegraph
+ for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
+ ModelAction *act = it->getVal();
+ modelclock_t actseq = act->get_seq_number();
+ thread_id_t act_tid = act->get_tid();
+ modelclock_t tid_clock = cvmin->getClock(act_tid);
+ if (actseq <= tid_clock) {
+ ModelAction * write;
+ if (act->is_write()) {
+ write = act;
+ } else if (act->is_read()) {
+ write = act->get_reads_from();
+ } else
+ continue;
+
+ //Mark everything earlier in MO graph to be freed
+ queue->push_back(mo_graph->getNode_noCreate(write));
+ while(!queue->empty()) {
+ CycleNode * node = queue->back();
+ queue->pop_back();
+ for(unsigned int i=0;i<node->getNumInEdges();i++) {
+ CycleNode * prevnode = node->getInEdge(i);
+ ModelAction * prevact = prevnode->getAction();
+ if (prevact->get_type() != READY_FREE) {
+ prevact->set_free();
+ queue->push_back(prevnode);
+ }
+ }
+ }
+ }
+ }
+ for (sllnode<ModelAction*>* it = action_trace.end();it != NULL;it=it->getPrev()) {
+ ModelAction *act = it->getVal();
+ if (act->is_free()) {
+ removeAction(act);
+ delete act;
+ } else if (act->is_read()) {
+ if (act->get_reads_from()->is_free()) {
+ removeAction(act);
+ delete act;
+ } else {
+ const ModelAction *rel_fence =act->get_last_fence_release();
+ if (rel_fence != NULL) {
+ modelclock_t relfenceseq = rel_fence->get_seq_number();
+ thread_id_t relfence_tid = rel_fence->get_tid();
+ modelclock_t tid_clock = cvmin->getClock(relfence_tid);
+ //Remove references to irrelevant release fences
+ if (relfenceseq <= tid_clock)
+ act->set_last_fence_release(NULL);
+ }
+ }
+ } else if (act->is_fence()) {
+ //Note that acquire fences can always be safely
+ //removed, but could incur extra overheads in
+ //traversals. Removing them before the cvmin seems
+ //like a good compromise.
+
+ //Release fences before the cvmin don't do anything
+ //because everyone has already synchronized.
+
+ //Sequentially fences before cvmin are redundant
+ //because happens-before will enforce same
+ //orderings.
+
+ modelclock_t actseq = act->get_seq_number();
+ thread_id_t act_tid = act->get_tid();
+ modelclock_t tid_clock = cvmin->getClock(act_tid);
+ if (actseq <= tid_clock) {
+ removeAction(act);
+ delete act;
+ }
+ } else {
+ //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish
+ //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
+ //need to keep most recent unlock/wait for each lock
+ }
+ }
+
+ delete cvmin;
+ delete queue;
+}
+
+
+
Fuzzer * ModelExecution::getFuzzer() {
return fuzzer;
}
projects / c11tester.git / blobdiff