More code towards freeing old actions

diff --git a/execution.cc b/execution.cc
index 5aaabbcf00060a1ffe55cb77ad11f049037d7648..d84ebbb2d6da19b0ecc1d225ed2be2658386abe5 100644 (file)
--- 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<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;
+                       }
                }
        }
 

diff --git a/execution.h b/execution.h
index 1aaa9db3b79d7a280f689f935de3c27dcf334548..2d227d21361a24918a47720139bf8148166d6a01 100644 (file)
--- 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 17bc71c86a87783614ffe5200e68d54ff0fc12c1..e814f0efbd1bdf4444b9c0895d673b01df223458 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();

diff --git a/model.cc b/model.cc
index a934d0adcb7be451907d3141243f4239564743d2..7ae63b69334c1a35faae4d94a4dde0fcf5be4c7b 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

diff --git a/params.h b/params.h
index 2c007c631a4926ef5e5690e4ea39115c0bf87237..af49c6b0026fe7b17d451cd2a014925bbe140cf4 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;