forgot to add two files...

bug fixes...

diff --git a/action.cc b/action.cc
index 57058921d95726fb5c8f305b5316e34a80e6d39d..16f2327e8dc73de1ef564747bb27ae8c54c639fd 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -187,6 +187,19 @@ bool ModelAction::is_seqcst() const
 
 bool ModelAction::same_var(const ModelAction *act) const
 {
+       if ( act->is_wait() || is_wait() ) {
+               if ( act->is_wait() && is_wait() ) {
+                       if ( ((void *)value) == ((void *)act->value) )
+                               return true;
+               } else if ( is_wait() ) {
+                       if ( ((void *)value) == act->location )
+                               return true;
+               } else if ( act->is_wait() ) {
+                       if ( location == ((void *)act->value) )
+                               return true;
+               }
+       }
+
        return location == act->location;
 }
 
@@ -244,6 +257,27 @@ bool ModelAction::could_synchronize_with(const ModelAction *act) const
        if (is_read() && is_acquire() && act->could_be_write() && act->is_release())
                return true;
 
+       //lock just released...we can grab lock
+       if ((is_lock() ||is_trylock()) && (act->is_unlock()||act->is_wait()))
+               return true;
+
+       //lock just acquired...we can fail to grab lock
+       if (is_trylock() && act->is_success_lock())
+               return true;
+
+       //other thread stalling on lock...we can release lock
+       if (is_unlock() && (act->is_trylock()||act->is_lock()))
+               return true;
+
+       if (is_trylock() && (act->is_unlock()||act->is_wait()))
+               return true;
+
+       if ( is_notify() && act->is_wait() )
+               return true;
+
+       if ( is_wait() && act->is_notify() )
+               return true;
+
        // Otherwise handle by reads_from relation
        return false;
 }
@@ -398,6 +432,15 @@ void ModelAction::print() const
        case ATOMIC_TRYLOCK:
                type_str = "trylock";
                break;
+       case ATOMIC_WAIT:
+               type_str = "wait";
+               break;
+       case ATOMIC_NOTIFY_ONE:
+               type_str = "notify one";
+               break;
+       case ATOMIC_NOTIFY_ALL:
+               type_str = "notify all";
+               break;
        default:
                type_str = "unknown type";
        }

diff --git a/conditionvariable.cc b/conditionvariable.cc
new file mode 100644 (file)
index 0000000..5bd0beb
--- /dev/null
+++ b/conditionvariable.cc
@@ -0,0 +1,26 @@
+#include <mutex>
+#include "model.h"
+#include "conditionvariable.h"
+
+
+namespace std {
+
+condition_variable::condition_variable() {
+               
+}
+
+void condition_variable::notify_one() {
+       model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ONE, std::memory_order_seq_cst, this));
+}
+
+void condition_variable::notify_all() {
+       model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ALL, std::memory_order_seq_cst, this));
+}
+
+void condition_variable::wait(mutex& lock) {
+       model->switch_to_master(new ModelAction(ATOMIC_WAIT, std::memory_order_seq_cst, this, (uint64_t) &lock));
+       //relock as a second action
+       lock.lock();
+}
+}
+

diff --git a/conditionvariable.h b/conditionvariable.h
new file mode 100644 (file)
index 0000000..d1db7ff
--- /dev/null
+++ b/conditionvariable.h
@@ -0,0 +1,23 @@
+#ifndef CONDITIONVARIABLE_H
+#define CONDITIONVARIABLE_H
+
+namespace std {
+       class mutex;
+
+       struct condition_variable_state {
+               int reserved;
+       };
+
+       class condition_variable {
+       public:
+               condition_variable();
+               ~condition_variable();
+               void notify_one();
+               void notify_all();
+               void wait(mutex& lock);
+               
+       private:
+               struct condition_variable_state state;
+       };
+}
+#endif

diff --git a/model.cc b/model.cc
index 101a5f0864cb6bc7472ee40e58e8b33b36d3f726..2aaa1c26dbea3ad9e78720683635a117d83243f1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -498,8 +498,17 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
  * @return True if synchronization was updated; false otherwise
  */
 bool ModelChecker::process_mutex(ModelAction *curr) {
-       std::mutex *mutex = (std::mutex *)curr->get_location();
-       struct std::mutex_state *state = mutex->get_state();
+       std::mutex *mutex=NULL;
+       struct std::mutex_state *state=NULL;
+
+       if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
+               mutex = (std::mutex *)curr->get_location();
+               state = mutex->get_state();
+       } else if(curr->is_wait()) {
+               mutex = (std::mutex *)curr->get_value();
+               state = mutex->get_state();
+       }
+
        switch (curr->get_type()) {
        case ATOMIC_TRYLOCK: {
                bool success = !state->islocked;
@@ -1657,6 +1666,20 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        if ((int)thrd_last_action->size() <= tid)
                thrd_last_action->resize(get_num_threads());
        (*thrd_last_action)[tid] = act;
+
+       if (act->is_wait()) {
+               void *mutex_loc=(void *) act->get_value();
+               obj_map->get_safe_ptr(mutex_loc)->push_back(act);
+       
+               std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
+               if (tid >= (int)vec->size())
+                       vec->resize(priv->next_thread_id);
+               (*vec)[tid].push_back(act);
+
+               if ((int)thrd_last_action->size() <= tid)
+                       thrd_last_action->resize(get_num_threads());
+               (*thrd_last_action)[tid] = act;
+       }
 }
 
 /**
@@ -1708,7 +1731,7 @@ ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
        /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++)
-               if ((*rit)->is_unlock())
+               if ((*rit)->is_unlock() || (*rit)->is_wait())
                        return *rit;
        return NULL;
 }