read_from(curr, rf);
get_thread(curr)->set_return_value(curr->get_return_value());
delete priorset;
+ //Update acquire fence clock vector
+ ClockVector * hbcv = get_hb_from_write(curr->get_reads_from());
+ if (hbcv != NULL)
+ get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
return canprune && (curr->get_type() == ATOMIC_READ);
}
priorset->clear();
state->locked = NULL;
/* disable this thread */
- get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
+ get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr);
scheduler->sleep(get_thread(curr));
}
* @param curr The ModelAction to process
* @return True if synchronization was updated
*/
-bool ModelExecution::process_fence(ModelAction *curr)
+void ModelExecution::process_fence(ModelAction *curr)
{
/*
* fence-relaxed: no-op
* sequences
* fence-seq-cst: MO constraints formed in {r,w}_modification_order
*/
- bool updated = false;
if (curr->is_acquire()) {
- action_list_t *list = &action_trace;
- sllnode<ModelAction *> * rit;
- /* Find X : is_read(X) && X --sb-> curr */
- 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;
- /* Stop at the beginning of the thread */
- if (act->is_thread_start())
- break;
- /* Stop once we reach a prior fence-acquire */
- if (act->is_fence() && act->is_acquire())
- break;
- if (!act->is_read())
- continue;
- /* read-acquire will find its own release sequences */
- if (act->is_acquire())
- continue;
-
- /* Establish hypothetical release sequences */
- ClockVector *cv = get_hb_from_write(act->get_reads_from());
- if (cv != NULL && curr->get_cv()->merge(cv))
- updated = true;
- }
+ curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
}
- return updated;
}
/**
int tid = id_to_int(act->get_tid());
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));
+ list->addAction(act);
}
// Update action trace, a total order of all actions
- act->setTraceRef(action_trace.add_back(act));
+ action_trace.addAction(act);
// Update obj_thrd_map, a per location, per thread, order of actions
new (&(*vec)[i]) action_list_t();
}
if (!canprune && (act->is_read() || act->is_write()))
- act->setThrdMapRef((*vec)[tid].add_back(act));
+ (*vec)[tid].addAction(act);
// Update thrd_last_action, the last action taken by each thread
if ((int)thrd_last_action.size() <= tid)
if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
- act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
+ get_safe_ptr_action(&obj_map, mutex_loc)->addAction(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))
- return list->add_back(act);
- else {
- for(;rit != NULL;rit=rit->getPrev()) {
- if (rit->getVal()->get_seq_number() <= next_seq) {
- return list->insertAfter(rit, act);
- }
- }
- return list->add_front(act);
- }
+void insertIntoActionList(action_list_t *list, ModelAction *act) {
+ list->addAction(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 list->add_back(act);
- } else if (rit->getVal()->get_seq_number() <= next_seq) {
- act->create_cv(rit->getVal());
- 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());
- return list->insertAfter(rit, act);
- }
- }
- return list->add_front(act);
- }
+void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+ act->create_cv(NULL);
+ list->addAction(act);
}
/**
void ModelExecution::add_normal_write_to_lists(ModelAction *act)
{
int tid = id_to_int(act->get_tid());
- act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
+ 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();
}
- act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
+ insertIntoActionList(&(*vec)[tid],act);
ModelAction * lastact = thrd_last_action[tid];
// Update thrd_last_action, the last action taken by each thrad
for(uint i=oldsize;i<priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- write->setActionRef((*vec)[tid].add_back(write));
+ (*vec)[tid].addAction(write);
}
/**
int length = 25;
int counter = 0;
SnapList<ModelAction *> list;
- for (it = action_trace.end(); it != NULL; it = it->getPrev()) {
+ for (it = action_trace.end();it != NULL;it = it->getPrev()) {
if (counter > length)
break;
void ModelExecution::removeAction(ModelAction *act) {
{
- sllnode<ModelAction *> * listref = act->getTraceRef();
- if (listref != NULL) {
- action_trace.erase(listref);
- }
+ action_trace.removeAction(act);
}
{
- 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);
- }
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ (*vec)[act->get_tid()].removeAction(act);
}
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);
- }
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ list->removeAction(act);
} 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);
- }
+ void *mutex_loc = (void *) act->get_value();
+ get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
} else if (act->is_free()) {
- 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);
- }
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+ (*vec)[act->get_tid()].removeAction(act);
+
//Clear it from last_sc_map
if (obj_last_sc_map.get(act->get_location()) == act) {
obj_last_sc_map.remove(act->get_location());
projects / c11tester.git / blobdiff