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(this);
+ fuzzer->register_engine(m, this);
scheduler->register_engine(this);
#ifdef TLS
pthread_key_create(&pthreadkey, tlsdestructor);
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;
}
//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
/* unlock the lock - after checking who was waiting on it */
state->locked = NULL;
- /* disable this thread */
- get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
+ /* remove old wait action and disable this thread */
+ 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));
}
//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));
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()) {
for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- if (!canprune)
+ if (!canprune && (act->is_read() || act->is_write()))
act->setThrdMapRef((*vec)[tid].add_back(act));
// Update thrd_last_action, the last action taken by each thread
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))
+ 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) {
+ if (rit->getVal()->get_seq_number() <= next_seq) {
return list->insertAfter(rit, act);
}
}
- return NULL;
+ return list->add_front(act);
}
}
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) {
+ 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) {
+ if (rit->getVal()->get_seq_number() <= next_seq) {
act->create_cv(rit->getVal());
return list->insertAfter(rit, act);
}
}
- return NULL;
+ return list->add_front(act);
}
}
}
+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();
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;
//Thread 0 isn't a real thread, so skip it..
return cvmin;
}
-//Options...
-//How often to check for memory
-//How much of the trace to always keep
-//Whether to sacrifice completeness...i.e., remove visible writes
+
+/** 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();
- cvmin->print();
SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
thread_id_t act_tid = act->get_tid();
modelclock_t tid_clock = cvmin->getClock(act_tid);
+
+ //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()) {
}
}
}
- for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;it2=it2->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();
- if (act->is_read() && act->get_reads_from()->is_free()) {
- act->set_read_from(NULL);
+ //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();
//Do iteration early since we may delete node...
}
if (act->is_read()) {
- if (!islastact && act->get_reads_from()->is_free()) {
- removeAction(act);
- delete act;
- continue;
- }
- if (islastact && act->get_reads_from()->is_free()) {
- act->set_read_from(NULL);
- }
-
- 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->get_reads_from()->is_free()) {
+ if (act->is_rmw()) {
+ act->set_type(ATOMIC_WRITE);
+ } else {
+ removeAction(act);
+ if (islastact) {
+ fixupLastAct(act);
+ }
+ delete act;
+ continue;
+ }
}
- } else if (islastact) {
- 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()) {
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 cvmin;
delete queue;
}
-
-
Fuzzer * ModelExecution::getFuzzer() {
return fuzzer;
}
projects / c11tester.git / blobdiff