#include <stdio.h>
#include <algorithm>
+#include <mutex>
#include "model.h"
#include "action.h"
#include "cyclegraph.h"
#include "promise.h"
#include "datarace.h"
-#include "mutex.h"
#include "threads-model.h"
#define INITIAL_THREAD_ID 0
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>()),
+ condvar_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 *, SnapshotAlloc<Promise *> >()),
futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
delete obj_thrd_map;
delete obj_map;
delete lock_waiters_map;
+ delete condvar_waiters_map;
delete action_trace;
for (unsigned int i = 0; i < promises->size(); i++)
return ++priv->used_sequence_numbers;
}
+Node * ModelChecker::get_curr_node() {
+ return node_stack->get_head();
+}
+
/**
* @brief Choose the next thread to execute.
*
scheduler->update_sleep_set(prevnode);
/* Reached divergence point */
- if (nextnode->increment_promise()) {
+ if (nextnode->increment_misc()) {
+ /* The next node will try to satisfy a different misc_index values. */
+ tid = next->get_tid();
+ node_stack->pop_restofstack(2);
+ } else if (nextnode->increment_promise()) {
/* The next node will try to satisfy a different set of promises. */
tid = next->get_tid();
node_stack->pop_restofstack(2);
Thread *thr=get_thread(tid);
if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
ModelAction *pending_act=thr->get_pending();
- if (pending_act->could_synchronize_with(curr)) {
+ if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) {
//Remove this thread from sleep set
scheduler->remove_sleep(thr);
}
}
break;
}
+ case ATOMIC_WAIT: {
+ /* 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->same_thread(prev)&&prev->is_failed_trylock())
+ return prev;
+ if (!act->same_thread(prev)&&prev->is_notify())
+ return prev;
+ }
+ break;
+ }
+
+ case ATOMIC_NOTIFY_ALL:
+ case ATOMIC_NOTIFY_ONE: {
+ /* 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->same_thread(prev)&&prev->is_wait())
+ return prev;
+ }
+ break;
+ }
default:
break;
}
*/
bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
{
- uint64_t value;
+ uint64_t value = VALUE_NONE;
bool updated = false;
while (true) {
const ModelAction *reads_from = curr->get_node()->get_read_from();
* @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;
waiters->clear();
break;
}
+ case ATOMIC_WAIT: {
+ //unlock the lock
+ state->islocked = false;
+ //wake up the other threads
+ action_list_t *waiters = lock_waiters_map->get_safe_ptr((void *) curr->get_value());
+ //activate all the waiting threads
+ for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+ scheduler->wake(get_thread(*rit));
+ }
+ waiters->clear();
+ //check whether we should go to sleep or not...simulate spurious failures
+ if (curr->get_node()->get_misc()==0) {
+ condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
+ //disable us
+ scheduler->sleep(get_current_thread());
+ }
+ break;
+ }
+ case ATOMIC_NOTIFY_ALL: {
+ action_list_t *waiters = condvar_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++) {
+ scheduler->wake(get_thread(*rit));
+ }
+ waiters->clear();
+ break;
+ }
+ case ATOMIC_NOTIFY_ONE: {
+ action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location());
+ int wakeupthread=curr->get_node()->get_misc();
+ action_list_t::iterator it = waiters->begin();
+ advance(it, wakeupthread);
+ scheduler->wake(get_thread(*it));
+ waiters->erase(it);
+ break;
+ }
+
default:
ASSERT(0);
}
compute_promises(newcurr);
else if (newcurr->is_relseq_fixup())
compute_relseq_breakwrites(newcurr);
+ else if (newcurr->is_wait())
+ newcurr->get_node()->set_misc_max(2);
+ else if (newcurr->is_notify_one()) {
+ newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
+ }
}
return newcurr;
}
ModelAction *newcurr = initialize_curr_action(curr);
- wake_up_sleeping_actions(curr);
+ wake_up_sleeping_actions(newcurr);
/* Add the action to lists before any other model-checking tasks */
if (!second_part_of_rmw)
Node *parnode = currnode->get_parent();
if ((!parnode->backtrack_empty() ||
+ !currnode->misc_empty() ||
!currnode->read_from_empty() ||
!currnode->future_value_empty() ||
!currnode->promise_empty() ||
return true;
}
-/** Arbitrary reads from the future are not allowed. Section 29.3
- * part 9 places some constraints. This method checks one result of constraint
- * constraint. Others require compiler support. */
-bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
+/**
+ * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
+ * some constraints. This method checks one the following constraint (others
+ * require compiler support):
+ *
+ * If X --hb-> Y --mo-> Z, then X should not read from Z.
+ */
+bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
+{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+ unsigned int i;
- //Get write that follows reader action
- action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
- action_list_t::reverse_iterator rit;
- ModelAction *first_write_after_read=NULL;
-
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
- if (act==reader)
- break;
- if (act->is_write())
- first_write_after_read=act;
- }
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ ModelAction *write_after_read = NULL;
- if (first_write_after_read==NULL)
- return true;
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
- return !mo_graph->checkReachable(first_write_after_read, writer);
-}
+ if (!reader->happens_before(act))
+ break;
+ else if (act->is_write())
+ write_after_read = act;
+ }
+ if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+ return false;
+ }
+ return true;
+}
/**
* Finds the head(s) of the release sequence(s) containing a given ModelAction.
continue;
}
- /* Only writes can break release sequences */
- if (!act->is_write())
+ /* Only non-RMW writes can break release sequences */
+ if (!act->is_write() || act->is_rmw())
continue;
/* Check modification order */
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;
+ }
}
/**
/* 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;
}
act->is_read() &&
!act->could_synchronize_with(curr) &&
!act->same_thread(curr) &&
+ act->get_location() == curr->get_location() &&
promise->get_value() == curr->get_value()) {
curr->get_node()->set_promise(i);
}
if (!initialized) {
/** @todo Need a more informative way of reporting errors. */
printf("ERROR: may read from uninitialized atomic\n");
+ set_assert();
}
if (DBG_ENABLED() || !initialized) {
curr->get_node()->print_may_read_from();
printf("End printing may_read_from\n");
}
-
- ASSERT(initialized);
}
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {