* 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;
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 */
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)),
+ thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
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 *)snapshot_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 pending_rel_seqs;
delete thrd_last_action;
+ delete thrd_last_fence_release;
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);
+ delete priv;
}
static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
{
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);
}
/** @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;
+}
+
/**
* 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
void ModelChecker::record_stats()
{
stats.num_total++;
- if (!isfinalfeasible())
+ if (!isfeasibleprefix())
stats.num_infeasible++;
else if (have_bug_reports())
stats.num_buggy_executions++;
{
DBG();
/* Is this execution a feasible execution that's worth bug-checking? */
- bool complete = isfinalfeasible() && (is_complete_execution() ||
+ bool complete = isfeasibleprefix() && (is_complete_execution() ||
have_bug_reports());
/* End-of-execution bug checks */
ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
{
switch (act->get_type()) {
+ case ATOMIC_FENCE:
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 = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator 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;
}
- curr->read_from(reads_from);
+ read_from(curr, reads_from);
mo_graph->commitChanges();
mo_check_promises(curr->get_tid(), reads_from);
/* Read from future value */
value = curr->get_node()->get_future_value();
modelclock_t expiration = curr->get_node()->get_future_value_expiration();
- curr->read_from(NULL);
+ read_from(curr, NULL);
Promise *valuepromise = new Promise(curr, value, expiration);
promises->push_back(valuepromise);
}
return updated_mod_order || updated_promises;
}
+/**
+ * Process a fence ModelAction
+ * @param curr The ModelAction to process
+ * @return True if synchronization was updated
+ */
+bool ModelChecker::process_fence(ModelAction *curr)
+{
+ /*
+ * fence-relaxed: no-op
+ * fence-release: only log the occurence (not in this function), for
+ * use in later synchronization
+ * fence-acquire (this function): search for hypothetical release
+ * sequences
+ */
+ bool updated = false;
+ if (curr->is_acquire()) {
+ action_list_t *list = action_trace;
+ action_list_t::reverse_iterator rit;
+ /* Find X : is_read(X) && X --sb-> curr */
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+ if (act == curr)
+ continue;
+ if (act->get_tid() != curr->get_tid())
+ continue;
+ /* Stop at the beginning of the thread */
+ if (act->is_thread_start())
+ break;
+ /* Stop once we reach a prior fence-acquire */
+ if (act->is_fence() && act->is_acquire())
+ break;
+ if (!act->is_read())
+ continue;
+ /* read-acquire will find its own release sequences */
+ if (act->is_acquire())
+ continue;
+
+ /* Establish hypothetical release sequences */
+ 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();
+ if (release_heads.size() != 0)
+ updated = true;
+ }
+ }
+ return updated;
+}
+
/**
* @brief Process the current action for thread-related activity
*
(*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())
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ /* Assign most recent release fence */
+ newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
+
/*
* Perform one-time actions when pushing new ModelAction onto
* NodeStack
}
}
+/**
+ * @brief Establish reads-from relation between two actions
+ *
+ * Perform basic operations involved with establishing a concrete rf relation,
+ * including setting the ModelAction data and checking for release sequences.
+ *
+ * @param act The action that is reading (must be a read)
+ * @param rf The action from which we are reading (must be a write)
+ *
+ * @return True if this read established synchronization
+ */
+bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
+{
+ act->set_read_from(rf);
+ if (rf != NULL && act->is_acquire()) {
+ rel_heads_list_t release_heads;
+ 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();
+ num_heads--;
+ }
+ return num_heads > 0;
+ }
+ return false;
+}
+
/**
* @brief Check whether a model action is enabled.
*
if (act->is_write() && process_write(act))
update = true;
+ if (act->is_fence() && process_fence(act))
+ update_all = true;
+
if (act->is_mutex_op() && process_mutex(act))
update_all = true;
return false;
}
-/** @return whether the current partial trace must be a prefix of a
- * feasible trace. */
+/**
+ * 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 promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
+ 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() const
+/**
+ * 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() const
+/**
+ * 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() const
-{
- 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 = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
int tid = id_to_int(curr->get_tid());
/* 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 added = false;
ASSERT(curr->is_read());
+ /* Last SC fence in the current thread */
+ ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
+ /* Last SC fence in thread i */
+ ModelAction *last_sc_fence_thread_local = NULL;
+ if (int_to_id((int)i) != curr->get_tid())
+ last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
+
+ /* Last SC fence in thread i, before last SC fence in current thread */
+ ModelAction *last_sc_fence_thread_before = NULL;
+ if (last_sc_fence_local)
+ last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+
/* 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;
+ if (act->is_write() && act != rf && act != curr) {
+ /* C++, Section 29.3 statement 5 */
+ if (curr->is_seqcst() && last_sc_fence_thread_local &&
+ *act < *last_sc_fence_thread_local) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ /* C++, Section 29.3 statement 4 */
+ else if (act->is_seqcst() && last_sc_fence_local &&
+ *act < *last_sc_fence_local) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ /* C++, Section 29.3 statement 6 */
+ else if (last_sc_fence_thread_before &&
+ *act < *last_sc_fence_thread_before) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ }
+
/*
* Include at most one act per-thread that "happens
* before" curr. Don't consider reflexively.
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;
}
}
+ /* Last SC fence in the current thread */
+ ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
+ /* Last SC fence in thread i, before last SC fence in current thread */
+ ModelAction *last_sc_fence_thread_before = NULL;
+ if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
+ last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
continue;
}
+ /* C++, Section 29.3 statement 7 */
+ if (last_sc_fence_thread_before && act->is_write() &&
+ *act < *last_sc_fence_thread_before) {
+ mo_graph->addEdge(act, curr);
+ added = true;
+ }
+
/*
* Include at most one act per-thread that "happens
* before" curr
*/
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);
}
if (rf->is_release())
release_heads->push_back(rf);
+ else if (rf->get_last_fence_release())
+ release_heads->push_back(rf->get_last_fence_release());
if (!rf->is_rmw())
break; /* End of RMW chain */
if (rf->is_release())
return true; /* complete */
- /* else relaxed write; check modification order for contiguous subsequence
- * -> rf must be same thread as release */
+ /* else relaxed write
+ * - check for fence-release in the same thread (29.8, stmt. 3)
+ * - check modification order for contiguous subsequence
+ * -> rf must be same thread as release */
+
+ const ModelAction *fence_release = rf->get_last_fence_release();
+ /* Synchronize with a fence-release unconditionally; we don't need to
+ * find any more "contiguous subsequence..." for it */
+ if (fence_release)
+ release_heads->push_back(fence_release);
+
int tid = id_to_int(rf->get_tid());
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];
rit = std::find(list->rbegin(), list->rend(), rf);
ASSERT(rit != list->rend());
- /* Find the last write/release */
- for (; rit != list->rend(); rit++)
+ /* Find the last {write,fence}-release */
+ for (; rit != list->rend(); rit++) {
+ if (fence_release && *(*rit) < *fence_release)
+ break;
if ((*rit)->is_release())
break;
+ }
if (rit == list->rend()) {
/* No write-release in this thread */
return true; /* complete */
- }
+ } else if (fence_release && *(*rit) < *fence_release) {
+ /* The fence-release is more recent (and so, "stronger") than
+ * the most recent write-release */
+ return true; /* complete */
+ } /* else, need to establish contiguous release sequence */
ModelAction *release = *rit;
ASSERT(rf->same_thread(release));
}
/**
- * A public interface for getting the release sequence head(s) with which a
+ * An interface for getting the release sequence head(s) with which a
* given ModelAction must synchronize. This function only returns a non-empty
* result when it can locate a release sequence head with certainty. Otherwise,
* it may mark the internal state of the ModelChecker so that it will handle
- * the release sequence at a later time, causing @a act to update its
+ * the release sequence at a later time, causing @a acquire to update its
* synchronization at some later point in execution.
- * @param act The 'acquire' action that may read from a release sequence
+ *
+ * @param acquire The 'acquire' action that may synchronize with a release
+ * sequence
+ * @param read The read action that may read from a release sequence; this may
+ * be the same as acquire, or else an earlier action in the same thread (i.e.,
+ * when 'acquire' is a fence-acquire)
* @param release_heads A pass-by-reference return parameter. Will be filled
* with the head(s) of the release sequence(s), if they exists with certainty.
* @see ModelChecker::release_seq_heads
*/
-void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
+void ModelChecker::get_release_seq_heads(ModelAction *acquire,
+ ModelAction *read, rel_heads_list_t *release_heads)
{
- const ModelAction *rf = act->get_reads_from();
+ const ModelAction *rf = read->get_reads_from();
struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
- sequence->acquire = act;
+ sequence->acquire = acquire;
+ sequence->read = read;
if (!release_seq_heads(rf, release_heads, sequence)) {
/* add act to 'lazy checking' list */
std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
while (it != pending_rel_seqs->end()) {
struct release_seq *pending = *it;
- ModelAction *act = pending->acquire;
+ ModelAction *acquire = pending->acquire;
+ const ModelAction *read = pending->read;
/* Only resolve sequences on the given location, if provided */
- if (location && act->get_location() != location) {
+ if (location && read->get_location() != location) {
it++;
continue;
}
- const ModelAction *rf = act->get_reads_from();
+ const ModelAction *rf = read->get_reads_from();
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 (!act->has_synchronized_with(release_heads[i])) {
- if (act->synchronize_with(release_heads[i]))
+ if (!acquire->has_synchronized_with(release_heads[i])) {
+ if (acquire->synchronize_with(release_heads[i]))
updated = true;
else
set_bad_synchronization();
if (updated) {
/* Re-check all pending release sequences */
work_queue->push_back(CheckRelSeqWorkEntry(NULL));
- /* Re-check act for mo_graph edges */
- work_queue->push_back(MOEdgeWorkEntry(act));
+ /* Re-check read-acquire for mo_graph edges */
+ if (acquire->is_read())
+ work_queue->push_back(MOEdgeWorkEntry(acquire));
/* propagate synchronization to later actions */
action_list_t::reverse_iterator rit = action_trace->rbegin();
- for (; (*rit) != act; rit++) {
+ for (; (*rit) != acquire; rit++) {
ModelAction *propagate = *rit;
- if (act->happens_before(propagate)) {
- propagate->synchronize_with(act);
+ if (acquire->happens_before(propagate)) {
+ propagate->synchronize_with(acquire);
/* Re-check 'propagate' for mo_graph edges */
work_queue->push_back(MOEdgeWorkEntry(propagate));
}
thrd_last_action->resize(get_num_threads());
(*thrd_last_action)[tid] = act;
+ if (act->is_fence() && act->is_release()) {
+ if ((int)thrd_last_fence_release->size() <= tid)
+ thrd_last_fence_release->resize(get_num_threads());
+ (*thrd_last_fence_release)[tid] = act;
+ }
+
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
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;
}
}
return NULL;
}
+/**
+ * @brief Get the last fence release performed by a particular Thread
+ * @param tid The thread ID of the Thread in question
+ * @return The last fence release in the thread, if one exists; NULL otherwise
+ */
+ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
+{
+ int threadid = id_to_int(tid);
+ if (threadid < (int)thrd_last_fence_release->size())
+ return (*thrd_last_fence_release)[id_to_int(tid)];
+ else
+ return NULL;
+}
+
/**
* Gets the last memory_order_seq_cst write (in the total global sequence)
* performed on a particular object (i.e., memory location), not including the
* 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 = get_safe_ptr_action(obj_map, location);
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
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();
}
if (read->is_rmw()) {
mo_graph->addRMWEdge(write, read);
}
- read->read_from(write);
+ read_from(read, write);
//First fix up the modification order for actions that happened
//before the read
r_modification_order(read, write);
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;
}
}
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) {
- 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);
+ bool allow_read = true;
+
+ if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
+ allow_read = false;
+ else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
+ allow_read = false;
+
+ if (allow_read) {
+ 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 */
dumpGraph(buffername);
#endif
- if (!isfinalfeasible())
+ if (!isfeasibleprefix())
model_print("INFEASIBLE EXECUTION!\n");
print_list(action_trace, stats.num_total);
model_print("\n");
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();
* (4) no pending promises
*/
if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
- isfinalfeasible() && !unrealizedraces.empty()) {
+ 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,
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