merge stuff

Merge branch 'master' into mutex

Conflicts:
	model.cc
	model.h

diff --git a/action.cc b/action.cc
index 801e548306b09b82581cbea4d5ee186e7b968c54..f7ca249f965e6b351cd9763f382f9c792d586182 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -27,6 +27,30 @@ ModelAction::~ModelAction()
                delete cv;
 }
 
+bool ModelAction::is_mutex_op() const {
+       return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
+}
+
+bool ModelAction::is_lock() const {
+       return type == ATOMIC_LOCK;
+}
+
+bool ModelAction::is_unlock() const {
+       return type == ATOMIC_UNLOCK;
+}
+
+bool ModelAction::is_trylock() const {
+       return type == ATOMIC_TRYLOCK;
+}
+
+bool ModelAction::is_success_lock() const {
+       return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
+}
+
+bool ModelAction::is_failed_trylock() const {
+       return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
+}
+
 bool ModelAction::is_read() const
 {
        return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW;
@@ -167,6 +191,13 @@ void ModelAction::create_cv(const ModelAction *parent)
                cv = new ClockVector(NULL, this);
 }
 
+void ModelAction::set_try_lock(bool obtainedlock) {
+       if (obtainedlock)
+               value=VALUE_TRYSUCCESS;
+       else
+               value=VALUE_TRYFAILED;
+}
+
 /** Update the model action's read_from action */
 void ModelAction::read_from(const ModelAction *act)
 {

diff --git a/action.h b/action.h
index 0e3f3d572792303444c2e4efa3cce73326135039..c5179bcfa81a77de58b79b5c57077a28d32cfb24 100644 (file)
--- a/action.h
+++ b/action.h
@@ -24,6 +24,8 @@ using std::memory_order_seq_cst;
                hence by iteself does not indicate no value. */
 
 #define VALUE_NONE 1234567890
+#define VALUE_TRYSUCCESS 1
+#define VALUE_TRYFAILED 0
 
 /** @brief Represents an action type, identifying one of several types of
  * ModelAction */
@@ -70,6 +72,13 @@ public:
        Node * get_node() const { return node; }
        void set_node(Node *n) { node = n; }
 
+       void set_try_lock(bool obtainedlock);
+       bool is_mutex_op() const;
+       bool is_lock() const;
+       bool is_trylock() const;
+       bool is_unlock() const;
+       bool is_success_lock() const;
+       bool is_failed_trylock() const;
        bool is_read() const;
        bool is_write() const;
        bool is_rmwr() const;

diff --git a/model.cc b/model.cc
index ec99b9a745de0960087e1f4a4bd33aafa82a920c..b539aba6beba1339231a4f0c10cbf2e996a76f0e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -11,6 +11,7 @@
 #include "cyclegraph.h"
 #include "promise.h"
 #include "datarace.h"
+#include "mutex.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -27,6 +28,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
+       lock_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
        obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
        promises(new std::vector<Promise *>()),
        futurevalues(new std::vector<struct PendingFutureValue>()),
@@ -55,6 +57,7 @@ ModelChecker::~ModelChecker()
 
        delete obj_thrd_map;
        delete obj_map;
+       delete lock_waiters_map;
        delete action_trace;
 
        for (unsigned int i = 0; i < promises->size(); i++)
@@ -118,12 +121,14 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 {
        thread_id_t tid;
 
-       /* Do not split atomic actions. */
-       if (curr->is_rmwr())
-               return thread_current();
-       /* The THREAD_CREATE action points to the created Thread */
-       else if (curr->get_type() == THREAD_CREATE)
-               return (Thread *)curr->get_location();
+       if (curr!=NULL) {
+               /* Do not split atomic actions. */
+               if (curr->is_rmwr())
+                       return thread_current();
+               /* The THREAD_CREATE action points to the created Thread */
+               else if (curr->get_type() == THREAD_CREATE)
+                       return (Thread *)curr->get_location();
+       }
 
        /* Have we completed exploring the preselected path? */
        if (diverge == NULL)
@@ -197,21 +202,33 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
        action_type type = act->get_type();
 
-       switch (type) {
-               case ATOMIC_READ:
-               case ATOMIC_WRITE:
-               case ATOMIC_RMW:
-                       break;
-               default:
-                       return NULL;
-       }
-       /* linear search: from most recent to oldest */
-       action_list_t *list = obj_map->get_safe_ptr(act->get_location());
-       action_list_t::reverse_iterator rit;
-       for (rit = list->rbegin(); rit != list->rend(); rit++) {
-               ModelAction *prev = *rit;
-               if (act->is_synchronizing(prev))
-                       return prev;
+       if (type==ATOMIC_READ||type==ATOMIC_WRITE||type==ATOMIC_RMW) {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (act->is_synchronizing(prev))
+                               return prev;
+               }
+       } else if (type==ATOMIC_LOCK||type==ATOMIC_TRYLOCK) {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (prev->is_success_lock())
+                               return prev;
+               }
+       } else if (type==ATOMIC_UNLOCK) {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (prev->is_failed_trylock())
+                               return prev;
+               }
        }
        return NULL;
 }
@@ -308,6 +325,46 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
        }
 }
 
+void ModelChecker::process_mutex(ModelAction *curr) {
+       std::mutex * mutex=(std::mutex *) curr->get_location();
+       struct std::mutex_state * state=mutex->get_state();
+       switch(curr->get_type()) {
+       case ATOMIC_TRYLOCK: {
+               bool success=!state->islocked;
+               curr->set_try_lock(success);
+               if (!success)
+                       break;
+       }
+               //otherwise fall into the lock case
+       case ATOMIC_LOCK: {
+               if (curr->get_cv()->getClock(state->alloc_tid)<=state->alloc_clock) {
+                       printf("Lock access before initialization\n");
+                       set_assert();
+               }
+               state->islocked=true;
+               ModelAction *unlock=get_last_unlock(curr);
+               //synchronize with the previous unlock statement
+               curr->synchronize_with(unlock);
+               break;
+       }
+       case ATOMIC_UNLOCK: {
+               //unlock the lock
+               state->islocked=false;
+               //wake up the other threads
+               action_list_t * waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
+               //activate all the waiting threads
+               for(action_list_t::iterator rit = waiters->begin(); rit!=waiters->end(); rit++) {
+                       add_thread(get_thread((*rit)->get_tid()));
+               }
+               waiters->clear();
+               break;
+       }
+       default:
+               ASSERT(0);
+       }
+}
+
+
 /**
  * Process a write ModelAction
  * @param curr The ModelAction to process
@@ -355,12 +412,14 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                return newcurr;
        }
 
-       newcurr = node_stack->explore_action(curr);
+       newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
        if (newcurr) {
                /* First restore type and order in case of RMW operation */
                if (curr->is_rmwr())
                        newcurr->copy_typeandorder(curr);
 
+               ASSERT(curr->get_location()==newcurr->get_location());
+
                /* Discard duplicate ModelAction; use action from NodeStack */
                delete curr;
 
@@ -380,6 +439,20 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
        return newcurr;
 }
 
+bool ModelChecker::check_action_enabled(ModelAction *curr) {
+       if (curr->is_lock()) {
+               std::mutex * lock=(std::mutex *) curr->get_location();
+               struct std::mutex_state * state = lock->get_state();
+               if (state->islocked) {
+                       //Stick the action in the appropriate waiting queue
+                       lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
+                       return false;
+               }
+       }
+
+       return true;
+}
+
 /**
  * This is the heart of the model checker routine. It performs model-checking
  * actions corresponding to a given "current action." Among other processes, it
@@ -398,6 +471,14 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
        bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
 
+       if (!check_action_enabled(curr)) {
+               //we'll make the execution look like we chose to run this action
+               //much later...when a lock is actually available to relese
+               remove_thread(get_current_thread());
+               get_current_thread()->set_pending(curr);
+               return get_next_thread(NULL);
+       }
+
        ModelAction *newcurr = initialize_curr_action(curr);
 
        /* Add the action to lists before any other model-checking tasks */
@@ -409,6 +490,15 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                build_reads_from_past(curr);
        curr = newcurr;
 
+       /* Add the action to lists before any other model-checking tasks */
+       if (!second_part_of_rmw)
+               add_action_to_lists(newcurr);
+
+       /* Build may_read_from set for newly-created actions */
+       if (curr == newcurr && curr->is_read())
+               build_reads_from_past(curr);
+       curr = newcurr;
+
        /* Thread specific actions */
        switch (curr->get_type()) {
        case THREAD_CREATE: {
@@ -463,6 +553,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        if (act->is_write() && process_write(act))
                                updated = true;
 
+                       if (act->is_mutex_op()) 
+                               process_mutex(act);
+
                        if (updated)
                                work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
                        break;
@@ -1141,10 +1234,11 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 
 ModelAction * ModelChecker::get_last_action(thread_id_t tid)
 {
-       int nthreads = get_num_threads();
-       if ((int)thrd_last_action->size() < nthreads)
-               thrd_last_action->resize(nthreads);
-       return (*thrd_last_action)[id_to_int(tid)];
+       int threadid=id_to_int(tid);
+       if (threadid<(int)thrd_last_action->size())
+               return (*thrd_last_action)[id_to_int(tid)];
+       else
+               return NULL;
 }
 
 /**
@@ -1167,6 +1261,18 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr)
        return NULL;
 }
 
+ModelAction * ModelChecker::get_last_unlock(ModelAction *curr)
+{
+       void *location = curr->get_location();
+       action_list_t *list = obj_map->get_safe_ptr(location);
+       /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
+       action_list_t::reverse_iterator rit;
+       for (rit = list->rbegin(); rit != list->rend(); rit++)
+               if ((*rit)->is_unlock())
+                       return *rit;
+       return NULL;
+}
+
 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
 {
        ModelAction *parent = get_last_action(tid);
@@ -1400,25 +1506,23 @@ int ModelChecker::switch_to_master(ModelAction *act)
  * @return Returns true (success) if a step was taken and false otherwise.
  */
 bool ModelChecker::take_step() {
-       Thread *curr, *next;
-
        if (has_asserted())
                return false;
 
-       curr = thread_current();
+       Thread * curr = thread_current();
        if (curr) {
                if (curr->get_state() == THREAD_READY) {
                        ASSERT(priv->current_action);
 
                        priv->nextThread = check_current_action(priv->current_action);
                        priv->current_action = NULL;
-                       if (!curr->is_blocked() && !curr->is_complete())
-                               scheduler->add_thread(curr);
+                       if (curr->is_blocked() || curr->is_complete())
+                               scheduler->remove_thread(curr);
                } else {
                        ASSERT(false);
                }
        }
-       next = scheduler->next_thread(priv->nextThread);
+       Thread * next = scheduler->next_thread(priv->nextThread);
 
        /* Infeasible -> don't take any more steps */
        if (!isfeasible())
@@ -1431,6 +1535,15 @@ bool ModelChecker::take_step() {
        /* next == NULL -> don't take any more steps */
        if (!next)
                return false;
+
+       if ( next->get_pending() != NULL ) {
+               //restart a pending action
+               set_current_action(next->get_pending());
+               next->set_pending(NULL);
+               next->set_state(THREAD_READY);
+               return true;
+       }
+
        /* Return false only if swap fails with an error */
        return (Thread::swap(&system_context, next) == 0);
 }

diff --git a/model.h b/model.h
index fd6e6c234f1c4d55e9a9a17ac652484f28be53b2..8d10d51e7e2138904ae415cf8fa11c06c959765e 100644 (file)
--- a/model.h
+++ b/model.h
@@ -117,6 +117,8 @@ private:
        ModelAction * initialize_curr_action(ModelAction *curr);
        bool process_read(ModelAction *curr, bool second_part_of_rmw);
        bool process_write(ModelAction *curr);
+       void process_mutex(ModelAction *curr);
+       bool check_action_enabled(ModelAction *curr);
 
        bool take_step();
 
@@ -133,6 +135,7 @@ private:
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid);
        ModelAction * get_last_seq_cst(ModelAction *curr);
+       ModelAction * get_last_unlock(ModelAction *curr);
        void build_reads_from_past(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
        void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
@@ -152,6 +155,10 @@ private:
         * to a trace of all actions performed on the object. */
        HashTable<const void *, action_list_t, uintptr_t, 4> *obj_map;
 
+       /** Per-object list of actions. Maps an object (i.e., memory location)
+        * to a trace of all actions performed on the object. */
+       HashTable<const void *, action_list_t, uintptr_t, 4> *lock_waiters_map;
+
        HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 > *obj_thrd_map;
        std::vector<Promise *> *promises;
        std::vector<struct PendingFutureValue> *futurevalues;

diff --git a/mutex.cc b/mutex.cc
index b31b20a8ed2f02446fd1c4fbea5965c65b2b6979..51315d94bbf3081959c4c59d1d4c6af727f4a7ea 100644 (file)
--- a/mutex.cc
+++ b/mutex.cc
@@ -1,12 +1,12 @@
 #include "mutex.h"
 #include "model.h"
 
-
 namespace std {
-mutex::mutex() :
-       owner(0), islocked(false)
-{
-
+mutex::mutex() {
+       state.islocked=false;
+       thread_id_t tid=thread_current()->get_id();
+       state.alloc_tid=tid;
+       state.alloc_clock=model->get_cv(tid)->getClock(tid);
 }
        
 void mutex::lock() {

diff --git a/mutex.h b/mutex.h
index 1c6c3f3624fc1f9f31b4fa8331a756ea1eebee34..828aae53f9e1d273900b776ab657907c87e3cd08 100644 (file)
--- a/mutex.h
+++ b/mutex.h
@@ -1,8 +1,15 @@
 #ifndef MUTEX_H
 #define MUTEX_H
 #include "threads.h"
+#include "clockvector.h"
 
 namespace std {
+       struct mutex_state {
+               bool islocked;
+               thread_id_t alloc_tid;
+               modelclock_t alloc_clock;
+       };
+
        class mutex {
        public:
                mutex();
@@ -10,9 +17,10 @@ namespace std {
                void lock();
                bool try_lock();
                void unlock();
+               struct mutex_state * get_state() {return &state;}
+               
        private:
-               thread_id_t owner;
-               bool islocked;
+               struct mutex_state state;
        };
 }
 #endif

diff --git a/nodestack.cc b/nodestack.cc
index 69f0b5f513640f5861c6c3bf117c73fc440c7da6..b79863e2abbcc443e76721360724cc1c800d9b61 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -32,11 +32,12 @@ Node::Node(ModelAction *act, Node *par, int nthreads, bool *enabled)
        if (act)
                act->set_node(this);
        enabled_array=(bool *)MYMALLOC(sizeof(bool)*num_threads);
-       if (enabled)
+       if (enabled != NULL)
                memcpy(enabled_array, enabled, sizeof(bool)*num_threads);
-       else 
+       else {
                for(int i=0;i<num_threads;i++)
                        enabled_array[i]=false;
+       }
 }
 
 /** @brief Node desctructor */
@@ -332,7 +333,7 @@ void NodeStack::print()
        printf("............................................\n");
 }
 
-ModelAction * NodeStack::explore_action(ModelAction *act, bool * enabled)
+ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
 {
        DBG();
 
@@ -347,7 +348,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act, bool * enabled)
 
        /* Record action */
        get_head()->explore_child(act);
-       node_list.push_back(new Node(act, get_head(), model->get_num_threads(), enabled));
+       node_list.push_back(new Node(act, get_head(), model->get_num_threads(), is_enabled));
        total_nodes++;
        iter++;
        return NULL;

diff --git a/nodestack.h b/nodestack.h
index 6cd8cfd30806c7463d6710e5251041bf4b64cd81..3262a569d0e5da24689c46c706752a3b718c9a69 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -120,7 +120,7 @@ class NodeStack {
 public:
        NodeStack();
        ~NodeStack();
-       ModelAction * explore_action(ModelAction *act, bool * enabled);
+       ModelAction * explore_action(ModelAction *act, bool * is_enabled);
        Node * get_head();
        Node * get_next();
        void reset_execution();

diff --git a/schedule.cc b/schedule.cc
index cbb4957a3e4a3865730679e8e816dfb51f636324..8883d2a9b82cccc78a47b62a14d05e0e64ee52a5 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -5,10 +5,28 @@
 
 /** Constructor */
 Scheduler::Scheduler() :
+       is_enabled(NULL),
+       enabled_len(0),
+       curr_thread_index(0),
        current(NULL)
 {
 }
 
+void Scheduler::set_enabled(Thread *t, bool enabled_status) {
+       int threadid=id_to_int(t->get_id());
+       if (threadid>=enabled_len) {
+               bool * new_enabled=(bool *)malloc(sizeof(bool)*(threadid+1));
+               memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(bool));
+               if (is_enabled != NULL) {
+                       memcpy(new_enabled, is_enabled, enabled_len*sizeof(bool));
+                       free(is_enabled);
+               }
+               is_enabled=new_enabled;
+               enabled_len=threadid+1;
+       }
+       is_enabled[threadid]=enabled_status;
+}
+
 /**
  * Add a Thread to the scheduler's ready list.
  * @param t The Thread to add
@@ -16,7 +34,7 @@ Scheduler::Scheduler() :
 void Scheduler::add_thread(Thread *t)
 {
        DEBUG("thread %d\n", t->get_id());
-       readyList.push_back(t);
+       set_enabled(t, true);
 }
 
 /**
@@ -27,8 +45,7 @@ void Scheduler::remove_thread(Thread *t)
 {
        if (current == t)
                current = NULL;
-       else
-               readyList.remove(t);
+       set_enabled(t, false);
 }
 
 /**
@@ -38,7 +55,7 @@ void Scheduler::remove_thread(Thread *t)
  */
 void Scheduler::sleep(Thread *t)
 {
-       remove_thread(t);
+       set_enabled(t, false);
        t->set_state(THREAD_BLOCKED);
 }
 
@@ -48,7 +65,7 @@ void Scheduler::sleep(Thread *t)
  */
 void Scheduler::wake(Thread *t)
 {
-       add_thread(t);
+       set_enabled(t, true);
        t->set_state(THREAD_READY);
 }
 
@@ -62,19 +79,25 @@ void Scheduler::wake(Thread *t)
  */
 Thread * Scheduler::next_thread(Thread *t)
 {
-       if (t != NULL) {
-               current = t;
-               readyList.remove(t);
-       } else if (readyList.empty()) {
-               t = NULL;
+       if ( t == NULL ) {
+               int old_curr_thread = curr_thread_index;
+               while(true) {
+                       curr_thread_index = (curr_thread_index+1) % enabled_len;
+                       if (is_enabled[curr_thread_index]) {
+                               t = model->get_thread(int_to_id(curr_thread_index));
+                               break;
+                       }
+                       if (curr_thread_index == old_curr_thread) {
+                               print();
+                               return NULL;
+                       }
+               }
        } else {
-               t = readyList.front();
-               current = t;
-               readyList.pop_front();
+               curr_thread_index = id_to_int(t->get_id());
        }
 
+       current = t;
        print();
-
        return t;
 }
 
@@ -96,9 +119,4 @@ void Scheduler::print() const
                DEBUG("Current thread: %d\n", current->get_id());
        else
                DEBUG("No current thread\n");
-       DEBUG("Num. threads in ready list: %zu\n", readyList.size());
-
-       std::list<Thread *, MyAlloc< Thread * > >::const_iterator it;
-       for (it = readyList.begin(); it != readyList.end(); it++)
-               DEBUG("In ready list: thread %d\n", (*it)->get_id());
 }

diff --git a/schedule.h b/schedule.h
index a7483e02340942cf773ea7a69c890d72b384f69a..fb4d082adc2dbe220baf49d8347fc70fe6c0d560 100644 (file)
--- a/schedule.h
+++ b/schedule.h
@@ -23,11 +23,15 @@ public:
        Thread * next_thread(Thread *t);
        Thread * get_current_thread() const;
        void print() const;
+       bool * get_enabled() { return is_enabled; };
 
        SNAPSHOTALLOC
 private:
        /** The list of available Threads that are not currently running */
-       std::list<Thread *> readyList;
+       bool * is_enabled;
+       int enabled_len;
+       int curr_thread_index;
+       void set_enabled(Thread *t, bool enabled_status);
 
        /** The currently-running Thread */
        Thread *current;

diff --git a/threads.cc b/threads.cc
index 7fa4507ee94397e7e092730567901de94cf07a46..39f049541d69184cc012bcd042f2400208863a3a 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -119,6 +119,7 @@ void Thread::complete()
  * @param a The parameter to pass to this function.
  */
 Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
+       pending(NULL),
        start_routine(func),
        arg(a),
        user_thread(t),

diff --git a/threads.h b/threads.h
index 87a21ef2633f46f14de70240f052bc50af2adcce..9456a22f2fe4942b1004a87794fa3474eaeab26b 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -84,6 +84,8 @@ public:
         */
        void push_wait_list(ModelAction *act) { wait_list.push_back(act); }
 
+       ModelAction * get_pending() { return pending; }
+       void set_pending(ModelAction *act) { pending = act; }
        /**
         * Remove one ModelAction from the waiting list
         * @return The ModelAction that was removed from the waiting list
@@ -102,6 +104,7 @@ private:
        Thread *parent;
        ModelAction *creation;
 
+       ModelAction *pending;
        void (*start_routine)(void *);
        void *arg;
        ucontext_t context;