Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

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
new file mode 100644 (file)
index 0000000..f372f9e
--- /dev/null
+++ b/hashtable.h
@@ -0,0 +1,143 @@
+#ifndef HASHTABLE_H
+#define HASHTABLE_H
+
+#include <stdlib.h>
+#include <stdio.h>
+
+template<typename _Key, typename _Val>
+       struct hashlistnode {
+               _Key key;
+               _Val val;
+               struct hashlistnode<_Key,_Val> *next;
+       };
+
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
+       class HashTable {
+ public:
+       HashTable(unsigned int initialcapacity=1024, double factor=0.5) {
+               // Allocate space for the hash table
+               table = (struct hashlistnode<_Key,_Val> **) calloc(initialcapacity, sizeof(struct hashlistnode<_Key,_Val> *));
+               loadfactor = factor;
+               capacity = initialcapacity;
+               threshold = initialcapacity*loadfactor;
+               mask = (capacity << _Shift)-1;
+               size = 0; // Initial number of elements in the hash
+       }
+
+       ~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 put(_Key key, _Val val) {
+               if(size > threshold) {
+                       //Resize
+                       unsigned int newsize = capacity << 1;
+                       resize(newsize);
+               }
+               
+               struct hashlistnode<_Key,_Val> *ptr = table[(((_KeyInt)key) & mask)>>_Shift];
+               size++;
+               struct hashlistnode<_Key,_Val> *search = ptr;
+
+               while(search!=NULL) {
+                       if (search->key==key) {
+                               search->val=val;
+                               return;
+                       }
+                       search=search->next;
+               }
+
+               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[(((_KeyInt)key)&mask)>>_Shift]=newptr;
+       }
+
+       _Val get(_Key key) {
+               struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
+               
+               while(search!=NULL) {
+                       if (search->key==key) {
+                               return search->val;
+                       }
+                       search=search->next;
+               }
+               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 = (struct hashlistnode<_Key,_Val> **) calloc(newsize, sizeof(struct hashlistnode<_Key,_Val> *))) == NULL) {
+                       printf("Calloc error %s %d\n", __FILE__, __LINE__);
+                       exit(-1);
+               }
+               
+               table = newtable;          //Update the global hashtable upon resize()
+               capacity = newsize;
+               threshold = newsize * loadfactor;
+               mask = (newsize << _Shift)-1;
+               
+               for(unsigned int i = 0; i < oldcapacity; i++) {
+                       struct hashlistnode<_Key, _Val> * bin = oldtable[i];
+                       
+                       while(bin!=NULL) {
+                               _Key key=bin->key;
+                               struct hashlistnode<_Key, _Val> * next=bin->next;
+                               
+                               unsigned int index = (((_KeyInt)key) & mask) >>_Shift;
+                               struct hashlistnode<_Key, _Val> * tmp=newtable[index];
+                               bin->next=tmp;
+                               newtable[index]=bin;
+                               bin = next;
+                       }
+               }
+               
+               free(oldtable);            //Free the memory of the old hash table
+       }
+       
+ private:
+       struct hashlistnode<_Key,_Val> **table;
+       unsigned int capacity;
+       _KeyInt mask;
+       unsigned int size;
+       unsigned int threshold;
+       double loadfactor;
+};
+#endif

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);