builds

diff --git a/Makefile b/Makefile
index b65830fa2ce0e222d04163c563ec33676aa997b6..ddc89cb2440926aaf0551084fe89c88a3e2bbdfa 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -8,9 +8,9 @@ LIB_SO=lib$(LIB_NAME).so
 USER_O=userprog.o
 USER_H=libthreads.h libatomic.h
 
-MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc
-MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o
-MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h
+MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc cyclegraph.cc
+MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o
+MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h cyclegraph.h hashtable.h
 
 SHMEM_CC=snapshot.cc malloc.c mymemory.cc
 SHMEM_O=snapshot.o malloc.o mymemory.o

diff --git a/cyclegraph.cc b/cyclegraph.cc
new file mode 100644 (file)
index 0000000..c1fea4f
--- /dev/null
+++ b/cyclegraph.cc
@@ -0,0 +1,59 @@
+#include "cyclegraph.h"
+
+CycleGraph::CycleGraph() {
+       hasCycles=false;
+}
+
+CycleNode * CycleGraph::getNode(ModelAction * action) {
+       CycleNode *node=actionToNode.get(action);
+       if (node==NULL) {
+               node=new CycleNode(action);
+               actionToNode.put(action, node);
+       }
+       return node;
+}
+
+void CycleGraph::addEdge(ModelAction *from, ModelAction *to) {
+       CycleNode *fromnode=getNode(from);
+       CycleNode *tonode=getNode(to);
+       if (!hasCycles) {
+               // Check for Cycles
+               hasCycles=checkReachable(fromnode, tonode);
+       }
+       fromnode->addEdge(tonode);
+}
+
+bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
+       std::vector<class CycleNode *> queue;
+       HashTable<class CycleNode *, class CycleNode *, uintptr_t, 4> discovered;
+       
+       queue.push_back(from);
+       discovered.put(from, from);
+       while(!queue.empty()) {
+               class CycleNode * node=queue.back();
+               queue.pop_back();
+               if (node==to)
+                       return true;
+               
+               for(unsigned int i=0;i<node->getEdges()->size();i++) {
+                       CycleNode *next=(*node->getEdges())[i];
+                       if (!discovered.contains(next)) {
+                               discovered.put(next,next);
+                               queue.push_back(next);
+                       }
+               }
+       }
+       return false;
+}
+
+CycleNode::CycleNode(ModelAction *modelaction) {
+       action=modelaction;
+}
+
+std::vector<class CycleNode *> * CycleNode::getEdges() {
+       return &edges;
+}
+
+void CycleNode::addEdge(CycleNode * node) {
+       edges.push_back(node);
+}

diff --git a/cyclegraph.h b/cyclegraph.h
new file mode 100644 (file)
index 0000000..ed53417
--- /dev/null
+++ b/cyclegraph.h
@@ -0,0 +1,37 @@
+#ifndef CYCLEGRAPH_H
+#define CYCLEGRAPH_H
+
+#include "hashtable.h"
+#include "action.h"
+#include <vector>
+
+class CycleNode;
+
+/** @brief A graph of Model Actions for tracking cycles. */
+class CycleGraph {
+ public:
+       CycleGraph();
+       void addEdge(ModelAction *from, ModelAction *to);
+       bool checkForCycles();
+
+ private:
+       CycleNode * getNode(ModelAction *);
+       HashTable<class ModelAction *, class CycleNode *, uintptr_t, 4> actionToNode;
+       bool checkReachable(CycleNode *from, CycleNode *to);
+       
+       bool hasCycles;
+
+};
+
+class CycleNode {
+ public:
+       CycleNode(ModelAction *action);
+       void addEdge(CycleNode * node);
+       std::vector<class CycleNode *> * getEdges();
+
+ private:
+       ModelAction *action;
+       std::vector<class CycleNode *> edges;
+};
+
+#endif

diff --git a/hashtable.h b/hashtable.h
index ee7dc19f932fcd08f8ba9b8b7f66a835ecd515f1..f372f9e7b96f0efb7f08d6574d768a6cc7cdf2db 100644 (file)
--- a/hashtable.h
+++ b/hashtable.h
@@ -11,12 +11,12 @@ template<typename _Key, typename _Val>
                struct hashlistnode<_Key,_Val> *next;
        };
 
-template<typename _Key, typename _Val, int _Shift>
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
        class HashTable {
  public:
-       HashTable(unsigned int initialcapacity, double factor) {
+       HashTable(unsigned int initialcapacity=1024, double factor=0.5) {
                // Allocate space for the hash table
-               table = calloc(initialcapacity, sizeof(struct hashlistnode<_Key,_Val> *));
+               table = (struct hashlistnode<_Key,_Val> **) calloc(initialcapacity, sizeof(struct hashlistnode<_Key,_Val> *));
                loadfactor = factor;
                capacity = initialcapacity;
                threshold = initialcapacity*loadfactor;
@@ -25,17 +25,38 @@ template<typename _Key, typename _Val, int _Shift>
        }
 
        ~HashTable() {
+               for(unsigned int i=0;i<capacity;i++) {
+                       struct hashlistnode<_Key,_Val> * bin = table[i];
+                       while(bin!=NULL) {
+                               struct hashlistnode<_Key,_Val> * next=bin->next;
+                               free(bin);
+                               bin=next;
+                       }
+               }
                free(table);
        }
+
+       void reset() {
+               for(int i=0;i<capacity;i++) {
+                       struct hashlistnode<_Key,_Val> * bin = table[i];
+                       while(bin!=NULL) {
+                               struct hashlistnode<_Key,_Val> * next=bin->next;
+                               free(bin);
+                               bin=next;
+                       }
+               }
+               memset(table, 0, capacity*sizeof(struct hashlistnode<_Key, _Val> *));
+               size=0;
+       }
        
-       void insert(_Key key, _Val val) {
+       void put(_Key key, _Val val) {
                if(size > threshold) {
                        //Resize
                        unsigned int newsize = capacity << 1;
                        resize(newsize);
                }
                
-               struct hashlistnode<_Key,_Val> *ptr = table[(key & mask)>>_Shift];
+               struct hashlistnode<_Key,_Val> *ptr = table[(((_KeyInt)key) & mask)>>_Shift];
                size++;
                struct hashlistnode<_Key,_Val> *search = ptr;
 
@@ -47,15 +68,15 @@ template<typename _Key, typename _Val, int _Shift>
                        search=search->next;
                }
 
-               struct hashlistnode<_Key,_Val> *newptr=malloc(sizeof(struct hashlistnode<_Key,_Val>));
+               struct hashlistnode<_Key,_Val> *newptr=(struct hashlistnode<_Key,_Val> *)malloc(sizeof(struct hashlistnode<_Key,_Val>));
                newptr->key=key;
                newptr->val=val;
                newptr->next=ptr;
-               table[(key&mask)>>_Shift]=newptr;
+               table[(((_KeyInt)key)&mask)>>_Shift]=newptr;
        }
 
        _Val get(_Key key) {
-               struct hashlistnode<_Key,_Val> *search = table[(key & mask)>>_Shift];
+               struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
                
                while(search!=NULL) {
                        if (search->key==key) {
@@ -65,13 +86,25 @@ template<typename _Key, typename _Val, int _Shift>
                }
                return (_Val)0;
        }
+
+       bool contains(_Key key) {
+               struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
+               
+               while(search!=NULL) {
+                       if (search->key==key) {
+                               return true;
+                       }
+                       search=search->next;
+               }
+               return false;
+       }
        
        void resize(unsigned int newsize) {
                struct hashlistnode<_Key,_Val> ** oldtable = table;
                struct hashlistnode<_Key,_Val> ** newtable;
                unsigned int oldcapacity = capacity;
                
-               if((newtable = calloc(newsize, sizeof(struct hashlistnode<_Key,_Val> *))) == NULL) {
+               if((newtable = (struct hashlistnode<_Key,_Val> **) calloc(newsize, sizeof(struct hashlistnode<_Key,_Val> *))) == NULL) {
                        printf("Calloc error %s %d\n", __FILE__, __LINE__);
                        exit(-1);
                }
@@ -88,8 +121,8 @@ template<typename _Key, typename _Val, int _Shift>
                                _Key key=bin->key;
                                struct hashlistnode<_Key, _Val> * next=bin->next;
                                
-                               unsigned int index = (key & mask) >>_Shift;
-                               struct hashlistnode<_Key, _Val> tmp=newtable[index];
+                               unsigned int index = (((_KeyInt)key) & mask) >>_Shift;
+                               struct hashlistnode<_Key, _Val> * tmp=newtable[index];
                                bin->next=tmp;
                                newtable[index]=bin;
                                bin = next;
@@ -102,7 +135,7 @@ template<typename _Key, typename _Val, int _Shift>
  private:
        struct hashlistnode<_Key,_Val> **table;
        unsigned int capacity;
-       _Key mask;
+       _KeyInt mask;
        unsigned int size;
        unsigned int threshold;
        double loadfactor;

diff --git a/model.cc b/model.cc
index 27b6cd6a9df24856be3c9b2cc712eb2972ae98f3..090528500e4d11c20ed63f852738b290c43559dd 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -258,6 +258,12 @@ void ModelChecker::check_current_action(void)
        add_action_to_lists(curr);
 }
 
+
+/**
+ * Adds an action to the per-object, per-thread action vector.
+ * @param act is the ModelAction to add.
+ */
+
 void ModelChecker::add_action_to_lists(ModelAction *act)
 {
        action_trace->push_back(act);

diff --git a/mymemory.cc b/mymemory.cc
index 2c5adc0a84324e045d66e33332472bd8f7fd56e2..88018e269093c531a67bde16d27de8a95d6d6305 100644 (file)
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -13,9 +13,6 @@ int howManyFreed = 0;
 static mspace sStaticSpace = NULL;
 #endif
 
-//SUBRAMANIAN!!! PLEASE FIX THE MALLOC/FREE/CALLOC/ETC FOR FORK-BASED APPROACH
-//YOU HAVE NOT DONE THIS!!!!!!!!!!!
-
 /** Non-snapshotting malloc for our use. */
 
 void *MYMALLOC(size_t size) {