More bug fixes

diff --git a/action.cc b/action.cc
index 814c7fb1be0f05df2e42725ef6fb7cd86c641b1c..16dcc5cde20afc4f5f3bf7a27d900fba52c5da0e 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;
 }
 
        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;
 bool ModelAction::is_free() const
 {
        return type == READY_FREE;

diff --git a/action.h b/action.h
index 95167c437a0ff91a6f05405ea6c810ad8d403f81..2b4b4141da042161dfe1db76f7b4573339b92001 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_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;
        bool is_notify() const;
        bool is_notify_one() const;
        bool is_success_lock() const;

diff --git a/cyclegraph.cc b/cyclegraph.cc
index bb481e1374c6ad19f91a9a9eb27828517b775919..6c7e945e98ee8e58ab0a73911f24b8484a935389 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -297,6 +297,10 @@ void CycleGraph::freeAction(const ModelAction * act) {
                CycleNode *dst = cn->edges[i];
                dst->removeInEdge(cn);
        }
                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;
 }
 
        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
 /**
  * @param i The index of the edge to return
  * @returns The CycleNode edge indexed by i

diff --git a/cyclegraph.h b/cyclegraph.h
index a7e2a115929066e03b5f0a018509f78e145d7c1f..716e811d64ea6ea4153572d6d9c485762b0988ef 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -70,6 +70,7 @@ public:
        void clearRMW() { hasRMW = NULL; }
        ModelAction * getAction() const { return action; }
        void removeInEdge(CycleNode *src);
        void clearRMW() { hasRMW = NULL; }
        ModelAction * getAction() const { return action; }
        void removeInEdge(CycleNode *src);

+       void removeEdge(CycleNode *dst);

        ~CycleNode();
 
        SNAPSHOTALLOC
        ~CycleNode();
 
        SNAPSHOTALLOC

diff --git a/execution.cc b/execution.cc
index 4e4a6bb28e9b8a1d885ddd78fd4023cec6893c2b..1c03a97a7fd84ebd94e62023dca558602e33d93e 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -63,7 +63,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        thrd_last_fence_release(),
        priv(new struct model_snapshot_members ()),
        mo_graph(new CycleGraph()),
        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 */
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */


@@ -1823,6 +1823,11 @@ void ModelExecution::collectActions() {
                                        removeAction(act);
                                        delete act;
                                }
                                        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;
                        } else {
                                removeAction(act);
                                delete act;