#define INITIAL_THREAD_ID 0
+#ifdef COLLECT_STAT
+static unsigned int atomic_load_count = 0;
+static unsigned int atomic_store_count = 0;
+static unsigned int atomic_rmw_count = 0;
+
+static unsigned int atomic_fence_count = 0;
+static unsigned int atomic_lock_count = 0;
+static unsigned int atomic_trylock_count = 0;
+static unsigned int atomic_unlock_count = 0;
+static unsigned int atomic_notify_count = 0;
+static unsigned int atomic_wait_count = 0;
+static unsigned int atomic_timedwait_count = 0;
+#endif
+
/**
* Structure for holding small ModelChecker members that should be snapshotted
*/
scheduler(scheduler),
thread_map(2), /* We'll always need at least 2 threads */
pthread_map(0),
- pthread_counter(1),
+ pthread_counter(2),
action_trace(),
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
+ obj_wr_thrd_map(),
+ obj_last_sc_map(),
mutex_map(),
+ cond_map(),
thrd_last_action(1),
thrd_last_fence_release(),
priv(new struct model_snapshot_members ()),
mo_graph(new CycleGraph()),
+#ifdef NEWFUZZER
fuzzer(new NewFuzzer()),
+#else
+ fuzzer(new Fuzzer()),
+#endif
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
add_thread(model_thread);
- fuzzer->register_engine(m->get_history(), this);
+ fuzzer->register_engine(m, this);
scheduler->register_engine(this);
#ifdef TLS
pthread_key_create(&pthreadkey, tlsdestructor);
return model->get_execution_number();
}
-static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
{
- action_list_t *tmp = hash->get(ptr);
+ SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
- tmp = new action_list_t();
+ tmp = new SnapVector<action_list_t>();
hash->put(ptr, tmp);
}
return tmp;
}
-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
+static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)
{
- SnapVector<action_list_t> *tmp = hash->get(ptr);
+ simple_action_list_t *tmp = hash->get(ptr);
if (tmp == NULL) {
- tmp = new SnapVector<action_list_t>();
+ tmp = new simple_action_list_t();
+ hash->put(ptr, tmp);
+ }
+ return tmp;
+}
+
+static SnapVector<simple_action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<simple_action_list_t> *, uintptr_t, 2> * hash, void * ptr)
+{
+ SnapVector<simple_action_list_t> *tmp = hash->get(ptr);
+ if (tmp == NULL) {
+ tmp = new SnapVector<simple_action_list_t>();
hash->put(ptr, tmp);
}
return tmp;
}
+/**
+ * When vectors of action lists are reallocated due to resize, the root address of
+ * action lists may change. Hence we need to fix the parent pointer of the children
+ * of root.
+ */
+static void fixup_action_list(SnapVector<action_list_t> * vec)
+{
+ for (uint i = 0;i < vec->size();i++) {
+ action_list_t * list = &(*vec)[i];
+ if (list != NULL)
+ list->fixupParent();
+ }
+}
+
+#ifdef COLLECT_STAT
+static inline void record_atomic_stats(ModelAction * act)
+{
+ switch (act->get_type()) {
+ case ATOMIC_WRITE:
+ atomic_store_count++;
+ break;
+ case ATOMIC_RMW:
+ atomic_load_count++;
+ break;
+ case ATOMIC_READ:
+ atomic_rmw_count++;
+ break;
+ case ATOMIC_FENCE:
+ atomic_fence_count++;
+ break;
+ case ATOMIC_LOCK:
+ atomic_lock_count++;
+ break;
+ case ATOMIC_TRYLOCK:
+ atomic_trylock_count++;
+ break;
+ case ATOMIC_UNLOCK:
+ atomic_unlock_count++;
+ break;
+ case ATOMIC_NOTIFY_ONE:
+ case ATOMIC_NOTIFY_ALL:
+ atomic_notify_count++;
+ break;
+ case ATOMIC_WAIT:
+ atomic_wait_count++;
+ break;
+ case ATOMIC_TIMEDWAIT:
+ atomic_timedwait_count++;
+ default:
+ return;
+ }
+}
+
+void print_atomic_accesses()
+{
+ model_print("atomic store count: %u\n", atomic_store_count);
+ model_print("atomic load count: %u\n", atomic_load_count);
+ model_print("atomic rmw count: %u\n", atomic_rmw_count);
+
+ model_print("atomic fence count: %u\n", atomic_fence_count);
+ model_print("atomic lock count: %u\n", atomic_lock_count);
+ model_print("atomic trylock count: %u\n", atomic_trylock_count);
+ model_print("atomic unlock count: %u\n", atomic_unlock_count);
+ model_print("atomic notify count: %u\n", atomic_notify_count);
+ model_print("atomic wait count: %u\n", atomic_wait_count);
+ model_print("atomic timedwait count: %u\n", atomic_timedwait_count);
+}
+#endif
/** @return a thread ID for a new Thread */
thread_id_t ModelExecution::get_next_id()
{
return ++priv->used_sequence_numbers;
}
+/** @return a sequence number for a new ModelAction */
+modelclock_t ModelExecution::get_curr_seq_num()
+{
+ return priv->used_sequence_numbers;
+}
+
/** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
void ModelExecution::restore_last_seq_num()
{
void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
{
for (unsigned int i = 0;i < get_num_threads();i++) {
- Thread *thr = get_thread(int_to_id(i));
- if (scheduler->is_sleep_set(thr)) {
+ thread_id_t tid = int_to_id(i);
+ Thread *thr = get_thread(tid);
+ if (scheduler->is_sleep_set(tid)) {
if (should_wake_up(curr, thr)) {
/* Remove this thread from sleep set */
scheduler->remove_sleep(thr);
add_normal_write_to_lists(act);
add_write_to_lists(act);
w_modification_order(act);
+#ifdef NEWFUZZER
model->get_history()->process_action(act, act->get_tid());
+#endif
return act;
}
* Processes a read model action.
* @param curr is the read model action to process.
* @param rf_set is the set of model actions we can possibly read from
- * @return True if processing this read updates the mo_graph.
+ * @return True if the read can be pruned from the thread map list.
*/
bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
{
}
// Remove writes that violate read modification order
- uint i = 0;
- while (i < rf_set->size()) {
- ModelAction * rf = (*rf_set)[i];
- if (!r_modification_order(curr, rf, NULL, NULL, true)) {
- (*rf_set)[i] = rf_set->back();
- rf_set->pop_back();
- } else
- i++;
- }
+ /*
+ uint i = 0;
+ while (i < rf_set->size()) {
+ ModelAction * rf = (*rf_set)[i];
+ if (!r_modification_order(curr, rf, NULL, NULL, true)) {
+ (*rf_set)[i] = rf_set->back();
+ rf_set->pop_back();
+ } else
+ i++;
+ }*/
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
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();
- curr->setThrdMapRef(NULL);
- }
- return true;
+ //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);
}
-
- ASSERT(false);
- /* TODO: Following code not needed anymore */
priorset->clear();
(*rf_set)[index] = rf_set->back();
rf_set->pop_back();
//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");
+
+ // TODO: lock count for recursive mutexes
state->locked = get_thread(curr);
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
break;
}
case ATOMIC_WAIT: {
- /* wake up the other threads */
- for (unsigned int i = 0;i < get_num_threads();i++) {
- Thread *t = get_thread(int_to_id(i));
- Thread *curr_thrd = get_thread(curr);
- if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
- scheduler->wake(t);
- }
+ //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
+ if (fuzzer->shouldWait(curr)) {
+ /* wake up the other threads */
+ for (unsigned int i = 0;i < get_num_threads();i++) {
+ Thread *t = get_thread(int_to_id(i));
+ Thread *curr_thrd = get_thread(curr);
+ if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+ scheduler->wake(t);
+ }
- /* unlock the lock - after checking who was waiting on it */
- state->locked = NULL;
+ /* unlock the lock - after checking who was waiting on it */
+ state->locked = NULL;
- if (fuzzer->shouldWait(curr)) {
- /* disable this thread */
- get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
+ /* remove old wait action and disable this thread */
+ simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+ for (sllnode<ModelAction *> * it = waiters->begin();it != NULL;it = it->getNext()) {
+ ModelAction * wait = it->getVal();
+ if (wait->get_tid() == curr->get_tid()) {
+ waiters->erase(it);
+ break;
+ }
+ }
+
+ waiters->push_back(curr);
scheduler->sleep(get_thread(curr));
}
}
case ATOMIC_TIMEDWAIT:
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...
-
+ //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...
+
+ // TODO: lock count for recursive mutexes
/* wake up the other threads */
for (unsigned int i = 0;i < get_num_threads();i++) {
Thread *t = get_thread(int_to_id(i));
break;
}
case ATOMIC_NOTIFY_ALL: {
- action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+ simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
//activate all the waiting threads
for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
scheduler->wake(get_thread(rit->getVal()));
break;
}
case ATOMIC_NOTIFY_ONE: {
- action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+ simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
if (waiters->size() != 0) {
Thread * thread = fuzzer->selectNotify(waiters);
scheduler->wake(thread);
* @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;
}
/**
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
synchronize(act, curr);
- break; // WL: to be add (modified)
+ break;
}
case THREADONLY_FINISH:
if (curr->is_lock()) {
cdsc::mutex *lock = curr->get_mutex();
struct cdsc::mutex_state *state = lock->get_state();
- if (state->locked)
+ if (state->locked) {
+ Thread *lock_owner = (Thread *)state->locked;
+ Thread *curr_thread = get_thread(curr);
+ if (lock_owner == curr_thread && state->type == PTHREAD_MUTEX_RECURSIVE) {
+ return true;
+ }
+
return false;
+ }
} else if (curr->is_thread_join()) {
Thread *blocking = curr->get_thread_operand();
if (!blocking->is_complete()) {
ModelAction * ModelExecution::check_current_action(ModelAction *curr)
{
ASSERT(curr);
- bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
bool newly_explored = initialize_curr_action(&curr);
DBG();
wake_up_sleeping_actions(curr);
SnapVector<ModelAction *> * rf_set = NULL;
+ bool canprune = false;
/* Build may_read_from set for newly-created actions */
- if (newly_explored && curr->is_read())
+ if (curr->is_read() && newly_explored) {
rf_set = build_may_read_from(curr);
-
- if (curr->is_read() && !second_part_of_rmw) {
- process_read(curr, rf_set);
+ canprune = process_read(curr, rf_set);
delete rf_set;
} else
ASSERT(rf_set == NULL);
- /* Add the action to lists */
- if (!second_part_of_rmw)
- add_action_to_lists(curr);
+ /* Add the action to lists if not the second part of a rmw */
+ if (newly_explored) {
+#ifdef COLLECT_STAT
+ record_atomic_stats(curr);
+#endif
+ add_action_to_lists(curr, canprune);
+ }
if (curr->is_write())
add_write_to_lists(curr);
*/
bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
- SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
+ SnapVector<ModelAction *> * priorset, bool * canprune)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
- unsigned int i;
ASSERT(curr->is_read());
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
int tid = curr->get_tid();
+
+ /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
+ if ((int)thrd_lists->size() <= tid) {
+ uint oldsize = thrd_lists->size();
+ thrd_lists->resize(priv->next_thread_id);
+ for(uint i = oldsize;i < priv->next_thread_id;i++)
+ new (&(*thrd_lists)[i]) action_list_t();
+
+ fixup_action_list(thrd_lists);
+ }
+
ModelAction *prev_same_thread = NULL;
/* Iterate over all threads */
- for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
+ for (unsigned int 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 (i != 0)
*act < *last_sc_fence_thread_local) {
if (mo_graph->checkReachable(rf, act))
return false;
- if (!check_only)
- priorset->push_back(act);
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 4 */
*act < *last_sc_fence_local) {
if (mo_graph->checkReachable(rf, act))
return false;
- if (!check_only)
- priorset->push_back(act);
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 6 */
*act < *last_sc_fence_thread_before) {
if (mo_graph->checkReachable(rf, act))
return false;
- if (!check_only)
- priorset->push_back(act);
+ priorset->push_back(act);
break;
}
}
if (act->is_write()) {
if (mo_graph->checkReachable(rf, act))
return false;
- if (!check_only)
- priorset->push_back(act);
+ priorset->push_back(act);
} else {
ModelAction *prevrf = act->get_reads_from();
if (!prevrf->equals(rf)) {
if (mo_graph->checkReachable(rf, prevrf))
return false;
- if (!check_only)
- priorset->push_back(prevrf);
+ priorset->push_back(prevrf);
} else {
if (act->get_tid() == curr->get_tid()) {
//Can prune curr from obj list
- if (!check_only)
- *canprune = true;
+ *canprune = true;
}
}
}
}
-/**
- * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
- * some constraints. This method checks one the following constraint (others
- * require compiler support):
- *
- * If X --hb-> Y --mo-> Z, then X should not read from Z.
- * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
- */
-bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
-{
- SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
- unsigned int i;
- /* Iterate over all threads */
- for (i = 0;i < thrd_lists->size();i++) {
- const ModelAction *write_after_read = NULL;
-
- /* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
- 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)
- break;
- else if (act->is_write())
- write_after_read = act;
- else if (act->is_read() && act->get_reads_from() != NULL)
- write_after_read = act->get_reads_from();
- }
-
- if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
- return false;
- }
- return true;
-}
-
/**
* Computes the clock vector that happens before propagates from this write.
*
//operation that isn't release
if (rf->get_last_fence_release()) {
if (vec == NULL)
- vec = rf->get_last_fence_release()->get_cv();
+ vec = new ClockVector(rf->get_last_fence_release()->get_cv(), NULL);
else
(vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
+ } else {
+ if (vec == NULL) {
+ if (rf->is_rmw()) {
+ vec = new ClockVector(NULL, NULL);
+ }
+ } else {
+ vec = new ClockVector(vec, NULL);
+ }
}
rf->set_rfcv(vec);
}
*
* @param act is the ModelAction to add.
*/
-void ModelExecution::add_action_to_lists(ModelAction *act)
+void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
{
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());
+ simple_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
- act->setTraceRef(action_trace.add_back(act));
+ action_trace.addAction(act);
// Update obj_thrd_map, a per location, per thread, order of actions
vec->resize(priv->next_thread_id);
for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
+
+ fixup_action_list(vec);
}
- act->setThrdMapRef((*vec)[tid].add_back(act));
+ if (!canprune && (act->is_read() || act->is_write()))
+ (*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));
-
- SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
- 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();
- }
- act->setThrdMapRef((*vec)[tid].add_back(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 NULL;
- }
+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 NULL;
- } 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 NULL;
- }
+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());
vec->resize(priv->next_thread_id);
for(uint i=oldsize;i<priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
+
+ fixup_action_list(vec);
}
- 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
- if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
+ if (lastact == NULL || lastact->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());
+ SnapVector<simple_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();
+ new (&(*vec)[i]) simple_action_list_t();
}
write->setActionRef((*vec)[tid].add_back(write));
}
ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
{
/* All fences should have location FENCE_LOCATION */
- action_list_t *list = obj_map.get(FENCE_LOCATION);
+ simple_action_list_t *list = obj_map.get(FENCE_LOCATION);
if (!list)
return NULL;
{
void *location = curr->get_location();
- action_list_t *list = obj_map.get(location);
+ simple_action_list_t *list = obj_map.get(location);
if (list == NULL)
return NULL;
*/
SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
{
- SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
+ SnapVector<simple_action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
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];
- sllnode<ModelAction *> * rit;
- for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
- ModelAction *act = rit->getVal();
-
- if (act == curr)
- continue;
+ if (thrd_lists != NULL)
+ for (i = 0;i < thrd_lists->size();i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ simple_action_list_t *list = &(*thrd_lists)[i];
+ sllnode<ModelAction *> * rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
+
+ if (act == curr)
+ continue;
- /* Don't consider more than one seq_cst write if we are a seq_cst read. */
- bool allow_read = true;
-
- if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
- allow_read = false;
-
- /* Need to check whether we will have two RMW reading from the same value */
- if (curr->is_rmwr()) {
- /* It is okay if we have a failing CAS */
- if (!curr->is_rmwrcas() ||
- valequals(curr->get_value(), act->get_value(), curr->getSize())) {
- //Need to make sure we aren't the second RMW
- CycleNode * node = mo_graph->getNode_noCreate(act);
- if (node != NULL && node->getRMW() != NULL) {
- //we are the second RMW
- allow_read = false;
+ /* Don't consider more than one seq_cst write if we are a seq_cst read. */
+ bool allow_read = true;
+
+ if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
+ allow_read = false;
+
+ /* Need to check whether we will have two RMW reading from the same value */
+ if (curr->is_rmwr()) {
+ /* It is okay if we have a failing CAS */
+ if (!curr->is_rmwrcas() ||
+ valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+ //Need to make sure we aren't the second RMW
+ CycleNode * node = mo_graph->getNode_noCreate(act);
+ if (node != NULL && node->getRMW() != NULL) {
+ //we are the second RMW
+ allow_read = false;
+ }
}
}
- }
- if (allow_read) {
- /* Only add feasible reads */
- rf_set->push_back(act);
- }
+ if (allow_read) {
+ /* Only add feasible reads */
+ rf_set->push_back(act);
+ }
- /* Include at most one act per-thread that "happens before" curr */
- if (act->happens_before(curr))
- break;
+ /* Include at most one act per-thread that "happens before" curr */
+ if (act->happens_before(curr))
+ break;
+ }
}
- }
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
}
+void ModelExecution::print_tail()
+{
+ model_print("Execution trace %d:\n", get_execution_number());
+
+ sllnode<ModelAction*> *it;
+
+ model_print("------------------------------------------------------------------------------------\n");
+ model_print("# t Action type MO Location Value Rf CV\n");
+ model_print("------------------------------------------------------------------------------------\n");
+
+ unsigned int hash = 0;
+
+ int length = 25;
+ int counter = 0;
+ SnapList<ModelAction *> list;
+ for (it = action_trace.end();it != NULL;it = it->getPrev()) {
+ if (counter > length)
+ break;
+
+ ModelAction * act = it->getVal();
+ list.push_front(act);
+ counter++;
+ }
+
+ 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->getVal()->hash());
+ }
+ model_print("HASH %u\n", hash);
+ model_print("------------------------------------------------------------------------------------\n");
+}
+
/**
* Add a Thread to the system for the first time. Should only be called once
* per thread.
* @return A Thread reference
*/
Thread * ModelExecution::get_pthread(pthread_t pid) {
+ // pid 1 is reserved for the main thread, pthread ids should start from 2
+ if (pid == 1)
+ return get_thread(pid);
+
union {
pthread_t p;
uint32_t v;
} x;
x.p = pid;
uint32_t thread_id = x.v;
- if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
- else return NULL;
+
+ if (thread_id < pthread_counter + 1)
+ return pthread_map[thread_id];
+ else
+ return NULL;
}
/**
Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
{
/* Do not split atomic RMW */
- if (curr->is_rmwr() && !paused_by_fuzzer(curr))
+ if (curr->is_rmwr())
return get_thread(curr);
/* Follow CREATE with the created thread */
/* which is not needed, because model.cc takes care of this */
return NULL;
}
-/** @param act A read atomic action */
-bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
-{
- ASSERT(act->is_read());
-
- // Actions paused by fuzzer have their sequence number reset to 0
- return act->get_seq_number() == 0;
-}
-
/**
* Takes the next step in the execution, if possible.
* @param curr The current step to take
ASSERT(curr);
/* Process this action in ModelHistory for records */
+#ifdef NEWFUZZER
model->get_history()->process_action( curr, curr->get_tid() );
-
+#endif
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
return action_select_next_thread(curr);
}
+/** This method removes references to an Action before we delete it. */
+
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());
+ simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
list->erase(listref);
}
} else if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
}
- } else if (act->is_write()) {
+ } 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());
+ SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
(*vec)[act->get_tid()].erase(listref);
}
+
+ //Clear it from last_sc_map
+ if (obj_last_sc_map.get(act->get_location()) == act) {
+ obj_last_sc_map.remove(act->get_location());
+ }
+
//Remove from Cyclegraph
mo_graph->freeAction(act);
}
}
+/** Computes clock vector that all running threads have already synchronized to. */
+
ClockVector * ModelExecution::computeMinimalCV() {
ClockVector *cvmin = NULL;
- for(unsigned int i = 0;i < thread_map.size();i++) {
+ //Thread 0 isn't a real thread, so skip it..
+ for(unsigned int i = 1;i < thread_map.size();i++) {
Thread * t = thread_map[i];
- if (t->get_state() == THREAD_COMPLETED)
+ if (t->is_complete())
continue;
thread_id_t tid = int_to_id(i);
ClockVector * cv = get_cv(tid);
return cvmin;
}
+
+/** Sometimes we need to remove an action that is the most recent in the thread. This happens if it is mo before action in other threads. In that case we need to create a replacement latest ModelAction */
+
+void ModelExecution::fixupLastAct(ModelAction *act) {
+ ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid()));
+ newact->set_seq_number(get_next_seq_num());
+ newact->create_cv(act);
+ newact->set_last_fence_release(act->get_last_fence_release());
+ add_action_to_lists(newact, false);
+}
+
+/** Compute which actions to free. */
+
void ModelExecution::collectActions() {
+ if (priv->used_sequence_numbers < params->traceminsize)
+ return;
+
//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
+ modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
+
+ //Next 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()) {
+ sllnode<ModelAction*> * it;
+ for (it = action_trace.begin();it != NULL;it=it->getNext()) {
ModelAction *act = it->getVal();
modelclock_t actseq = act->get_seq_number();
+
+ //See if we are done
+ if (actseq > maxtofree)
+ break;
+
thread_id_t act_tid = act->get_tid();
modelclock_t tid_clock = cvmin->getClock(act_tid);
- if (actseq <= tid_clock) {
+
+ //Free if it is invisible or we have set a flag to remove visible actions.
+ if (actseq <= tid_clock || params->removevisible) {
ModelAction * write;
if (act->is_write()) {
write = act;
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);
+ CycleNode * cn = mo_graph->getNode_noCreate(write);
+ if (cn != NULL) {
+ queue->push_back(cn);
+ 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()) {
+
+ //We may need to remove read actions in the window we don't delete to preserve correctness.
+
+ for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
+ ModelAction *act = it2->getVal();
+ //Do iteration early in case we delete the act
+ it2=it2->getPrev();
+ bool islastact = false;
+ ModelAction *lastact = get_last_action(act->get_tid());
+ if (act == lastact) {
+ Thread * th = get_thread(act);
+ islastact = !th->is_complete();
+ }
+
+ if (act->is_read()) {
+ if (act->get_reads_from()->is_free()) {
+ if (act->is_rmw()) {
+ //Weaken a RMW from a freed store to a write
+ act->set_type(ATOMIC_WRITE);
+ } else {
+ removeAction(act);
+ if (islastact) {
+ fixupLastAct(act);
+ }
+
+ delete act;
+ continue;
+ }
+ }
+ }
+ //If we don't delete the action, we should remove references to release fences
+
+ 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);
+ }
+ }
+ //Now we are in the window of old actions that we remove if possible
+ for (;it != NULL;) {
ModelAction *act = it->getVal();
- if (act->is_free()) {
- removeAction(act);
- delete act;
- } else if (act->is_read()) {
+ //Do iteration early since we may delete node...
+ it=it->getPrev();
+ bool islastact = false;
+ ModelAction *lastact = get_last_action(act->get_tid());
+ if (act == lastact) {
+ Thread * th = get_thread(act);
+ islastact = !th->is_complete();
+ }
+
+ 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);
+ if (act->is_rmw()) {
+ act->set_type(ATOMIC_WRITE);
+ } else {
+ removeAction(act);
+ if (islastact) {
+ fixupLastAct(act);
+ }
+ delete act;
+ continue;
}
}
+ } else if (act->is_free()) {
+ removeAction(act);
+ if (islastact) {
+ fixupLastAct(act);
+ }
+ delete act;
+ continue;
+ } else if (act->is_write()) {
+ //Do nothing with write that hasn't been marked to be freed
+ } else if (islastact) {
+ //Keep the last action for non-read/write actions
} else if (act->is_fence()) {
//Note that acquire fences can always be safely
//removed, but could incur extra overheads in
modelclock_t tid_clock = cvmin->getClock(act_tid);
if (actseq <= tid_clock) {
removeAction(act);
+ // Remove reference to act from thrd_last_fence_release
+ int thread_id = id_to_int( act->get_tid() );
+ if (thrd_last_fence_release[thread_id] == act) {
+ thrd_last_fence_release[thread_id] = NULL;
+ }
delete act;
+ continue;
}
} else {
- //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish
+ //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
//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
+ if(act->is_unlock() || act->is_wait()) {
+ ModelAction * lastlock = get_last_unlock(act);
+ if (lastlock != act) {
+ removeAction(act);
+ delete act;
+ continue;
+ }
+ } else if (act->is_create()) {
+ if (act->get_thread_operand()->is_complete()) {
+ removeAction(act);
+ delete act;
+ continue;
+ }
+ } else {
+ removeAction(act);
+ delete act;
+ continue;
+ }
+ }
+
+ //If we don't delete the action, we should remove references to release fences
+ 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);
}
}
delete queue;
}
-
-
Fuzzer * ModelExecution::getFuzzer() {
return fuzzer;
}
projects / c11tester.git / blobdiff