#include "promise.h"
#include "datarace.h"
#include "threads-model.h"
+#include "output.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
+ */
+struct model_snapshot_members {
+ model_snapshot_members() :
+ current_action(NULL),
+ /* First thread created will have id INITIAL_THREAD_ID */
+ next_thread_id(INITIAL_THREAD_ID),
+ used_sequence_numbers(0),
+ nextThread(NULL),
+ next_backtrack(NULL),
+ bugs(),
+ stats(),
+ failed_promise(false),
+ too_many_reads(false),
+ bad_synchronization(false),
+ asserted(false)
+ { }
+
+ ~model_snapshot_members() {
+ for (unsigned int i = 0; i < bugs.size(); i++)
+ delete bugs[i];
+ bugs.clear();
+ }
+
+ ModelAction *current_action;
+ unsigned int next_thread_id;
+ modelclock_t used_sequence_numbers;
+ Thread *nextThread;
+ ModelAction *next_backtrack;
+ std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
+ struct execution_stats stats;
+ bool failed_promise;
+ bool too_many_reads;
+ /** @brief Incorrectly-ordered synchronization was made */
+ bool bad_synchronization;
+ bool asserted;
+
+ SNAPSHOTALLOC
+};
+
/** @brief Constructor */
ModelChecker::ModelChecker(struct model_params params) :
/* Initialize default scheduler */
params(params),
scheduler(new Scheduler()),
- num_executions(0),
- num_feasible_executions(0),
diverge(NULL),
earliest_diverge(NULL),
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 *, std::vector<action_list_t>, uintptr_t, 4 >()),
+ 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> >()),
pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
node_stack(new NodeStack()),
- mo_graph(new CycleGraph()),
- failed_promise(false),
- too_many_reads(false),
- asserted(false),
- bad_synchronization(false)
+ priv(new struct model_snapshot_members()),
+ mo_graph(new CycleGraph())
{
- /* Allocate this "size" on the snapshotting heap */
- priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
- /* First thread created will have id INITIAL_THREAD_ID */
- priv->next_thread_id = INITIAL_THREAD_ID;
-
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
thread_map->put(id_to_int(model_thread->get_id()), model_thread);
delete node_stack;
delete scheduler;
delete mo_graph;
+ delete priv;
+}
+
+static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
+ action_list_t * tmp=hash->get(ptr);
+ if (tmp==NULL) {
+ tmp=new action_list_t();
+ hash->put(ptr, tmp);
+ }
+ return tmp;
+}
+
+static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr) {
+ std::vector<action_list_t> * tmp=hash->get(ptr);
+ if (tmp==NULL) {
+ tmp=new std::vector<action_list_t>();
+ hash->put(ptr, tmp);
+ }
+ return tmp;
}
/**
{
DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
- failed_promise = false;
- too_many_reads = false;
- bad_synchronization = false;
- reset_asserted();
+
+ /* Print all model-checker output before rollback */
+ fflush(model_out);
+
snapshotObject->backTrackBeforeStep(0);
}
}
/** @return the number of user threads created during this execution */
-unsigned int ModelChecker::get_num_threads()
+unsigned int ModelChecker::get_num_threads() const
{
return priv->next_thread_id;
}
/** @return The currently executing Thread. */
-Thread * ModelChecker::get_current_thread()
+Thread * ModelChecker::get_current_thread() const
{
return scheduler->get_current_thread();
}
return ++priv->used_sequence_numbers;
}
-Node * ModelChecker::get_curr_node() {
+Node * ModelChecker::get_curr_node() const
+{
return node_stack->get_head();
}
}
}
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelChecker::set_bad_synchronization()
+{
+ priv->bad_synchronization = true;
+}
+
+bool ModelChecker::has_asserted() const
+{
+ return priv->asserted;
+}
+
+void ModelChecker::set_assert()
+{
+ priv->asserted = true;
+}
+
/**
- * Queries the model-checker for more executions to explore and, if one
- * exists, resets the model-checker state to execute a new execution.
+ * Check if we are in a deadlock. Should only be called at the end of an
+ * execution, although it should not give false positives in the middle of an
+ * execution (there should be some ENABLED thread).
*
- * @return If there are more executions to explore, return true. Otherwise,
- * return false.
+ * @return True if program is in a deadlock; false otherwise
*/
-bool ModelChecker::next_execution()
+bool ModelChecker::is_deadlocked() const
{
- DBG();
+ bool blocking_threads = false;
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ thread_id_t tid = int_to_id(i);
+ if (is_enabled(tid))
+ return false;
+ Thread *t = get_thread(tid);
+ if (!t->is_model_thread() && t->get_pending())
+ blocking_threads = true;
+ }
+ return blocking_threads;
+}
- num_executions++;
+/**
+ * Check if this is a complete execution. That is, have all thread completed
+ * execution (rather than exiting because sleep sets have forced a redundant
+ * execution).
+ *
+ * @return True if the execution is complete.
+ */
+bool ModelChecker::is_complete_execution() const
+{
+ for (unsigned int i = 0; i < get_num_threads(); i++)
+ if (is_enabled(int_to_id(i)))
+ return false;
+ return true;
+}
- if (isfinalfeasible()) {
- printf("Earliest divergence point since last feasible execution:\n");
+/**
+ * @brief Assert a bug in the executing program.
+ *
+ * Use this function to assert any sort of bug in the user program. If the
+ * current trace is feasible (actually, a prefix of some feasible execution),
+ * then this execution will be aborted, printing the appropriate message. If
+ * the current trace is not yet feasible, the error message will be stashed and
+ * printed if the execution ever becomes feasible.
+ *
+ * @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)
+{
+ priv->bugs.push_back(new bug_message(msg));
+
+ if (isfeasibleprefix()) {
+ set_assert();
+ return true;
+ }
+ return false;
+}
+
+/**
+ * @brief Assert a bug in the executing program, asserted by a user thread
+ * @see ModelChecker::assert_bug
+ * @param msg Descriptive message for the bug (do not include newline char)
+ */
+void ModelChecker::assert_user_bug(const char *msg)
+{
+ /* If feasible bug, bail out now */
+ if (assert_bug(msg))
+ switch_to_master(NULL);
+}
+
+/** @return True, if any bugs have been reported for this execution */
+bool ModelChecker::have_bug_reports() const
+{
+ return priv->bugs.size() != 0;
+}
+
+/** @brief Print bug report listing for this execution (if any bugs exist) */
+void ModelChecker::print_bugs() const
+{
+ if (have_bug_reports()) {
+ model_print("Bug report: %zu bug%s detected\n",
+ priv->bugs.size(),
+ priv->bugs.size() > 1 ? "s" : "");
+ for (unsigned int i = 0; i < priv->bugs.size(); i++)
+ priv->bugs[i]->print();
+ }
+}
+
+/**
+ * @brief Record end-of-execution stats
+ *
+ * Must be run when exiting an execution. Records various stats.
+ * @see struct execution_stats
+ */
+void ModelChecker::record_stats()
+{
+ stats.num_total++;
+ if (!isfeasibleprefix())
+ stats.num_infeasible++;
+ else if (have_bug_reports())
+ stats.num_buggy_executions++;
+ else if (is_complete_execution())
+ stats.num_complete++;
+ else
+ stats.num_redundant++;
+}
+
+/** @brief Print execution stats */
+void ModelChecker::print_stats() const
+{
+ model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+ model_print("Number of redundant executions: %d\n", stats.num_redundant);
+ model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
+ model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
+ model_print("Total executions: %d\n", stats.num_total);
+ model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
+}
+
+/**
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
+ */
+void ModelChecker::print_execution(bool printbugs) const
+{
+ print_program_output();
+
+ if (DBG_ENABLED() || params.verbose) {
+ model_print("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
earliest_diverge->print();
else
- printf("(Not set)\n");
+ model_print("(Not set)\n");
- earliest_diverge = NULL;
- num_feasible_executions++;
+ model_print("\n");
+ print_stats();
}
- DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
- pending_rel_seqs->size());
+ /* Don't print invalid bugs */
+ if (printbugs)
+ print_bugs();
+
+ model_print("\n");
+ print_summary();
+}
+
+/**
+ * Queries the model-checker for more executions to explore and, if one
+ * exists, resets the model-checker state to execute a new execution.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
+bool ModelChecker::next_execution()
+{
+ DBG();
+ /* Is this execution a feasible execution that's worth bug-checking? */
+ bool complete = isfeasibleprefix() && (is_complete_execution() ||
+ have_bug_reports());
+ /* End-of-execution bug checks */
+ if (complete) {
+ if (is_deadlocked())
+ assert_bug("Deadlock detected");
- if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
checkDataRaces();
- print_summary();
}
+ record_stats();
+
+ /* Output */
+ if (DBG_ENABLED() || params.verbose || have_bug_reports())
+ print_execution(complete);
+ else
+ clear_program_output();
+
+ if (complete)
+ earliest_diverge = NULL;
+
if ((diverge = get_next_backtrack()) == NULL)
return false;
if (DBG_ENABLED()) {
- printf("Next execution will diverge at:\n");
+ model_print("Next execution will diverge at:\n");
diverge->print();
}
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
+ /* Optimization: relaxed operations don't need backtracking */
+ if (act->is_relaxed())
+ return NULL;
/* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
case ATOMIC_LOCK:
case ATOMIC_TRYLOCK: {
/* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
}
case ATOMIC_UNLOCK: {
/* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
}
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 *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
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 *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
}
- if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
+ if (!second_part_of_rmw&&is_infeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
mo_graph->rollbackChanges();
- too_many_reads = false;
+ priv->too_many_reads = false;
continue;
}
}
//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();
- }
+ if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+ assert_bug("Lock access before initialization");
state->islocked = true;
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
//unlock the lock
state->islocked = false;
//wake up the other threads
- action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
+ 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));
//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());
+ 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->get_node()->get_misc()==0) {
- condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
+ get_safe_ptr_action(condvar_waiters_map, 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());
+ action_list_t *waiters = get_safe_ptr_action(condvar_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));
break;
}
case ATOMIC_NOTIFY_ONE: {
- action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location());
+ action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
int wakeupthread=curr->get_node()->get_misc();
action_list_t::iterator it = waiters->begin();
advance(it, wakeupthread);
}
/* See if we have realized a data race */
- if (checkDataRaces())
- set_assert();
+ checkDataRaces();
}
/**
(*curr)->set_seq_number(get_next_seq_num());
- newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
+ newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
if (newcurr) {
/* First restore type and order in case of RMW operation */
if ((*curr)->is_rmwr())
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());
+ newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
}
return true; /* This was a new ModelAction */
}
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);
+ get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
return false;
}
} else if (curr->get_type() == THREAD_JOIN) {
return true;
}
+/**
+ * Stores the ModelAction for the current thread action. Call this
+ * immediately before switching from user- to system-context to pass
+ * data between them.
+ * @param act The ModelAction created by the user-thread action
+ */
+void ModelChecker::set_current_action(ModelAction *act) {
+ priv->current_action = act;
+}
+
/**
* This is the heart of the model checker routine. It performs model-checking
* actions corresponding to a given "current action." Among other processes, it
/* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
- while (!work_queue.empty()) {
+ while (!work_queue.empty() && !has_asserted()) {
WorkQueueEntry work = work_queue.front();
work_queue.pop_front();
}
}
-bool ModelChecker::promises_expired() {
+bool ModelChecker::promises_expired() const
+{
for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
Promise *promise = (*promises)[promise_index];
if (promise->get_expiration()<priv->used_sequence_numbers) {
return false;
}
-/** @return whether the current partial trace must be a prefix of a
- * feasible trace. */
-bool ModelChecker::isfeasibleprefix() {
- return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
+/**
+ * This is the strongest feasibility check available.
+ * @return whether the current trace (partial or complete) must be a prefix of
+ * a feasible trace.
+ */
+bool ModelChecker::isfeasibleprefix() const
+{
+ return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
+}
+
+/**
+ * Returns whether the current completed trace is feasible, except for pending
+ * release sequences.
+ */
+bool ModelChecker::is_feasible_prefix_ignore_relseq() const
+{
+ if (DBG_ENABLED() && promises->size() != 0)
+ DEBUG("Infeasible: unrevolved promises\n");
+
+ return !is_infeasible() && promises->size() == 0;
}
-/** @return whether the current partial trace is feasible. */
-bool ModelChecker::isfeasible() {
+/**
+ * Check if the current partial trace is infeasible. Does not check any
+ * end-of-execution flags, which might rule out the execution. Thus, this is
+ * useful only for ruling an execution as infeasible.
+ * @return whether the current partial trace is infeasible.
+ */
+bool ModelChecker::is_infeasible() const
+{
if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
DEBUG("Infeasible: RMW violation\n");
- return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
+ return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
}
-/** @return whether the current partial trace is feasible other than
- * multiple RMW reading from the same store. */
-bool ModelChecker::isfeasibleotherthanRMW() {
+/**
+ * Check If the current partial trace is infeasible, while ignoring
+ * infeasibility related to 2 RMW's reading from the same store. It does not
+ * check end-of-execution feasibility.
+ * @see ModelChecker::is_infeasible
+ * @return whether the current partial trace is infeasible, ignoring multiple
+ * RMWs reading from the same store.
+ * */
+bool ModelChecker::is_infeasible_ignoreRMW() const
+{
if (DBG_ENABLED()) {
if (mo_graph->checkForCycles())
DEBUG("Infeasible: modification order cycles\n");
- if (failed_promise)
+ if (priv->failed_promise)
DEBUG("Infeasible: failed promise\n");
- if (too_many_reads)
+ if (priv->too_many_reads)
DEBUG("Infeasible: too many reads\n");
- if (bad_synchronization)
+ if (priv->bad_synchronization)
DEBUG("Infeasible: bad synchronization ordering\n");
if (promises_expired())
DEBUG("Infeasible: promises expired\n");
}
- return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
-}
-
-/** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() {
- if (DBG_ENABLED() && promises->size() != 0)
- DEBUG("Infeasible: unrevolved promises\n");
-
- return isfeasible() && promises->size() == 0;
+ return mo_graph->checkForCycles() || priv->failed_promise ||
+ priv->too_many_reads || priv->bad_synchronization ||
+ promises_expired();
}
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
return;
//Must make sure that execution is currently feasible... We could
//accidentally clear by rolling back
- if (!isfeasible())
+ if (is_infeasible())
return;
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
int tid = id_to_int(curr->get_tid());
/* Skip checks */
/* Test to see whether this is a feasible write to read from*/
mo_graph->startChanges();
r_modification_order(curr, write);
- bool feasiblereadfrom = isfeasible();
+ bool feasiblereadfrom = !is_infeasible();
mo_graph->rollbackChanges();
if (!feasiblereadfrom)
}
}
if (feasiblewrite) {
- too_many_reads = true;
+ priv->too_many_reads = true;
return;
}
}
*/
bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
bool added = false;
ASSERT(curr->is_read());
*/
void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
*/
bool ModelChecker::w_modification_order(ModelAction *curr)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
bool added = false;
ASSERT(curr->is_write());
if (curr->is_seqcst()) {
/* We have to at least see the last sequentially consistent write,
so we are initialized. */
- ModelAction *last_seq_cst = get_last_seq_cst(curr);
+ ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
if (last_seq_cst != NULL) {
mo_graph->addEdge(last_seq_cst, curr);
added = true;
*/
if (thin_air_constraint_may_allow(curr, act)) {
- if (isfeasible() ||
- (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
+ if (!is_infeasible() ||
+ (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
struct PendingFutureValue pfv = {curr,act};
futurevalues->push_back(pfv);
}
*/
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());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
unsigned int i;
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
/* else relaxed write; check modification order for contiguous subsequence
* -> rf must be same thread as release */
int tid = id_to_int(rf->get_tid());
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
action_list_t *list = &(*thrd_lists)[tid];
action_list_t::const_reverse_iterator rit;
ModelAction *last = get_last_action(int_to_id(i));
Thread *th = get_thread(int_to_id(i));
if ((last && rf->happens_before(last)) ||
- !scheduler->is_enabled(th) ||
+ !is_enabled(th) ||
th->is_complete())
future_ordered = true;
}
// If we resolved promises or data races, see if we have realized a data race.
- if (checkDataRaces()) {
- set_assert();
- }
+ checkDataRaces();
return updated;
}
int tid = id_to_int(act->get_tid());
action_trace->push_back(act);
- obj_map->get_safe_ptr(act->get_location())->push_back(act);
+ get_safe_ptr_action(obj_map, act->get_location())->push_back(act);
- std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
+ std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
(*vec)[tid].push_back(act);
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
- obj_map->get_safe_ptr(mutex_loc)->push_back(act);
+ get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
- std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
+ std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
(*vec)[tid].push_back(act);
* check
* @return The last seq_cst write
*/
-ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
+ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list = obj_map->get_safe_ptr(location);
+ action_list_t *list = get_safe_ptr_action(obj_map, 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++)
return NULL;
}
+/**
+ * Gets the last memory_order_seq_cst fence (in the total global sequence)
+ * performed in a particular thread, prior to a particular fence.
+ * @param tid The ID of the thread to check
+ * @param before_fence The fence from which to begin the search; if NULL, then
+ * search for the most recent fence in the thread.
+ * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
+ */
+ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
+{
+ /* All fences should have NULL location */
+ action_list_t *list = get_safe_ptr_action(obj_map, NULL);
+ action_list_t::reverse_iterator rit = list->rbegin();
+
+ if (before_fence) {
+ for (; rit != list->rend(); rit++)
+ if (*rit == before_fence)
+ break;
+
+ ASSERT(*rit == before_fence);
+ rit++;
+ }
+
+ for (; rit != list->rend(); rit++)
+ if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
+ return *rit;
+ return NULL;
+}
+
/**
* Gets the last unlock operation performed on a particular mutex (i.e., memory
* location). This function identifies the mutex according to the current
ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list = obj_map->get_safe_ptr(location);
+ action_list_t *list = get_safe_ptr_action(obj_map, location);
/* 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++)
return NULL;
}
-ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
+ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
{
ModelAction *parent = get_last_action(tid);
if (!parent)
* @param tid The thread whose clock vector we want
* @return Desired clock vector
*/
-ClockVector * ModelChecker::get_cv(thread_id_t tid)
+ClockVector * ModelChecker::get_cv(thread_id_t tid) const
{
return get_parent_action(tid)->get_cv();
}
merge_cv->synchronized_since(act)) {
if (promise->increment_threads(tid)) {
//Promise has failed
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
if (promise->check_promise()) {
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
promise->set_write(write);
//The pwrite cannot happen before the promise
if (write->happens_before(act) && (write != act)) {
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
if (mo_graph->checkPromise(write, promise)) {
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
*/
void ModelChecker::build_reads_from_past(ModelAction *curr)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
- ModelAction *last_seq_cst = NULL;
+ ModelAction *last_sc_write = NULL;
/* Track whether this object has been initialized */
bool initialized = false;
if (curr->is_seqcst()) {
- last_seq_cst = get_last_seq_cst(curr);
+ last_sc_write = get_last_seq_cst_write(curr);
/* We have to at least see the last sequentially consistent write,
so we are initialized. */
- if (last_seq_cst != NULL)
+ if (last_sc_write != NULL)
initialized = true;
}
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
- if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
- DEBUG("Adding action to may_read_from:\n");
- if (DBG_ENABLED()) {
- act->print();
- curr->print();
- }
-
- if (curr->get_sleep_flag() && ! curr->is_seqcst()) {
- if (sleep_can_read_from(curr, act))
- curr->get_node()->add_read_from(act);
- } else
+ if (!curr->is_seqcst() || (!act->is_seqcst() && (last_sc_write == NULL || !act->happens_before(last_sc_write))) || act == last_sc_write) {
+ if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
+ DEBUG("Adding action to may_read_from:\n");
+ if (DBG_ENABLED()) {
+ act->print();
+ curr->print();
+ }
curr->get_node()->add_read_from(act);
+ }
}
/* Include at most one act per-thread that "happens before" curr */
}
}
- if (!initialized) {
- /** @todo Need a more informative way of reporting errors. */
- printf("ERROR: may read from uninitialized atomic\n");
- set_assert();
- }
+ if (!initialized)
+ assert_bug("May read from uninitialized atomic");
if (DBG_ENABLED() || !initialized) {
- printf("Reached read action:\n");
+ model_print("Reached read action:\n");
curr->print();
- printf("Printing may_read_from\n");
+ model_print("Printing may_read_from\n");
curr->get_node()->print_may_read_from();
- printf("End printing may_read_from\n");
+ model_print("End printing may_read_from\n");
}
}
}
}
-static void print_list(action_list_t *list)
+static void print_list(action_list_t *list, int exec_num = -1)
{
action_list_t::iterator it;
- printf("---------------------------------------------------------------------\n");
- printf("Trace:\n");
+ model_print("---------------------------------------------------------------------\n");
+ if (exec_num >= 0)
+ model_print("Execution %d:\n", exec_num);
+
unsigned int hash=0;
for (it = list->begin(); it != list->end(); it++) {
(*it)->print();
hash=hash^(hash<<3)^((*it)->hash());
}
- printf("HASH %u\n", hash);
- printf("---------------------------------------------------------------------\n");
+ model_print("HASH %u\n", hash);
+ model_print("---------------------------------------------------------------------\n");
}
#if SUPPORT_MOD_ORDER_DUMP
}
#endif
-void ModelChecker::print_summary()
+/** @brief Prints an execution trace summary. */
+void ModelChecker::print_summary() const
{
- printf("\n");
- printf("Number of executions: %d\n", num_executions);
- printf("Number of feasible executions: %d\n", num_feasible_executions);
- printf("Total nodes created: %d\n", node_stack->get_total_nodes());
-
#if SUPPORT_MOD_ORDER_DUMP
scheduler->print();
char buffername[100];
- sprintf(buffername, "exec%04u", num_executions);
+ sprintf(buffername, "exec%04u", stats.num_total);
mo_graph->dumpGraphToFile(buffername);
- sprintf(buffername, "graph%04u", num_executions);
+ sprintf(buffername, "graph%04u", stats.num_total);
dumpGraph(buffername);
#endif
- if (!isfinalfeasible())
- printf("INFEASIBLE EXECUTION!\n");
- print_list(action_trace);
- printf("\n");
+ if (!isfeasibleprefix())
+ model_print("INFEASIBLE EXECUTION!\n");
+ print_list(action_trace, stats.num_total);
+ model_print("\n");
}
/**
return get_thread(act->get_tid());
}
+/**
+ * @brief Check if a Thread is currently enabled
+ * @param t The Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool ModelChecker::is_enabled(Thread *t) const
+{
+ return scheduler->is_enabled(t);
+}
+
+/**
+ * @brief Check if a Thread is currently enabled
+ * @param tid The ID of the Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool ModelChecker::is_enabled(thread_id_t tid) const
+{
+ return scheduler->is_enabled(tid);
+}
+
/**
* Switch from a user-context to the "master thread" context (a.k.a. system
* context). This switch is made with the intention of exploring a particular
Thread *next = scheduler->next_thread(priv->nextThread);
/* Infeasible -> don't take any more steps */
- if (!isfeasible())
+ if (is_infeasible())
return false;
+ else if (isfeasibleprefix() && have_bug_reports()) {
+ set_assert();
+ return false;
+ }
if (params.bound != 0) {
if (priv->used_sequence_numbers > params.bound) {
* (4) no pending promises
*/
if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
- isfinalfeasible() && !unrealizedraces.empty()) {
- printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+ is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
+ model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
pending_rel_seqs->size());
ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
std::memory_order_seq_cst, NULL, VALUE_NONE,
return (Thread::swap(&system_context, next) == 0);
}
-/** Runs the current execution until threre are no more steps to take. */
-void ModelChecker::finish_execution() {
- DBG();
+/** Wrapper to run the user's main function, with appropriate arguments */
+void user_main_wrapper(void *)
+{
+ user_main(model->params.argc, model->params.argv);
+}
+
+/** @brief Run ModelChecker for the user program */
+void ModelChecker::run()
+{
+ do {
+ thrd_t user_thread;
+
+ /* Start user program */
+ add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
+
+ /* Wait for all threads to complete */
+ while (take_step());
+ } while (next_execution());
- while (take_step());
+ print_stats();
}
projects / c11tester.git / blobdiff