Redesign actionlist and change acquire fence
authorBrian Demsky <bdemsky@uci.edu>
Tue, 7 Apr 2020 07:05:48 +0000 (00:05 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Tue, 7 Apr 2020 07:05:48 +0000 (00:05 -0700)
14 files changed:
Makefile
action.cc
action.h
actionlist.cc [new file with mode: 0644]
actionlist.h [new file with mode: 0644]
classlist.h
config.h
execution.cc
execution.h
fuzzer.cc
model.h
stl-model.h
threads-model.h
threads.cc

index 4f83cd9..adb080d 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
           context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \
           sleeps.o history.o funcnode.o funcinst.o predicate.o printf.o newfuzzer.o \
-          concretepredicate.o waitobj.o hashfunction.o pipe.o
+          concretepredicate.o waitobj.o hashfunction.o pipe.o actionlist.o
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic -lpthread
index d656954..d90a94e 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -38,9 +38,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
-       trace_ref(NULL),
-       thrdmap_ref(NULL),
-       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -72,9 +69,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
-       trace_ref(NULL),
-       thrdmap_ref(NULL),
-       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -105,9 +99,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
-       trace_ref(NULL),
-       thrdmap_ref(NULL),
-       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -142,9 +133,6 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
-       trace_ref(NULL),
-       thrdmap_ref(NULL),
-       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -180,9 +168,6 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
-       trace_ref(NULL),
-       thrdmap_ref(NULL),
-       action_ref(NULL),
        value(value),
        type(type),
        order(order),
index 35368ef..c5ba6d7 100644 (file)
--- a/action.h
+++ b/action.h
@@ -192,12 +192,6 @@ public:
        /* to accomodate pthread create and join */
        Thread * thread_operand;
        void set_thread_operand(Thread *th) { thread_operand = th; }
-       void setTraceRef(sllnode<ModelAction *> *ref) { trace_ref = ref; }
-       void setThrdMapRef(sllnode<ModelAction *> *ref) { thrdmap_ref = ref; }
-       void setActionRef(sllnode<ModelAction *> *ref) { action_ref = ref; }
-       sllnode<ModelAction *> * getTraceRef() { return trace_ref; }
-       sllnode<ModelAction *> * getThrdMapRef() { return thrdmap_ref; }
-       sllnode<ModelAction *> * getActionRef() { return action_ref; }
 
        SNAPSHOTALLOC
 private:
@@ -233,9 +227,6 @@ private:
         */
        ClockVector *cv;
        ClockVector *rf_cv;
-       sllnode<ModelAction *> * trace_ref;
-       sllnode<ModelAction *> * thrdmap_ref;
-       sllnode<ModelAction *> * action_ref;
 
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;
diff --git a/actionlist.cc b/actionlist.cc
new file mode 100644 (file)
index 0000000..f859746
--- /dev/null
@@ -0,0 +1,248 @@
+#include "actionlist.h"
+#include "action.h"
+#include <string.h>
+#include "stl-model.h"
+#include <limits.h>
+
+actionlist::actionlist() :
+       _size(0)
+{
+}
+
+actionlist::~actionlist() {
+}
+
+allnode::allnode() :
+       count(0) {
+       bzero(children, sizeof(children));
+}
+
+allnode::~allnode() {
+       if (count != 0)
+               for(int i=0;i<ALLNODESIZE;i++) {
+                       if (children[i] != NULL && !(((uintptr_t) children[i]) & ISACT))
+                               delete children[i];
+               }
+}
+
+sllnode<ModelAction *> * allnode::findPrev(modelclock_t index) {
+       allnode * ptr = this;
+       modelclock_t increment = 1;
+       modelclock_t mask = ALLMASK;
+       int totalshift = 0;
+       index -= increment;
+
+       while(1) {
+               modelclock_t shiftclock = index >> totalshift;
+               modelclock_t currindex = shiftclock & ALLMASK;
+
+               //See if we went negative...
+               if (currindex != ALLMASK) {
+                       if (ptr->children[currindex] == NULL) {
+                               //need to keep searching at this level
+                               index -= increment;
+                               continue;
+                       } else {
+                               //found non-null...
+                               if (totalshift != 0)
+                                       ptr = ptr->children[currindex];
+                               //need to increment here...
+                               increment = increment >> ALLBITS;
+                               mask = mask >> ALLBITS;
+                               totalshift -= ALLBITS;
+                               break;
+                       }
+               }
+               //If we get here, we already did the decrement earlier...no need to decrement again
+               ptr = ptr->parent;
+               increment = increment << ALLBITS;
+               mask = mask << ALLBITS;
+               totalshift += ALLBITS;
+
+               if (increment == 0) {
+                       return NULL;
+               }
+       }
+
+       while(1) {
+               while(1) {
+                       modelclock_t shiftclock = index >> totalshift;
+                       modelclock_t currindex = shiftclock & ALLMASK;
+                       if (ptr->children[currindex] != NULL) {
+                               if (totalshift != 0) {
+                                       ptr = ptr->children[currindex];
+                               } else {
+                                       allnode * act = ptr->children[currindex];
+                                       sllnode<ModelAction *> * node = reinterpret_cast<sllnode<ModelAction *>*>(((uintptr_t)act) & ALLMASK);
+                                       return node;
+                               }
+                       }
+                       index -= increment;
+               }
+
+               increment = increment >> ALLBITS;
+               mask = mask >> ALLBITS;
+               totalshift -= ALLBITS;
+       }
+}
+
+void actionlist::addAction(ModelAction * act) {
+       _size++;
+       int shiftbits = MODELCLOCKBITS - ALLBITS;
+       modelclock_t clock = act->get_seq_number();
+
+       allnode * ptr = &root;
+       do {
+               int index = (clock >> shiftbits) & ALLMASK;
+               allnode * tmp = ptr->children[index];
+               if (shiftbits == 0) {
+                       sllnode<ModelAction *> * llnode = new sllnode<ModelAction *>();
+                       llnode->val = act;
+                       if (tmp == NULL) {
+                               ptr->children[index] = reinterpret_cast<allnode *>(((uintptr_t) llnode) | ISACT);
+                               sllnode<ModelAction *> * llnodeprev = ptr->findPrev(index);
+                               if (llnodeprev != NULL) {
+
+                                       llnode->next = llnodeprev->next;
+                                       llnode->prev = llnodeprev;
+
+                                       //see if we are the new tail
+                                       if (llnodeprev->next == NULL)
+                                               tail = llnode;
+                                       else
+                                               llnode->next->prev = llnode;
+
+                                       llnodeprev->next = llnode;
+                               } else {
+                                       //We are the begining
+                                       llnode->next = head;
+                                       llnode->prev = NULL;
+                                       if (head != NULL) {
+                                               head->prev = llnode;
+                                       } else {
+                                               //we are the first node
+                                               tail = llnode;
+                                       }
+
+                                       head = llnode;
+                               }
+                               //need to find next link
+                               ptr->count++;
+                       } else {
+                               //handle case where something else is here
+
+                               sllnode<ModelAction *> * llnodeprev = reinterpret_cast<sllnode<ModelAction *>*>(((uintptr_t) llnode) & ALLMASK);
+                               llnode->next = llnodeprev->next;
+                               llnode->prev = llnodeprev;
+                               llnode->next->prev = llnode;
+                               llnodeprev->next = llnode;
+                               ptr->children[index] = reinterpret_cast<allnode *>(((uintptr_t) llnode) | ISACT);
+                       }
+                       return;
+               } else if (tmp == NULL) {
+                       tmp = new allnode();
+                       ptr->children[index] = tmp;
+                       tmp->parent=ptr;
+                       ptr->count++;
+               }
+               shiftbits -= ALLBITS;
+               ptr = tmp;
+       } while(1);
+
+}
+
+void decrementCount(allnode * ptr) {
+       ptr->count--;
+       if (ptr->count == 0) {
+               if (ptr->parent != NULL) {
+                       for(uint i=0;i<ALLNODESIZE;i++) {
+                               if (ptr->parent->children[i]==ptr) {
+                                       ptr->parent->children[i] = NULL;
+                                       decrementCount(ptr->parent);
+                               }
+                       }
+               }
+               delete ptr;
+       }
+}
+
+void actionlist::removeAction(ModelAction * act) {
+       int shiftbits = MODELCLOCKBITS - ALLBITS;
+       modelclock_t clock = act->get_seq_number();
+       allnode * ptr = &root;
+       do {
+               int index = (clock >> shiftbits) & ALLMASK;
+               allnode * tmp = ptr->children[index];
+               if (shiftbits == 0) {
+                       if (tmp == NULL) {
+                               //not found
+                               return;
+                       } else {
+                               sllnode<ModelAction *> * llnode = reinterpret_cast<sllnode<ModelAction *> *>(((uintptr_t) tmp) & ALLMASK);
+                               bool first = true;
+                               do {
+                                       if (llnode->val == act) {
+                                               //found node to remove
+                                               sllnode<ModelAction *> * llnodeprev = llnode->prev;
+                                               sllnode<ModelAction *> * llnodenext = llnode->next;
+                                               if (llnodeprev != NULL) {
+                                                       llnodeprev->next = llnodenext;
+                                               } else {
+                                                       head = llnodenext;
+                                               }
+                                               if (llnodenext != NULL) {
+                                                       llnodenext->prev = llnodeprev;
+                                               } else {
+                                                       tail = llnodeprev;
+                                               }
+                                               if (first) {
+                                                       //see if previous node has same clock as us...
+                                                       if (llnodeprev->val->get_seq_number() == clock) {
+                                                               ptr->children[index] = reinterpret_cast<allnode *>(((uintptr_t)llnodeprev) | ISACT);
+                                                       } else {
+                                                               //remove ourselves and go up tree
+                                                               ptr->children[index] = NULL;
+                                                               decrementCount(ptr);
+                                                       }
+                                               }
+                                               delete llnode;
+                                               _size--;
+                                               return;
+                                       }
+                                       llnode = llnode->prev;
+                                       first = false;
+                               } while(llnode != NULL && llnode->val->get_seq_number() == clock);
+                               //node not found in list... no deletion
+                               return;
+                       }
+               } else if (tmp == NULL) {
+                       //not found
+                       return;
+               }
+               shiftbits -= ALLBITS;
+               ptr = tmp;
+       } while(1);
+}
+
+void actionlist::clear() {
+       for(uint i = 0;i < ALLNODESIZE;i++) {
+               if (root.children[i] != NULL) {
+                       delete root.children[i];
+                       root.children[i] = NULL;
+               }
+       }
+
+       while(head != NULL) {
+               sllnode<ModelAction *> *tmp=head->next;
+               delete head;
+               head = tmp;
+       }
+       tail=NULL;
+
+       root.count = 0;
+       _size = 0;
+}
+
+bool actionlist::isEmpty() {
+       return root.count == 0;
+}
diff --git a/actionlist.h b/actionlist.h
new file mode 100644 (file)
index 0000000..70f90eb
--- /dev/null
@@ -0,0 +1,52 @@
+#ifndef ACTIONLIST_H
+#define ACTIONLIST_H
+
+#include "classlist.h"
+#include "stl-model.h"
+
+#define ISACT 1
+#define ALLBITS 4
+#define ALLNODESIZE (1 << ALLBITS)
+#define ALLMASK ((1 << ALLBITS)-1)
+#define MODELCLOCKBITS 32
+
+class allnode;
+void decrementCount(allnode *);
+
+class allnode {
+public:
+       allnode();
+       ~allnode();
+       SNAPSHOTALLOC;
+
+private:
+       allnode * parent;
+       allnode * children[ALLNODESIZE];
+       int count;
+       sllnode<ModelAction *> * findPrev(modelclock_t index);
+       friend class actionlist;
+       friend void decrementCount(allnode *);
+};
+
+class actionlist {
+public:
+       actionlist();
+       ~actionlist();
+       void addAction(ModelAction * act);
+       void removeAction(ModelAction * act);
+       void clear();
+       bool isEmpty();
+       uint size() {return _size;}
+       sllnode<ModelAction *> * begin() {return head;}
+       sllnode<ModelAction *> * end() {return tail;}
+
+       SNAPSHOTALLOC;
+
+private:
+       allnode root;
+       sllnode<ModelAction *> * head;
+       sllnode<ModelAction* > * tail;
+
+       uint _size;
+};
+#endif
index ccbbbb1..71f5451 100644 (file)
@@ -22,11 +22,14 @@ class FuncInst;
 class Predicate;
 class ConcretePredicate;
 class WaitObj;
+class actionlist;
+
+#include "actionlist.h"
 
 struct model_snapshot_members;
 struct bug_message;
 
-typedef SnapList<ModelAction *> action_list_t;
+typedef actionlist action_list_t;
 typedef SnapList<uint32_t> func_id_list_t;
 typedef SnapList<FuncInst *> func_inst_list_t;
 
index 74c0c35..f86275a 100644 (file)
--- a/config.h
+++ b/config.h
@@ -54,7 +54,7 @@
 #define FORK_HANDLER_HACK
 
 /** Enable smart fuzzer */
-#define NEWFUZZER
+//#define NEWFUZZER
 
 /** Define semantics of volatile memory operations. */
 #define memory_order_volatile_load memory_order_acquire
index 97e5851..c37de41 100644 (file)
@@ -329,6 +329,10 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                        read_from(curr, rf);
                        get_thread(curr)->set_return_value(curr->get_return_value());
                        delete priorset;
+                       //Update acquire fence clock vector
+                       ClockVector * hbcv = get_hb_from_write(curr->get_reads_from());
+                       if (hbcv != NULL)
+                               get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
                        return canprune && (curr->get_type() == ATOMIC_READ);
                }
                priorset->clear();
@@ -400,7 +404,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                        state->locked = NULL;
 
                        /* disable this thread */
-                       get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
+                       get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr);
                        scheduler->sleep(get_thread(curr));
                }
 
@@ -469,7 +473,7 @@ void ModelExecution::process_write(ModelAction *curr)
  * @param curr The ModelAction to process
  * @return True if synchronization was updated
  */
-bool ModelExecution::process_fence(ModelAction *curr)
+void ModelExecution::process_fence(ModelAction *curr)
 {
        /*
         * fence-relaxed: no-op
@@ -479,36 +483,9 @@ bool ModelExecution::process_fence(ModelAction *curr)
         *   sequences
         * fence-seq-cst: MO constraints formed in {r,w}_modification_order
         */
-       bool updated = false;
        if (curr->is_acquire()) {
-               action_list_t *list = &action_trace;
-               sllnode<ModelAction *> * rit;
-               /* Find X : is_read(X) && X --sb-> curr */
-               for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
-                       ModelAction *act = rit->getVal();
-                       if (act == curr)
-                               continue;
-                       if (act->get_tid() != curr->get_tid())
-                               continue;
-                       /* Stop at the beginning of the thread */
-                       if (act->is_thread_start())
-                               break;
-                       /* Stop once we reach a prior fence-acquire */
-                       if (act->is_fence() && act->is_acquire())
-                               break;
-                       if (!act->is_read())
-                               continue;
-                       /* read-acquire will find its own release sequences */
-                       if (act->is_acquire())
-                               continue;
-
-                       /* Establish hypothetical release sequences */
-                       ClockVector *cv = get_hb_from_write(act->get_reads_from());
-                       if (cv != NULL && curr->get_cv()->merge(cv))
-                               updated = true;
-               }
+               curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
        }
-       return updated;
 }
 
 /**
@@ -1129,11 +1106,11 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
        int tid = id_to_int(act->get_tid());
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
                action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-               act->setActionRef(list->add_back(act));
+               list->addAction(act);
        }
 
        // Update action trace, a total order of all actions
-       act->setTraceRef(action_trace.add_back(act));
+       action_trace.addAction(act);
 
 
        // Update obj_thrd_map, a per location, per thread, order of actions
@@ -1145,7 +1122,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
                        new (&(*vec)[i]) action_list_t();
        }
        if (!canprune && (act->is_read() || act->is_write()))
-               act->setThrdMapRef((*vec)[tid].add_back(act));
+               (*vec)[tid].addAction(act);
 
        // Update thrd_last_action, the last action taken by each thread
        if ((int)thrd_last_action.size() <= tid)
@@ -1161,43 +1138,17 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
 
        if (act->is_wait()) {
                void *mutex_loc = (void *) act->get_value();
-               act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
+               get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
        }
 }
 
-sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *act) {
-       sllnode<ModelAction*> * rit = list->end();
-       modelclock_t next_seq = act->get_seq_number();
-       if (rit == NULL || (rit->getVal()->get_seq_number() <= next_seq))
-               return list->add_back(act);
-       else {
-               for(;rit != NULL;rit=rit->getPrev()) {
-                       if (rit->getVal()->get_seq_number() <= next_seq) {
-                               return list->insertAfter(rit, act);
-                       }
-               }
-               return list->add_front(act);
-       }
+void insertIntoActionList(action_list_t *list, ModelAction *act) {
+       list->addAction(act);
 }
 
-sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
-       sllnode<ModelAction*> * rit = list->end();
-       modelclock_t next_seq = act->get_seq_number();
-       if (rit == NULL) {
-               act->create_cv(NULL);
-               return list->add_back(act);
-       } else if (rit->getVal()->get_seq_number() <= next_seq) {
-               act->create_cv(rit->getVal());
-               return list->add_back(act);
-       } else {
-               for(;rit != NULL;rit=rit->getPrev()) {
-                       if (rit->getVal()->get_seq_number() <= next_seq) {
-                               act->create_cv(rit->getVal());
-                               return list->insertAfter(rit, act);
-                       }
-               }
-               return list->add_front(act);
-       }
+void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+       act->create_cv(NULL);
+       list->addAction(act);
 }
 
 /**
@@ -1211,7 +1162,7 @@ sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelA
 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 {
        int tid = id_to_int(act->get_tid());
-       act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
+       insertIntoActionListAndSetCV(&action_trace, act);
 
        // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
@@ -1221,7 +1172,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
                for(uint i=oldsize;i<priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
+       insertIntoActionList(&(*vec)[tid],act);
 
        ModelAction * lastact = thrd_last_action[tid];
        // Update thrd_last_action, the last action taken by each thrad
@@ -1239,7 +1190,7 @@ void ModelExecution::add_write_to_lists(ModelAction *write) {
                for(uint i=oldsize;i<priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       write->setActionRef((*vec)[tid].add_back(write));
+       (*vec)[tid].addAction(write);
 }
 
 /**
@@ -1542,7 +1493,7 @@ void ModelExecution::print_tail()
        int length = 25;
        int counter = 0;
        SnapList<ModelAction *> list;
-       for (it = action_trace.end(); it != NULL; it = it->getPrev()) {
+       for (it = action_trace.end();it != NULL;it = it->getPrev()) {
                if (counter > length)
                        break;
 
@@ -1697,36 +1648,22 @@ Thread * ModelExecution::take_step(ModelAction *curr)
 
 void ModelExecution::removeAction(ModelAction *act) {
        {
-               sllnode<ModelAction *> * listref = act->getTraceRef();
-               if (listref != NULL) {
-                       action_trace.erase(listref);
-               }
+               action_trace.removeAction(act);
        }
        {
-               sllnode<ModelAction *> * listref = act->getThrdMapRef();
-               if (listref != NULL) {
-                       SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
-                       (*vec)[act->get_tid()].erase(listref);
-               }
+               SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+               (*vec)[act->get_tid()].removeAction(act);
        }
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
-               sllnode<ModelAction *> * listref = act->getActionRef();
-               if (listref != NULL) {
-                       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-                       list->erase(listref);
-               }
+               action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+               list->removeAction(act);
        } else if (act->is_wait()) {
-               sllnode<ModelAction *> * listref = act->getActionRef();
-               if (listref != NULL) {
-                       void *mutex_loc = (void *) act->get_value();
-                       get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
-               }
+               void *mutex_loc = (void *) act->get_value();
+               get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
        } else if (act->is_free()) {
-               sllnode<ModelAction *> * listref = act->getActionRef();
-               if (listref != NULL) {
-                       SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
-                       (*vec)[act->get_tid()].erase(listref);
-               }
+               SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+               (*vec)[act->get_tid()].removeAction(act);
+
                //Clear it from last_sc_map
                if (obj_last_sc_map.get(act->get_location()) == act) {
                        obj_last_sc_map.remove(act->get_location());
index 722b864..7ca610c 100644 (file)
@@ -19,8 +19,6 @@
 #include <condition_variable>
 #include "classlist.h"
 
-typedef SnapList<ModelAction *> action_list_t;
-
 struct PendingFutureValue {
        PendingFutureValue(ModelAction *writer, ModelAction *reader) :
                writer(writer), reader(reader)
@@ -105,7 +103,7 @@ private:
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
        void process_write(ModelAction *curr);
-       bool process_fence(ModelAction *curr);
+       void process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
        void process_thread_action(ModelAction *curr);
        void read_from(ModelAction *act, ModelAction *rf);
index 371838d..c41af4a 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -23,7 +23,7 @@ Thread * Fuzzer::selectNotify(action_list_t * waiters) {
        while(random_index--)
                it=it->getNext();
        Thread *thread = model->get_thread(it->getVal());
-       waiters->erase(it);
+       waiters->removeAction(it->getVal());
        return thread;
 }
 
diff --git a/model.h b/model.h
index 62b227e..6347481 100644 (file)
--- a/model.h
+++ b/model.h
@@ -18,8 +18,6 @@
 #include "classlist.h"
 #include "snapshot-interface.h"
 
-typedef SnapList<ModelAction *> action_list_t;
-
 /** @brief Model checker execution stats */
 struct execution_stats {
        int num_total;  /**< @brief Total number of executions */
index d787a2d..611520f 100644 (file)
@@ -5,7 +5,6 @@
 #include "mymemory.h"
 typedef unsigned int uint;
 
-
 template<typename _Tp>
 class mllnode {
 public:
@@ -165,6 +164,8 @@ private:
        uint _size;
 };
 
+class actionlist;
+
 template<typename _Tp>
 class sllnode {
 public:
@@ -179,6 +180,7 @@ private:
        _Tp val;
        template<typename T>
        friend class SnapList;
+       friend class actionlist;
 };
 
 template<typename _Tp>
@@ -537,6 +539,15 @@ public:
                array[index] = item;
        }
 
+       void remove(type item) {
+               for(uint i = 0;i < _size;i++) {
+                       if (at(i) == item) {
+                               removeAt(i);
+                               return;
+                       }
+               }
+       }
+
        void removeAt(uint index) {
                for (uint i = index;(i + 1) < _size;i++) {
                        set(i, at(i + 1));
index e159697..f0b88bb 100644 (file)
@@ -102,6 +102,7 @@ public:
        bool is_model_thread() const { return model_thread; }
 
        void * get_stack_addr() { return stack; }
+       ClockVector * get_acq_fence_cv() { return acq_fence_cv; }
 
        friend void thread_startup();
 #ifdef TLS
@@ -137,6 +138,9 @@ private:
        /** @brief The parent Thread which created this Thread */
        Thread * const parent;
 
+       /** @brief Acquire fence cv */
+       ClockVector *acq_fence_cv;
+
        /** @brief The THREAD_CREATE ModelAction which created this Thread */
        ModelAction *creation;
 
index 8b55a91..a2d2ed1 100644 (file)
@@ -14,6 +14,7 @@
 #include "model.h"
 #include "execution.h"
 #include "schedule.h"
+#include "clockvector.h"
 
 #ifdef TLS
 #include <dlfcn.h>
@@ -359,6 +360,7 @@ void Thread::complete()
  */
 Thread::Thread(thread_id_t tid) :
        parent(NULL),
+       acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
        start_routine(NULL),
@@ -384,6 +386,7 @@ Thread::Thread(thread_id_t tid) :
  */
 Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread *parent) :
        parent(parent),
+       acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
        start_routine(func),
@@ -416,6 +419,7 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread
  */
 Thread::Thread(thread_id_t tid, thrd_t *t, void *(*func)(void *), void *a, Thread *parent) :
        parent(parent),
+       acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
        start_routine(NULL),
@@ -444,6 +448,8 @@ Thread::~Thread()
 {
        if (!is_complete())
                complete();
+
+       delete acq_fence_cv;
 }
 
 /** @return The thread_id_t corresponding to this Thread object. */