From: Brian Demsky Date: Mon, 16 Dec 2019 22:41:08 +0000 (-0800) Subject: More code towards freeing old actions X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=0ab0cd9eb506f1c00fd753c4bec10fed64ef0e85 More code towards freeing old actions --- diff --git a/execution.cc b/execution.cc index 5aaabbcf..d84ebbb2 100644 --- a/execution.cc +++ b/execution.cc @@ -129,6 +129,12 @@ modelclock_t ModelExecution::get_next_seq_num() 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() { @@ -378,18 +384,19 @@ bool ModelExecution::process_mutex(ModelAction *curr) 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); scheduler->sleep(get_thread(curr)); @@ -399,7 +406,14 @@ bool ModelExecution::process_mutex(ModelAction *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... /* wake up the other threads */ for (unsigned int i = 0;i < get_num_threads();i++) { @@ -1693,20 +1707,33 @@ ClockVector * ModelExecution::computeMinimalCV() { 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 + void ModelExecution::collectActions() { //Compute minimal clock vector for all live threads ClockVector *cvmin = computeMinimalCV(); SnapVector * queue = new SnapVector(); - //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* it = action_trace.begin();it != NULL;it=it->getNext()) { + sllnode * 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) { + if (actseq <= tid_clock || params->removevisible) { ModelAction * write; if (act->is_write()) { write = act; @@ -1716,7 +1743,8 @@ void ModelExecution::collectActions() { continue; //Mark everything earlier in MO graph to be freed - queue->push_back(mo_graph->getNode_noCreate(write)); + CycleNode * cn = mo_graph->getNode_noCreate(write); + queue->push_back(cn); while(!queue->empty()) { CycleNode * node = queue->back(); queue->pop_back(); @@ -1731,7 +1759,7 @@ void ModelExecution::collectActions() { } } } - for (sllnode* it = action_trace.end();it != NULL;it=it->getPrev()) { + for (;it != NULL;it=it->getPrev()) { ModelAction *act = it->getVal(); if (act->is_free()) { removeAction(act); @@ -1775,6 +1803,16 @@ void ModelExecution::collectActions() { //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 + if(act->is_unlock() || act->is_wait()) { + ModelAction * lastlock = get_last_unlock(act); + if (lastlock != act) { + removeAction(act); + delete act; + } + } else { + removeAction(act); + delete act; + } } } diff --git a/execution.h b/execution.h index 1aaa9db3..2d227d21 100644 --- a/execution.h +++ b/execution.h @@ -89,7 +89,7 @@ public: void setFinished() {isfinished = true;} void restore_last_seq_num(); void collectActions(); - + modelclock_t get_curr_seq_num(); #ifdef TLS pthread_key_t getPthreadKey() {return pthreadkey;} #endif diff --git a/main.cc b/main.cc index 17bc71c8..e814f0ef 100644 --- a/main.cc +++ b/main.cc @@ -21,7 +21,9 @@ void param_defaults(struct model_params *params) { params->verbose = !!DBG_ENABLED(); params->maxexecutions = 10; - params->tracebound = 0; + params->traceminsize = 0; + params->checkthreshold = 500000; + params->removevisible = false; params->nofork = false; } @@ -52,9 +54,16 @@ static void print_usage(struct model_params *params) "-x, --maxexec=NUM Maximum number of executions.\n" " Default: %u\n" " -o help for a list of options\n" - "-n No fork\n\n", + "-n No fork\n" + "-m, --minsize=NUM Minimum number of actions to keep\n", + " Default: %u\n" + "-f, --freqfree=NUM Frequency to free actions\n" + " Default: %u\n" + "-r, --removevisible Free visible writes\n", params->verbose, - params->maxexecutions); + params->maxexecutions, + params->traceminsize, + params->checkthreshold); model_print("Analysis plugins:\n"); for(unsigned int i=0;isize();i++) { TraceAnalysis * analysis=(*registeredanalysis)[i]; @@ -79,13 +88,16 @@ bool install_plugin(char * name) { } void parse_options(struct model_params *params) { - const char *shortopts = "hnt:o:x:v::"; + const char *shortopts = "hrnt:o:x:v:m:f::"; const struct option longopts[] = { {"help", no_argument, NULL, 'h'}, {"verbose", optional_argument, NULL, 'v'}, {"analysis", required_argument, NULL, 't'}, {"options", required_argument, NULL, 'o'}, {"maxexecutions", required_argument, NULL, 'x'}, + {"minsize", required_argument, NULL, 'm'}, + {"freqfree", required_argument, NULL, 'f'}, + {"removevisible", no_argument, NULL, 'r'}, {0, 0, 0, 0} /* Terminator */ }; int opt, longindex; @@ -133,6 +145,15 @@ void parse_options(struct model_params *params) { if (install_plugin(optarg)) error = true; break; + case 'm': + params->traceminsize = atoi(optarg); + break; + case 'f': + params->checkthreshold = atoi(optarg); + break; + case 'r': + params->removevisible = true; + break; case 'o': { ModelVector * analyses = getInstalledTraceAnalysis(); diff --git a/model.cc b/model.cc index a934d0ad..7ae63b69 100644 --- a/model.cc +++ b/model.cc @@ -392,11 +392,19 @@ void ModelChecker::run() //Need to initial random number generator state to avoid resets on rollback char random_state[256]; initstate(423121, random_state, sizeof(random_state)); - + modelclock_t checkfree = params.checkthreshold; for(int exec = 0;exec < params.maxexecutions;exec++) { Thread * t = init_thread; do { + /* Check whether we need to free model actions. */ + + if (params.traceminsize != 0 && + execution->get_curr_seq_num() > checkfree) { + checkfree += params.checkthreshold; + execution->collectActions(); + } + /* * Stash next pending action(s) for thread(s). There * should only need to stash one thread's action--the diff --git a/params.h b/params.h index 2c007c63..af49c6b0 100644 --- a/params.h +++ b/params.h @@ -8,7 +8,9 @@ struct model_params { int maxexecutions; bool nofork; - unsigned int tracebound; + modelclock_t traceminsize; + modelclock_t checkthreshold; + bool removevisible; /** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */ int verbose;