mo_graph(new CycleGraph()),
fuzzer(new Fuzzer()),
thrd_func_list(),
- thrd_func_inst_lists(),
+ thrd_func_act_lists(),
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
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;
}
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;
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())
if (!blocking->is_complete()) {
return false;
}
+ } else if (curr->is_sleep()) {
+ if (!fuzzer->shouldSleep(curr))
+ return false;
}
return true;
/* 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)
/* 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();
if (act == curr) {
/*
* 1) If RMW and it actually read from something, then we
/* 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)
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();
+ 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 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();
+ 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)
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
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();
+ 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) {
- action_list_t::reverse_iterator rit = list->rbegin();
+ sllnode<ModelAction*> * rit = list->end();
modelclock_t next_seq = act->get_seq_number();
- if (rit == list->rend() || (*rit)->get_seq_number() == next_seq)
+ if (rit == NULL || (rit->getVal()->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);
+ 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) {
- action_list_t::reverse_iterator rit = list->rbegin();
+ sllnode<ModelAction*> * rit = list->end();
modelclock_t next_seq = act->get_seq_number();
- if (rit == list->rend()) {
+ if (rit == NULL) {
act->create_cv(NULL);
- } else if ((*rit)->get_seq_number() == next_seq) {
- act->create_cv((*rit));
+ } else if (rit->getVal()->get_seq_number() == next_seq) {
+ act->create_cv(rit->getVal());
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);
+ for(;rit != NULL;rit=rit->getPrev()) {
+ if (rit->getVal()->get_seq_number() == next_seq) {
+ act->create_cv(rit->getVal());
+ list->insertAfter(rit, act);
break;
}
}
// 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();
+ 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);
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();
+ 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);
}
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;
}
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++) {
- ModelAction *act = *rit;
+ sllnode<ModelAction *> * rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
if (act == curr)
continue;
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*/
+ /* 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())
projects / c11tester.git / blobdiff