#include <stdio.h>
+#include <algorithm>
#include "model.h"
#include "action.h"
#include "clockvector.h"
#include "cyclegraph.h"
#include "promise.h"
+#include "datarace.h"
#define INITIAL_THREAD_ID 0
params(params),
current_action(NULL),
diverge(NULL),
- nextThread(THREAD_ID_T_NONE),
+ nextThread(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>()),
obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
promises(new std::vector<Promise *>()),
+ lazy_sync_with_release(new HashTable<void *, std::list<ModelAction *>, uintptr_t, 4>()),
thrd_last_action(new std::vector<ModelAction *>(1)),
node_stack(new NodeStack()),
next_backtrack(NULL),
mo_graph(new CycleGraph()),
- failed_promise(false)
+ failed_promise(false),
+ asserted(false)
{
}
delete (*promises)[i];
delete promises;
+ delete lazy_sync_with_release;
+
delete thrd_last_action;
delete node_stack;
delete scheduler;
current_action = NULL;
next_thread_id = INITIAL_THREAD_ID;
used_sequence_numbers = 0;
- nextThread = 0;
+ nextThread = NULL;
next_backtrack = NULL;
failed_promise = false;
+ reset_asserted();
snapshotObject->backTrackBeforeStep(0);
}
return ++used_sequence_numbers;
}
-/**
- * Performs the "scheduling" for the model-checker. That is, it checks if the
- * model-checker has selected a "next thread to run" and returns it, if
- * available. This function should be called from the Scheduler routine, where
- * the Scheduler falls back to a default scheduling routine if needed.
- *
- * @return The next thread chosen by the model-checker. If the model-checker
- * makes no selection, retuns NULL.
- */
-Thread * ModelChecker::schedule_next_thread()
-{
- Thread *t;
- if (nextThread == THREAD_ID_T_NONE)
- return NULL;
- t = thread_map->get(id_to_int(nextThread));
-
- ASSERT(t != NULL);
-
- return t;
-}
-
/**
* Choose the next thread in the replay sequence.
*
* from the backtracking set. Otherwise, simply returns the next thread in the
* sequence that is being replayed.
*/
-thread_id_t ModelChecker::get_next_replay_thread()
+Thread * ModelChecker::get_next_replay_thread()
{
thread_id_t tid;
/* Have we completed exploring the preselected path? */
if (diverge == NULL)
- return THREAD_ID_T_NONE;
+ return NULL;
/* Else, we are trying to replay an execution */
ModelAction *next = node_stack->get_next()->get_action();
tid = next->get_tid();
}
DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
- return tid;
+ ASSERT(tid != THREAD_ID_T_NONE);
+ return thread_map->get(id_to_int(tid));
}
/**
if (isfinalfeasible() || DBG_ENABLED())
print_summary();
- if ((diverge = model->get_next_backtrack()) == NULL)
+ if ((diverge = get_next_backtrack()) == NULL)
return false;
if (DBG_ENABLED()) {
diverge->print();
}
- model->reset_to_initial_state();
+ reset_to_initial_state();
return true;
}
return next;
}
-void ModelChecker::check_current_action(void)
+/**
+ * This is the heart of the model checker routine. It performs model-checking
+ * actions corresponding to a given "current action." Among other processes, it
+ * calculates reads-from relationships, updates synchronization clock vectors,
+ * forms a memory_order constraints graph, and handles replay/backtrack
+ * execution when running permutations of previously-observed executions.
+ *
+ * @param curr The current action to process
+ * @return The next Thread that must be executed. May be NULL if ModelChecker
+ * makes no choice (e.g., according to replay execution, combining RMW actions,
+ * etc.)
+ */
+Thread * ModelChecker::check_current_action(ModelAction *curr)
{
- ModelAction *curr = this->current_action;
bool already_added = false;
- this->current_action = NULL;
- if (!curr) {
- DEBUG("trying to push NULL action...\n");
- return;
- }
+
+ ASSERT(curr);
if (curr->is_rmwc() || curr->is_rmw()) {
ModelAction *tmp = process_rmw(curr);
if (curr->get_type() == THREAD_CREATE) {
Thread *th = (Thread *)curr->get_location();
th->set_creation(curr);
+ } else if (curr->get_type() == THREAD_JOIN) {
+ Thread *wait, *join;
+ wait = get_thread(curr->get_tid());
+ join = (Thread *)curr->get_location();
+ if (!join->is_complete())
+ scheduler->wait(wait, join);
+ } else if (curr->get_type() == THREAD_FINISH) {
+ Thread *th = get_thread(curr->get_tid());
+ while (!th->wait_list_empty()) {
+ Thread *wake = th->pop_wait_list();
+ scheduler->wake(wake);
+ }
+ th->complete();
}
/* Deal with new thread */
/* Assign reads_from values */
Thread *th = get_thread(curr->get_tid());
uint64_t value = VALUE_NONE;
+ bool updated = false;
if (curr->is_read()) {
const ModelAction *reads_from = curr->get_node()->get_read_from();
if (reads_from != NULL) {
value = reads_from->get_value();
/* Assign reads_from, perform release/acquire synchronization */
curr->read_from(reads_from);
- r_modification_order(curr,reads_from);
+ if (r_modification_order(curr,reads_from))
+ updated = true;
} else {
/* Read from future value */
value = curr->get_node()->get_future_value();
promises->push_back(valuepromise);
}
} else if (curr->is_write()) {
- w_modification_order(curr);
- resolve_promises(curr);
+ if (w_modification_order(curr))
+ updated = true;
+ if (resolve_promises(curr))
+ updated = true;
}
+ if (updated)
+ resolve_release_sequences(curr->get_location());
+
th->set_return_value(value);
/* Add action to list. */
if (!already_added)
add_action_to_lists(curr);
- /** @todo Is there a better interface for setting the next thread rather
- than this field/convoluted approach? Perhaps like just returning
- it or something? */
-
- /* Do not split atomic actions. */
- if (curr->is_rmwr())
- nextThread = thread_current()->get_id();
- else
- nextThread = get_next_replay_thread();
-
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
next_backtrack = curr;
set_backtracking(curr);
+
+ /* Do not split atomic actions. */
+ if (curr->is_rmwr())
+ return thread_current();
+ /* The THREAD_CREATE action points to the created Thread */
+ else if (curr->get_type() == THREAD_CREATE)
+ return (Thread *)curr->get_location();
+ else
+ return get_next_replay_thread();
+}
+
+/** @returns whether the current partial trace must be a prefix of a
+ * feasible trace. */
+
+bool ModelChecker::isfeasibleprefix() {
+ return promises->size()==0;
}
/** @returns whether the current partial trace is feasible. */
* Updates the mo_graph with the constraints imposed from the current read.
* @param curr The current action. Must be a read.
* @param rf The action that curr reads from. Must be a write.
+ * @return True if modification order edges were added; false otherwise
*/
-void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
+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());
unsigned int i;
+ bool added = false;
ASSERT(curr->is_read());
/* Iterate over all threads */
if (act->happens_before(curr)) {
if (act->is_read()) {
const ModelAction *prevreadfrom = act->get_reads_from();
- if (prevreadfrom != NULL && rf != prevreadfrom)
+ if (prevreadfrom != NULL && rf != prevreadfrom) {
mo_graph->addEdge(prevreadfrom, rf);
+ added = true;
+ }
} else if (rf != act) {
mo_graph->addEdge(act, rf);
+ added = true;
}
break;
}
}
}
+
+ return added;
}
/** Updates the mo_graph with the constraints imposed from the current read. */
/**
* Updates the mo_graph with the constraints imposed from the current write.
* @param curr The current action. Must be a write.
+ * @return True if modification order edges were added; false otherwise
*/
-void ModelChecker::w_modification_order(ModelAction * curr) {
+bool ModelChecker::w_modification_order(ModelAction *curr)
+{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(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->get_location());
- if (last_seq_cst != NULL)
+ if (last_seq_cst != NULL) {
mo_graph->addEdge(last_seq_cst, curr);
+ added = true;
+ }
}
/* Iterate over all threads */
mo_graph->addEdge(act->get_reads_from(), curr);
else
mo_graph->addEdge(act, curr);
+ added = true;
break;
} else if (act->is_read() && !act->is_synchronizing(curr) &&
!act->same_thread(curr)) {
}
}
}
+
+ return added;
}
/**
action_list_t::const_reverse_iterator rit;
/* Find rf in the thread list */
- for (rit = list->rbegin(); rit != list->rend(); rit++)
- if (*rit == rf)
- break;
+ rit = std::find(list->rbegin(), list->rend(), rf);
+ ASSERT(rit != list->rend());
/* Find the last write/release */
for (; rit != list->rend(); rit++)
if (id_to_int(rf->get_tid()) == (int)i)
continue;
list = &(*thrd_lists)[i];
+
+ /* Can we ensure no future writes from this thread may break
+ * the release seq? */
+ bool future_ordered = false;
+
for (rit = list->rbegin(); rit != list->rend(); rit++) {
const ModelAction *act = *rit;
if (!act->is_write())
/* Reach synchronization -> this thread is complete */
if (act->happens_before(release))
break;
- if (rf->happens_before(act))
+ if (rf->happens_before(act)) {
+ future_ordered = true;
continue;
+ }
/* Check modification order */
- if (mo_graph->checkReachable(rf, act))
+ if (mo_graph->checkReachable(rf, act)) {
/* rf --mo--> act */
+ future_ordered = true;
continue;
+ }
if (mo_graph->checkReachable(act, release))
/* act --mo--> release */
break;
}
certain = false;
}
+ if (!future_ordered)
+ return false; /* This thread is uncertain */
}
if (certain)
bool complete;
complete = release_seq_head(rf, release_heads);
if (!complete) {
- /** @todo complete lazy checking */
+ /* add act to 'lazy checking' list */
+ std::list<ModelAction *> *list;
+ list = lazy_sync_with_release->get_safe_ptr(act->get_location());
+ list->push_back(act);
}
}
+/**
+ * Attempt to resolve all stashed operations that might synchronize with a
+ * release sequence for a given location. This implements the "lazy" portion of
+ * determining whether or not a release sequence was contiguous, since not all
+ * modification order information is present at the time an action occurs.
+ *
+ * @param location The location/object that should be checked for release
+ * sequence resolutions
+ * @return True if any updates occurred (new synchronization, new mo_graph edges)
+ */
+bool ModelChecker::resolve_release_sequences(void *location)
+{
+ std::list<ModelAction *> *list;
+ list = lazy_sync_with_release->getptr(location);
+ if (!list)
+ return false;
+
+ bool updated = false;
+ std::list<ModelAction *>::iterator it = list->begin();
+ while (it != list->end()) {
+ ModelAction *act = *it;
+ const ModelAction *rf = act->get_reads_from();
+ std::vector<const ModelAction *> release_heads;
+ bool complete;
+ complete = release_seq_head(rf, &release_heads);
+ for (unsigned int i = 0; i < release_heads.size(); i++) {
+ if (!act->has_synchronized_with(release_heads[i])) {
+ updated = true;
+ act->synchronize_with(release_heads[i]);
+ }
+ }
+
+ if (updated) {
+ /* propagate synchronization to later actions */
+ action_list_t::reverse_iterator it = action_trace->rbegin();
+ while ((*it) != act) {
+ ModelAction *propagate = *it;
+ if (act->happens_before(propagate))
+ /** @todo new mo_graph edges along with
+ * this synchronization? */
+ propagate->synchronize_with(act);
+ }
+ }
+ if (complete)
+ it = list->erase(it);
+ else
+ it++;
+ }
+
+ // If we resolved promises or data races, see if we have realized a data race.
+ if (checkDataRaces()) {
+ set_assert();
+ }
+
+ return updated;
+}
+
/**
* Performs various bookkeeping operations for the current ModelAction. For
* instance, adds action to the per-object, per-thread action vector and to the
} else
promise_index++;
}
+
return resolved;
}
merge_cv->synchronized_since(act)) {
//This thread is no longer able to send values back to satisfy the promise
int num_synchronized_threads = promise->increment_threads();
- if (num_synchronized_threads == model->get_num_threads()) {
+ if (num_synchronized_threads == get_num_threads()) {
//Promise has failed
failed_promise = true;
return;
* context). This switch is made with the intention of exploring a particular
* model-checking action (described by a ModelAction object). Must be called
* from a user-thread context.
- * @param act The current action that will be explored. May be NULL, although
- * there is little reason to switch to the model-checker without an action to
- * explore (note: act == NULL is sometimes used as a hack to allow a thread to
- * yield control without performing any progress; see thrd_join()).
+ * @param act The current action that will be explored. Must not be NULL.
* @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
*/
int ModelChecker::switch_to_master(ModelAction *act)
bool ModelChecker::take_step() {
Thread *curr, *next;
+ if (has_asserted())
+ return false;
+
curr = thread_current();
if (curr) {
if (curr->get_state() == THREAD_READY) {
- check_current_action();
- scheduler->add_thread(curr);
- } else if (curr->get_state() == THREAD_RUNNING) {
- /* Stopped while running; i.e., completed */
- curr->complete();
+ ASSERT(current_action);
+ nextThread = check_current_action(current_action);
+ current_action = NULL;
+ if (!curr->is_blocked() && !curr->is_complete())
+ scheduler->add_thread(curr);
} else {
ASSERT(false);
}
}
- next = scheduler->next_thread();
+ next = scheduler->next_thread(nextThread);
/* Infeasible -> don't take any more steps */
if (!isfeasible())
projects / model-checker.git / blobdiff