More code towards freeing old actions
authorBrian Demsky <bdemsky@uci.edu>
Mon, 16 Dec 2019 22:41:08 +0000 (14:41 -0800)
committerBrian Demsky <bdemsky@uci.edu>
Mon, 16 Dec 2019 22:42:45 +0000 (14:42 -0800)
execution.cc
execution.h
main.cc
model.cc
params.h

index 5aaabbc..d84ebbb 100644 (file)
@@ -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<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) {
+               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<ModelAction*>* 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;
+                       }
                }
        }
 
index 1aaa9db..2d227d2 100644 (file)
@@ -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 17bc71c..e814f0e 100644 (file)
--- 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;i<registeredanalysis->size();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<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
index a934d0a..7ae63b6 100644 (file)
--- 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
index 2c007c6..af49c6b 100644 (file)
--- 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;