#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 {
+ 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;
+};
+
/** @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 *> >()),
bad_synchronization(false)
{
/* Allocate this "size" on the snapshotting heap */
- priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
+ priv = (struct model_snapshot_members *)snapshot_calloc(1, sizeof(*priv));
/* First thread created will have id INITIAL_THREAD_ID */
priv->next_thread_id = INITIAL_THREAD_ID;
delete node_stack;
delete scheduler;
delete mo_graph;
+
+ for (unsigned int i = 0; i < priv->bugs.size(); i++)
+ delete priv->bugs[i];
+ priv->bugs.clear();
+ snapshot_free(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;
}
/**
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 thread_map->get(id_to_int(tid));
}
-/**
+/**
* We need to know what the next actions of all threads in the sleep
* set will be. This method computes them and stores the actions at
* the corresponding thread object's pending action.
scheduler->remove_sleep(thr);
}
}
- }
+ }
+}
+
+/**
+ * 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 True if program is in a deadlock; false otherwise
+ */
+bool ModelChecker::is_deadlocked() const
+{
+ 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;
+}
+
+/**
+ * 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;
+}
+
+/**
+ * @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 (!isfinalfeasible())
+ stats.num_infeasible++;
+ else if (have_bug_reports())
+ stats.num_buggy_executions++;
+ else if (is_complete_execution())
+ stats.num_complete++;
+}
+
+/** @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 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());
}
/**
{
DBG();
- num_executions++;
+ if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
+ if (is_deadlocked())
+ assert_bug("Deadlock detected");
- if (isfinalfeasible()) {
- printf("Earliest divergence point since last feasible execution:\n");
- if (earliest_diverge)
- earliest_diverge->print();
- else
- printf("(Not set)\n");
+ checkDataRaces();
- earliest_diverge = NULL;
- num_feasible_executions++;
- }
+ if (DBG_ENABLED() || params.verbose || have_bug_reports()) {
+ print_program_output();
- DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
- pending_rel_seqs->size());
+ if (DBG_ENABLED() || params.verbose) {
+ model_print("Earliest divergence point since last feasible execution:\n");
+ if (earliest_diverge)
+ earliest_diverge->print();
+ else
+ model_print("(Not set)\n");
+ model_print("\n");
+ print_stats();
+ }
- if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
- checkDataRaces();
+ print_bugs();
+ model_print("\n");
+ print_summary();
+ } else
+ clear_program_output();
+
+ earliest_diverge = NULL;
+ } else if (DBG_ENABLED()) {
+ print_program_output();
+ model_print("\n");
+ print_stats();
print_summary();
+ } else {
+ clear_program_output();
}
+ record_stats();
+
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_WRITE:
case ATOMIC_RMW: {
/* 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;
/* Don't backtrack into a point where the thread is disabled or sleeping. */
if (node->enabled_status(tid)!=THREAD_ENABLED)
continue;
-
+
/* Check if this has been explored already */
if (node->has_been_explored(tid))
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();
}
/**
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 whether the current partial trace must be a prefix of a
* feasible trace. */
-bool ModelChecker::isfeasibleprefix() {
+bool ModelChecker::isfeasibleprefix() const
+{
return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
}
/** @return whether the current partial trace is feasible. */
-bool ModelChecker::isfeasible() {
+bool ModelChecker::isfeasible() const
+{
if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
DEBUG("Infeasible: RMW violation\n");
/** @return whether the current partial trace is feasible other than
* multiple RMW reading from the same store. */
-bool ModelChecker::isfeasibleotherthanRMW() {
+bool ModelChecker::isfeasibleotherthanRMW() const
+{
if (DBG_ENABLED()) {
if (mo_graph->checkForCycles())
DEBUG("Infeasible: modification order cycles\n");
}
/** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() {
+bool ModelChecker::isfinalfeasible() const
+{
if (DBG_ENABLED() && promises->size() != 0)
DEBUG("Infeasible: unrevolved promises\n");
//accidentally clear by rolling back
if (!isfeasible())
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 */
ModelAction *act = *rit;
if (!act->is_read())
return;
-
+
if (act->get_reads_from() != rf)
return;
if (act->get_node()->get_read_from_size() <= 1)
*/
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());
* 1) If RMW and it actually read from something, then we
* already have all relevant edges, so just skip to next
* thread.
- *
+ *
* 2) If RMW and it didn't read from anything, we should
* whatever edge we can get to speed up convergence.
*
if (curr->is_rmw()) {
if (curr->get_reads_from()!=NULL)
break;
- else
+ else
continue;
} else
continue;
*/
if (act->is_write())
mo_graph->addEdge(act, curr);
- else if (act->is_read()) {
+ else if (act->is_read()) {
//if previous read accessed a null, just keep going
if (act->get_reads_from() == NULL)
continue;
*/
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++) {
const ModelAction *write_after_read = NULL;
break;
else if (act->is_write())
write_after_read = act;
- else if (act->is_read()&&act->get_reads_from()!=NULL) {
+ else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
write_after_read = act->get_reads_from();
}
}
-
+
if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
return false;
}
-
return true;
}
/* 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);
-
- std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
+ get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
+
+ 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);
ModelAction * ModelChecker::get_last_seq_cst(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++)
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++)
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
delete(promise);
-
+
promises->erase(promises->begin() + promise_index);
threads_to_check.push_back(read->get_tid());
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
- *
+ *
* pread is the read that created the promise
*
* pwrite is either the first write to same location as pread by
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
const ModelAction *act = promise->get_action();
-
+
//Is this promise on the same location?
if ( act->get_location() != location )
continue;
return;
}
}
-
+
//Don't do any lookups twice for the same thread
if (promise->has_sync_thread(tid))
continue;
-
+
if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
failed_promise = true;
*/
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());
/* 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->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");
}
}
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
while(true) {
Node *prevnode=write->get_node()->get_parent();
-
+
bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
if (write->is_release()&&thread_sleep)
return true;
}
}
-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
void ModelChecker::dumpGraph(char *filename) {
char buffer[200];
- sprintf(buffer, "%s.dot",filename);
- FILE *file=fopen(buffer, "w");
- fprintf(file, "digraph %s {\n",filename);
+ sprintf(buffer, "%s.dot",filename);
+ FILE *file=fopen(buffer, "w");
+ fprintf(file, "digraph %s {\n",filename);
mo_graph->dumpNodes(file);
ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
-
+
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
ModelAction *action=*it;
if (action->is_read()) {
if (thread_array[action->get_tid()] != NULL) {
fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
}
-
+
thread_array[action->get_tid()]=action;
}
- fprintf(file,"}\n");
+ fprintf(file,"}\n");
model_free(thread_array);
- fclose(file);
+ fclose(file);
}
#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);
- dumpGraph(buffername);
+ sprintf(buffername, "graph%04u", stats.num_total);
+ dumpGraph(buffername);
#endif
if (!isfinalfeasible())
- printf("INFEASIBLE EXECUTION!\n");
- print_list(action_trace);
- printf("\n");
+ model_print("INFEASIBLE EXECUTION!\n");
+ print_list(action_trace, stats.num_total);
+ model_print("\n");
}
/**
}
/**
- * Removes a thread from the scheduler.
+ * Removes a thread from the scheduler.
* @param the thread to remove.
*/
void ModelChecker::remove_thread(Thread *t)
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
/* Infeasible -> don't take any more steps */
if (!isfeasible())
return false;
+ else if (isfeasibleprefix() && have_bug_reports()) {
+ set_assert();
+ return false;
+ }
if (params.bound != 0) {
if (priv->used_sequence_numbers > params.bound) {
*/
if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
isfinalfeasible() && !unrealizedraces.empty()) {
- printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+ 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,
projects / c11tester.git / blobdiff