fix

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

Conflicts:
	model.cc

diff --git a/Makefile b/Makefile
index 53b0331f2a250f7a18af120f87929b4cee605fdd..a732cb763ad7a8dcf1ef9900ac4473921000163c 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ include common.mk
 OBJECTS = libthreads.o schedule.o model.o threads.o librace.o action.o \
          nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
          datarace.o impatomic.o cmodelint.o \
-         snapshot.o malloc.o mymemory.o common.o
+         snapshot.o malloc.o mymemory.o common.o mutex.o
 
 CPPFLAGS += -Iinclude -I. -rdynamic
 LDFLAGS = -ldl -lrt

diff --git a/action.h b/action.h
index 9fa7a91c3f93443714f54ec34b153c4d09a1c20b..0e3f3d572792303444c2e4efa3cce73326135039 100644 (file)
--- a/action.h
+++ b/action.h
@@ -40,7 +40,10 @@ typedef enum action_type {
        ATOMIC_RMWC,          /**< Convert an atomic RMW action into a READ */
        ATOMIC_INIT,          /**< Initialization of an atomic object (e.g.,
                               *   atomic_init()) */
-       ATOMIC_FENCE
+       ATOMIC_FENCE,
+       ATOMIC_LOCK,
+       ATOMIC_TRYLOCK,
+       ATOMIC_UNLOCK
 } action_type_t;
 
 /* Forward declaration */

diff --git a/mutex.cc b/mutex.cc
new file mode 100644 (file)
index 0000000..b31b20a
--- /dev/null
+++ b/mutex.cc
@@ -0,0 +1,25 @@
+#include "mutex.h"
+#include "model.h"
+
+
+namespace std {
+mutex::mutex() :
+       owner(0), islocked(false)
+{
+
+}
+       
+void mutex::lock() {
+  model->switch_to_master(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this));
+}
+       
+bool mutex::try_lock() {
+  model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
+  return thread_current()->get_return_value();
+}
+
+void mutex::unlock() {
+  model->switch_to_master(new ModelAction(ATOMIC_UNLOCK, std::memory_order_seq_cst, this));
+}
+
+}

diff --git a/mutex.h b/mutex.h
new file mode 100644 (file)
index 0000000..1c6c3f3
--- /dev/null
+++ b/mutex.h
@@ -0,0 +1,18 @@
+#ifndef MUTEX_H
+#define MUTEX_H
+#include "threads.h"
+
+namespace std {
+       class mutex {
+       public:
+               mutex();
+               ~mutex();
+               void lock();
+               bool try_lock();
+               void unlock();
+       private:
+               thread_id_t owner;
+               bool islocked;
+       };
+}
+#endif

diff --git a/nodestack.cc b/nodestack.cc
index 431baafbdce9809a2cb49ebcea30837182c852cf..69f0b5f513640f5861c6c3bf117c73fc440c7da6 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -17,7 +17,7 @@
  * @param nthreads The number of threads which exist at this point in the
  * execution trace.
  */
-Node::Node(ModelAction *act, Node *par, int nthreads)
+Node::Node(ModelAction *act, Node *par, int nthreads, bool *enabled)
        : action(act),
        parent(par),
        num_threads(nthreads),
@@ -31,6 +31,12 @@ Node::Node(ModelAction *act, Node *par, int nthreads)
 {
        if (act)
                act->set_node(this);
+       enabled_array=(bool *)MYMALLOC(sizeof(bool)*num_threads);
+       if (enabled)
+               memcpy(enabled_array, enabled, sizeof(bool)*num_threads);
+       else 
+               for(int i=0;i<num_threads;i++)
+                       enabled_array[i]=false;
 }
 
 /** @brief Node desctructor */
@@ -38,6 +44,7 @@ Node::~Node()
 {
        if (action)
                delete action;
+       MYFREE(enabled_array);
 }
 
 /** Prints debugging info for the ModelAction associated with this Node */
@@ -212,7 +219,8 @@ thread_id_t Node::get_next_backtrack()
 
 bool Node::is_enabled(Thread *t)
 {
-       return id_to_int(t->get_id()) < num_threads;
+       int thread_id=id_to_int(t->get_id());
+       return thread_id < num_threads && enabled_array[thread_id];
 }
 
 /**
@@ -324,7 +332,7 @@ void NodeStack::print()
        printf("............................................\n");
 }
 
-ModelAction * NodeStack::explore_action(ModelAction *act)
+ModelAction * NodeStack::explore_action(ModelAction *act, bool * enabled)
 {
        DBG();
 
@@ -339,7 +347,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 
        /* Record action */
        get_head()->explore_child(act);
-       node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
+       node_list.push_back(new Node(act, get_head(), model->get_num_threads(), enabled));
        total_nodes++;
        iter++;
        return NULL;

diff --git a/nodestack.h b/nodestack.h
index 6c9779497e71f96e0621b37e762fbb199bd0556c..6cd8cfd30806c7463d6710e5251041bf4b64cd81 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -44,7 +44,7 @@ struct future_value {
  */
 class Node {
 public:
-       Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1);
+       Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, bool *enabled_array = NULL);
        ~Node();
        /* return true = thread choice has already been explored */
        bool has_been_explored(thread_id_t tid);
@@ -93,6 +93,7 @@ private:
        std::vector< bool, MyAlloc<bool> > explored_children;
        std::vector< bool, MyAlloc<bool> > backtrack;
        int numBacktracks;
+       bool *enabled_array;
 
        /** The set of ModelActions that this the action at this Node may read
         *  from. Only meaningful if this Node represents a 'read' action. */
@@ -119,7 +120,7 @@ class NodeStack {
 public:
        NodeStack();
        ~NodeStack();
-       ModelAction * explore_action(ModelAction *act);
+       ModelAction * explore_action(ModelAction *act, bool * enabled);
        Node * get_head();
        Node * get_next();
        void reset_execution();