#include <algorithm>
#include <mutex>
#include <new>
+#include <stdarg.h>
#include "model.h"
#include "action.h"
#include "datarace.h"
#include "threads-model.h"
#include "output.h"
+#include "traceanalysis.h"
+#include "bugmessage.h"
#define INITIAL_THREAD_ID 0
ModelChecker *model;
-struct bug_message {
- bug_message(const char *str) {
- const char *fmt = " [BUG] %s\n";
- msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
- sprintf(msg, fmt, str);
- }
- ~bug_message() { if (msg) snapshot_free(msg); }
-
- char *msg;
- void print() { model_print("%s", msg); }
-
- SNAPSHOTALLOC
-};
-
/**
* Structure for holding small ModelChecker members that should be snapshotted
*/
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>()),
condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
obj_thrd_map(new HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4 >()),
promises(new SnapVector<Promise *>()),
thrd_last_action(new SnapVector<ModelAction *>(1)),
thrd_last_fence_release(new SnapVector<ModelAction *>()),
node_stack(new NodeStack()),
+ trace_analyses(new ModelVector<TraceAnalysis *>()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
{
delete obj_thrd_map;
delete obj_map;
- delete lock_waiters_map;
delete condvar_waiters_map;
delete action_trace;
delete thrd_last_action;
delete thrd_last_fence_release;
delete node_stack;
+ for (unsigned int i = 0; i < trace_analyses->size(); i++)
+ delete (*trace_analyses)[i];
+ delete trace_analyses;
delete scheduler;
delete mo_graph;
delete priv;
return tmp;
}
+action_list_t * ModelChecker::get_actions_on_obj(void * obj, thread_id_t tid) {
+ SnapVector<action_list_t> *wrv=obj_thrd_map->get(obj);
+ if (wrv==NULL)
+ return NULL;
+ unsigned int thread=id_to_int(tid);
+ if (thread < wrv->size())
+ return &(*wrv)[thread];
+ else
+ return NULL;
+}
+
+
/**
* Restores user program to initial state and resets all model-checker data
* structures.
DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
- /* Print all model-checker output before rollback */
- fflush(model_out);
-
/**
* FIXME: if we utilize partial rollback, we will need to free only
* those pending actions which were NOT pending before the rollback
return ++priv->used_sequence_numbers;
}
-Node * ModelChecker::get_curr_node() const
-{
- return node_stack->get_head();
-}
-
/**
* @brief Select the next thread to execute based on the curren action
*
* scheduler decide
*/
if (diverge == NULL)
- return scheduler->select_next_thread();
+ return scheduler->select_next_thread(node_stack->get_head());
/* Else, we are trying to replay an execution */
ModelAction *next = node_stack->get_next()->get_action();
scheduler->update_sleep_set(prevnode);
/* Reached divergence point */
- 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);
- } else if (nextnode->increment_read_from()) {
- /* The next node will read from a different value. */
- tid = next->get_tid();
- node_stack->pop_restofstack(2);
- } else if (nextnode->increment_relseq_break()) {
- /* The next node will try to resolve a release sequence differently */
+ if (nextnode->increment_behaviors()) {
+ /* Execute the same thread with a new behavior */
tid = next->get_tid();
node_stack->pop_restofstack(2);
} else {
}
DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
ASSERT(tid != THREAD_ID_T_NONE);
- return thread_map->get(id_to_int(tid));
+ return get_thread(id_to_int(tid));
}
/**
return blocking_threads;
}
-/**
- * Check if a Thread has entered a circular wait deadlock situation. This will
- * not check other threads for potential deadlock situations, and may miss
- * deadlocks involving WAIT.
- *
- * @param t The thread which may have entered a deadlock
- * @return True if this Thread entered a deadlock; false otherwise
- */
-bool ModelChecker::is_circular_wait(const Thread *t) const
-{
- for (Thread *waiting = t->waiting_on() ; waiting != NULL; waiting = waiting->waiting_on())
- if (waiting == t)
- return true;
- return false;
-}
-
/**
* Check if this is a complete execution. That is, have all thread completed
* execution (rather than exiting because sleep sets have forced a redundant
* @param msg Descriptive message for the bug (do not include newline char)
* @return True if bug is immediately-feasible
*/
-bool ModelChecker::assert_bug(const char *msg)
+bool ModelChecker::assert_bug(const char *msg, ...)
{
- priv->bugs.push_back(new bug_message(msg));
+ char str[800];
+
+ va_list ap;
+ va_start(ap, msg);
+ vsnprintf(str, sizeof(str), msg, ap);
+ va_end(ap);
+
+ priv->bugs.push_back(new bug_message(str));
if (isfeasibleprefix()) {
set_assert();
assert_bug("Deadlock detected");
checkDataRaces();
+ run_trace_analyses();
}
record_stats();
return true;
}
+/** @brief Run trace analyses on complete trace */
+void ModelChecker::run_trace_analyses() {
+ for (unsigned int i = 0; i < trace_analyses->size(); i++)
+ (*trace_analyses)[i]->analyze(action_trace);
+}
+
/**
* @brief Find the last fence-related backtracking conflict for a ModelAction
*
Node *node = prev->get_node()->get_parent();
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
int low_tid, high_tid;
if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
low_tid = id_to_int(act->get_tid());
if (i >= node->get_num_threads())
break;
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
/* Don't backtrack into a point where the thread is disabled or sleeping. */
if (node->enabled_status(tid) != THREAD_ENABLED)
continue;
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
if (unlock != NULL) {
- curr->synchronize_with(unlock);
+ synchronize(unlock, curr);
return true;
}
break;
}
+ case ATOMIC_WAIT:
case ATOMIC_UNLOCK: {
- //unlock the lock
- state->locked = NULL;
- //wake up the other threads
- action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, 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));
+ /* wake up the other threads */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *t = get_thread(int_to_id(i));
+ Thread *curr_thrd = get_thread(curr);
+ if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+ scheduler->wake(t);
}
- waiters->clear();
- break;
- }
- case ATOMIC_WAIT: {
- //unlock the lock
+
+ /* unlock the lock - after checking who was waiting on it */
state->locked = NULL;
- //wake up the other threads
- action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (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->is_wait())
+ break; /* The rest is only for ATOMIC_WAIT */
+
+ /* Should we go to sleep? (simulate spurious failures) */
if (curr->get_node()->get_misc() == 0) {
get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
- //disable us
+ /* disable us */
scheduler->sleep(get_thread(curr));
}
break;
*
* If one of the following is true:
* (a) there are no pending promises
- * (b) the reader is ordered after the latest Promise creation
+ * (b) the reader and writer do not cross any promises
* Then, it is safe to pass a future value back now.
*
* Otherwise, we must save the pending future value until (a) or (b) is true
bool ModelChecker::promises_may_allow(const ModelAction *writer,
const ModelAction *reader) const
{
- return promises->empty() ||
- *(promises->back()->get_reader(0)) < *reader;
+ if (promises->empty())
+ return true;
+ for(int i=promises->size()-1;i>=0;i--) {
+ ModelAction *pr=(*promises)[i]->get_reader(0);
+ //reader is after promise...doesn't cross any promise
+ if (*reader > *pr)
+ return true;
+ //writer is after promise, reader before...bad...
+ if (*writer > *pr)
+ return false;
+ }
+ return true;
}
/**
}
}
- if (promises->empty()) {
- for (unsigned int i = 0; i < futurevalues->size(); i++) {
- struct PendingFutureValue pfv = (*futurevalues)[i];
+ /* Check the pending future values */
+ for (int i = (int)futurevalues->size() - 1; i >= 0; i--) {
+ struct PendingFutureValue pfv = (*futurevalues)[i];
+ if (promises_may_allow(pfv.writer, pfv.reader)) {
add_future_value(pfv.writer, pfv.reader);
+ futurevalues->erase(futurevalues->begin() + i);
}
- futurevalues->clear();
}
mo_graph->commitChanges();
rel_heads_list_t release_heads;
get_release_seq_heads(curr, act, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!curr->synchronize_with(release_heads[i]))
- set_bad_synchronization();
+ synchronize(release_heads[i], curr);
if (release_heads.size() != 0)
updated = true;
}
case THREAD_JOIN: {
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
- curr->synchronize_with(act);
+ synchronize(act, curr);
updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_FINISH: {
Thread *th = get_thread(curr);
- while (!th->wait_list_empty()) {
- ModelAction *act = th->pop_wait_list();
- scheduler->wake(get_thread(act));
+ /* Wake up any joining threads */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *waiting = get_thread(int_to_id(i));
+ if (waiting->waiting_on() == th &&
+ waiting->get_pending()->is_thread_join())
+ scheduler->wake(waiting);
}
th->complete();
/* Completed thread can't satisfy promises */
*/
/* Must synchronize */
- if (!acquire->synchronize_with(release)) {
- set_bad_synchronization();
+ if (!synchronize(release, acquire))
return;
- }
/* Re-check all pending release sequences */
work_queue->push_back(CheckRelSeqWorkEntry(NULL));
/* Re-check act for mo_graph edges */
for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
if (acquire->happens_before(propagate)) {
- propagate->synchronize_with(acquire);
+ synchronize(acquire, propagate);
/* Re-check 'propagate' for mo_graph edges */
work_queue->push_back(MOEdgeWorkEntry(propagate));
}
get_release_seq_heads(act, act, &release_heads);
int num_heads = release_heads.size();
for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!act->synchronize_with(release_heads[i])) {
- set_bad_synchronization();
+ if (!synchronize(release_heads[i], act))
num_heads--;
- }
return num_heads > 0;
}
return false;
}
+/**
+ * @brief Synchronizes two actions
+ *
+ * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
+ * This function performs the synchronization as well as providing other hooks
+ * for other checks along with synchronization.
+ *
+ * @param first The left-hand side of the synchronizes-with relation
+ * @param second The right-hand side of the synchronizes-with relation
+ * @return True if the synchronization was successful (i.e., was consistent
+ * with the execution order); false otherwise
+ */
+bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second)
+{
+ if (*second < *first) {
+ set_bad_synchronization();
+ return false;
+ }
+ check_promises(first->get_tid(), second->get_cv(), first->get_cv());
+ return second->synchronize_with(first);
+}
+
/**
* Check promises and eliminate potentially-satisfying threads when a thread is
* blocked (e.g., join, lock). A thread which is waiting on another thread can
*/
bool ModelChecker::check_action_enabled(ModelAction *curr) {
if (curr->is_lock()) {
- std::mutex *lock = (std::mutex *)curr->get_location();
+ std::mutex *lock = curr->get_mutex();
struct std::mutex_state *state = lock->get_state();
- if (state->locked) {
- //Stick the action in the appropriate waiting queue
- get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
+ if (state->locked)
return false;
- }
- } else if (curr->get_type() == THREAD_JOIN) {
- Thread *blocking = (Thread *)curr->get_location();
+ } else if (curr->is_thread_join()) {
+ Thread *blocking = curr->get_thread_operand();
if (!blocking->is_complete()) {
- blocking->push_wait_list(curr);
thread_blocking_check_promises(blocking, get_thread(curr));
return false;
}
{
ASSERT(curr);
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
-
- if (!check_action_enabled(curr)) {
- /* Make the execution look like we chose to run this action
- * much later, when a lock/join can succeed */
- get_thread(curr)->set_pending(curr);
- scheduler->sleep(get_thread(curr));
- return NULL;
- }
-
bool newly_explored = initialize_curr_action(&curr);
DBG();
- if (DBG_ENABLED())
- curr->print();
wake_up_sleeping_actions(curr);
}
/**
- * Updates the mo_graph with the constraints imposed from the current
+ * @brief Updates the mo_graph with the constraints imposed from the current
* read.
*
* Basic idea is the following: Go through each other thread and find
* the last action that happened before our read. Two cases:
*
- * (1) The action is a write => that write must either occur before
+ * -# The action is a write: that write must either occur before
* the write we read from or be the write we read from.
- *
- * (2) The action is a read => the write that that action read from
+ * -# The action is a read: the write that that action read from
* must occur before the write we read from or be the same write.
*
* @param curr The current action. Must be a read.
rel_heads_list_t release_heads;
bool complete;
complete = release_seq_heads(rf, &release_heads, pending);
- for (unsigned int i = 0; i < release_heads.size(); i++) {
- if (!acquire->has_synchronized_with(release_heads[i])) {
- if (acquire->synchronize_with(release_heads[i]))
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ if (!acquire->has_synchronized_with(release_heads[i]))
+ if (synchronize(release_heads[i], acquire))
updated = true;
- else
- set_bad_synchronization();
- }
- }
if (updated) {
/* Re-check all pending release sequences */
for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
if (acquire->happens_before(propagate)) {
- propagate->synchronize_with(acquire);
+ synchronize(acquire, propagate);
/* Re-check 'propagate' for mo_graph edges */
work_queue->push_back(MOEdgeWorkEntry(propagate));
}
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
+ ASSERT(check_action_enabled(curr)); /* May have side effects? */
curr = check_current_action(curr);
-
- /* Infeasible -> don't take any more steps */
- if (is_infeasible())
- return NULL;
- else if (isfeasibleprefix() && have_bug_reports()) {
- set_assert();
- return NULL;
- }
-
- if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
- return NULL;
+ ASSERT(curr);
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
- Thread *next_thrd = NULL;
- if (curr)
- next_thrd = action_select_next_thread(curr);
- if (!next_thrd)
- next_thrd = get_next_thread();
-
- DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
- next_thrd ? id_to_int(next_thrd->get_id()) : -1);
-
- return next_thrd;
+ return action_select_next_thread(curr);
}
/** Wrapper to run the user's main function, with appropriate arguments */
user_main(model->params.argc, model->params.argv);
}
+/** @return True if the execution has taken too many steps */
+bool ModelChecker::too_many_steps() const
+{
+ return params.bound != 0 && priv->used_sequence_numbers > params.bound;
+}
+
+bool ModelChecker::should_terminate_execution()
+{
+ /* Infeasible -> don't take any more steps */
+ if (is_infeasible())
+ return true;
+ else if (isfeasibleprefix() && have_bug_reports()) {
+ set_assert();
+ return true;
+ }
+
+ if (too_many_steps())
+ return true;
+ return false;
+}
+
/** @brief Run ModelChecker for the user program */
void ModelChecker::run()
{
Thread *thr = get_thread(tid);
if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
switch_from_master(thr);
- if (is_circular_wait(thr))
- assert_bug("Deadlock detected");
+ if (thr->is_waiting_on(thr))
+ assert_bug("Deadlock detected (thread %u)", i);
+ }
+ }
+
+ /* Don't schedule threads which should be disabled */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *th = get_thread(int_to_id(i));
+ ModelAction *act = th->get_pending();
+ if (act && is_enabled(th) && !check_action_enabled(act)) {
+ scheduler->sleep(th);
}
}
if (has_asserted())
break;
+ if (!t)
+ t = get_next_thread();
+ if (!t || t->is_model_thread())
+ break;
+
/* Consume the next action for a Thread */
ModelAction *curr = t->get_pending();
t->set_pending(NULL);
t = take_step(curr);
- } while (t && !t->is_model_thread());
+ } while (!should_terminate_execution());
/*
* Launch end-of-execution release sequence fixups only when