More bug fixes
authorroot <root@plrg-1.ics.uci.edu>
Thu, 26 Dec 2019 03:54:20 +0000 (19:54 -0800)
committerroot <root@plrg-1.ics.uci.edu>
Thu, 26 Dec 2019 03:54:20 +0000 (19:54 -0800)
action.cc
action.h
cyclegraph.cc
cyclegraph.h
execution.cc

index 814c7fb..16dcc5c 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -305,6 +305,11 @@ bool ModelAction::is_write() const
        return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == NONATOMIC_WRITE;
 }
 
+bool ModelAction::is_create() const
+{
+       return type == THREAD_CREATE || type == PTHREAD_CREATE;
+}
+
 bool ModelAction::is_free() const
 {
        return type == READY_FREE;
index 95167c4..2b4b414 100644 (file)
--- a/action.h
+++ b/action.h
@@ -136,6 +136,7 @@ public:
        bool is_trylock() const;
        bool is_unlock() const;
        bool is_wait() const;
+       bool is_create() const;
        bool is_notify() const;
        bool is_notify_one() const;
        bool is_success_lock() const;
index bb481e1..6c7e945 100644 (file)
@@ -297,6 +297,10 @@ void CycleGraph::freeAction(const ModelAction * act) {
                CycleNode *dst = cn->edges[i];
                dst->removeInEdge(cn);
        }
+       for(unsigned int i=0;i<cn->inedges.size();i++) {
+               CycleNode *src = cn->inedges[i];
+               src->removeEdge(cn);
+       }
        delete cn;
 }
 
@@ -325,6 +329,16 @@ void CycleNode::removeInEdge(CycleNode *src) {
        }
 }
 
+void CycleNode::removeEdge(CycleNode *dst) {
+       for(unsigned int i=0;i < edges.size();i++) {
+               if (edges[i] == dst) {
+                       edges[i] = edges[edges.size()-1];
+                       edges.pop_back();
+                       break;
+               }
+       }
+}
+
 /**
  * @param i The index of the edge to return
  * @returns The CycleNode edge indexed by i
index a7e2a11..716e811 100644 (file)
@@ -70,6 +70,7 @@ public:
        void clearRMW() { hasRMW = NULL; }
        ModelAction * getAction() const { return action; }
        void removeInEdge(CycleNode *src);
+       void removeEdge(CycleNode *dst);
        ~CycleNode();
 
        SNAPSHOTALLOC
index 4e4a6bb..1c03a97 100644 (file)
@@ -63,7 +63,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        thrd_last_fence_release(),
        priv(new struct model_snapshot_members ()),
        mo_graph(new CycleGraph()),
-       fuzzer(new NewFuzzer()),
+       fuzzer(new Fuzzer()),
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */
@@ -1823,6 +1823,11 @@ void ModelExecution::collectActions() {
                                        removeAction(act);
                                        delete act;
                                }
+                       } else if (act->is_create()) {
+                               if (act->get_thread_operand()->get_state()==THREAD_COMPLETED) {
+                                       removeAction(act);
+                                       delete act;
+                               }
                        } else {
                                removeAction(act);
                                delete act;