return node_stack->get_head();
}
+/**
+ * @brief Select the next thread to execute based on the curren action
+ *
+ * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
+ * actions should be followed by the execution of their child thread. In either
+ * case, the current action should determine the next thread schedule.
+ *
+ * @param curr The current action
+ * @return The next thread to run, if the current action will determine this
+ * selection; otherwise NULL
+ */
+Thread * ModelChecker::action_select_next_thread(const ModelAction *curr) const
+{
+ /* Do not split atomic RMW */
+ if (curr->is_rmwr())
+ return get_thread(curr);
+ /* Follow CREATE with the created thread */
+ if (curr->get_type() == THREAD_CREATE)
+ return curr->get_thread_operand();
+ return NULL;
+}
+
/**
* @brief Choose the next thread to execute.
*
- * This function chooses the next thread that should execute. It can force the
- * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
- * followed by a THREAD_START, or it can enforce execution replay/backtracking.
- * The model-checker may have no preference regarding the next thread (i.e.,
- * when exploring a new execution ordering), in which case we defer to the
- * scheduler.
+ * This function chooses the next thread that should execute. It can enforce
+ * execution replay/backtracking or, if the model-checker has no preference
+ * regarding the next thread (i.e., when exploring a new execution ordering),
+ * we defer to the scheduler.
*
- * @param curr Optional: The current ModelAction. Only used if non-NULL and it
- * might guide the choice of next thread (i.e., THREAD_CREATE should be
- * followed by THREAD_START, or ATOMIC_RMWR followed by ATOMIC_{RMW,RMWC})
- * @return The next chosen thread to run, if any exist. Or else if no threads
- * remain to be executed, return NULL.
+ * @return The next chosen thread to run, if any exist. Or else if the current
+ * execution should terminate, return NULL.
*/
-Thread * ModelChecker::get_next_thread(ModelAction *curr)
+Thread * ModelChecker::get_next_thread()
{
thread_id_t tid;
- if (curr != NULL) {
- /* Do not split atomic actions. */
- if (curr->is_rmwr())
- return get_thread(curr);
- else if (curr->get_type() == THREAD_CREATE)
- return curr->get_thread_operand();
- }
-
/*
* Have we completed exploring the preselected path? Then let the
* scheduler decide
return blocking_threads;
}
+/**
+ * Check if a Thread has entered a circular wait deadlock situation. This will
+ * not check other threads for potential deadlock situations, and may miss
+ * deadlocks involving WAIT.
+ *
+ * @param t The thread which may have entered a deadlock
+ * @return True if this Thread entered a deadlock; false otherwise
+ */
+bool ModelChecker::is_circular_wait(const Thread *t) const
+{
+ for (Thread *waiting = t->waiting_on() ; waiting != NULL; waiting = waiting->waiting_on())
+ if (waiting == t)
+ return true;
+ return false;
+}
+
/**
* Check if this is a complete execution. That is, have all thread completed
* execution (rather than exiting because sleep sets have forced a redundant
stats.num_buggy_executions++;
else if (is_complete_execution())
stats.num_complete++;
- else if (scheduler->all_threads_sleeping())
+ else {
stats.num_redundant++;
- else
- ASSERT(false);
+
+ /**
+ * @todo We can violate this ASSERT() when fairness/sleep sets
+ * conflict to cause an execution to terminate, e.g. with:
+ * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
+ */
+ //ASSERT(scheduler->all_threads_sleeping());
+ }
}
/** @brief Print execution stats */
{
print_program_output();
- if (DBG_ENABLED() || params.verbose) {
+ if (params.verbose) {
model_print("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
earliest_diverge->print();
record_stats();
/* Output */
- if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
+ if (params.verbose || (complete && have_bug_reports()))
print_execution(complete);
else
clear_program_output();
if (unfair)
continue;
}
+
+ /* See if CHESS-like yield fairness allows */
+ if (model->params.yieldon) {
+ bool unfair = false;
+ for (int t = 0; t < node->get_num_threads(); t++) {
+ thread_id_t tother = int_to_id(t);
+ if (node->is_enabled(tother) && node->has_priority_over(tid, tother)) {
+ unfair = true;
+ break;
+ }
+ }
+ if (unfair)
+ continue;
+ }
+
/* Cache the latest backtracking point */
set_latest_backtrack(prev);
bool ModelChecker::process_read(ModelAction *curr)
{
Node *node = curr->get_node();
- uint64_t value = VALUE_NONE;
- bool updated = false;
while (true) {
+ bool updated = false;
switch (node->get_read_from_status()) {
case READ_FROM_PAST: {
const ModelAction *rf = node->get_read_from_past();
ASSERT(rf);
mo_graph->startChanges();
- value = rf->get_value();
- check_recency(curr, rf);
- bool r_status = r_modification_order(curr, rf);
- if (is_infeasible() && node->increment_read_from()) {
- mo_graph->rollbackChanges();
- priv->too_many_reads = false;
- continue;
+ ASSERT(!is_infeasible());
+ if (!check_recency(curr, rf)) {
+ if (node->increment_read_from()) {
+ mo_graph->rollbackChanges();
+ continue;
+ } else {
+ priv->too_many_reads = true;
+ }
}
+ updated = r_modification_order(curr, rf);
read_from(curr, rf);
mo_graph->commitChanges();
mo_check_promises(curr, true);
-
- updated |= r_status;
break;
}
case READ_FROM_PROMISE: {
Promise *promise = curr->get_node()->get_read_from_promise();
- promise->add_reader(curr);
- value = promise->get_value();
+ if (promise->add_reader(curr))
+ priv->failed_promise = true;
curr->set_read_from_promise(promise);
mo_graph->startChanges();
+ if (!check_recency(curr, promise))
+ priv->too_many_reads = true;
updated = r_modification_order(curr, promise);
mo_graph->commitChanges();
break;
/* Read from future value */
struct future_value fv = node->get_future_value();
Promise *promise = new Promise(curr, fv);
- value = fv.value;
curr->set_read_from_promise(promise);
promises->push_back(promise);
mo_graph->startChanges();
default:
ASSERT(false);
}
- get_thread(curr)->set_return_value(value);
+ get_thread(curr)->set_return_value(curr->get_return_value());
return updated;
}
}
*/
bool ModelChecker::process_mutex(ModelAction *curr)
{
- std::mutex *mutex = NULL;
+ std::mutex *mutex = curr->get_mutex();
struct std::mutex_state *state = NULL;
- if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
- mutex = (std::mutex *)curr->get_location();
+ if (mutex)
state = mutex->get_state();
- } else if (curr->is_wait()) {
- mutex = (std::mutex *)curr->get_value();
- state = mutex->get_state();
- }
switch (curr->get_type()) {
case ATOMIC_TRYLOCK: {
- bool success = !state->islocked;
+ bool success = !state->locked;
curr->set_try_lock(success);
if (!success) {
get_thread(curr)->set_return_value(0);
case ATOMIC_LOCK: {
if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
assert_bug("Lock access before initialization");
- state->islocked = true;
+ state->locked = get_thread(curr);
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
if (unlock != NULL) {
}
case ATOMIC_UNLOCK: {
//unlock the lock
- state->islocked = false;
+ state->locked = NULL;
//wake up the other threads
action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
//activate all the waiting threads
}
case ATOMIC_WAIT: {
//unlock the lock
- state->islocked = false;
+ state->locked = NULL;
//wake up the other threads
action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
//activate all the waiting threads
write_thread = write_thread->get_parent();
struct future_value fv = {
- writer->get_value(),
+ writer->get_write_value(),
writer->get_seq_number() + params.maxfuturedelay,
write_thread->get_id(),
};
*/
bool ModelChecker::process_write(ModelAction *curr)
{
- bool updated_mod_order = w_modification_order(curr);
- bool updated_promises = resolve_promises(curr);
+ /* Readers to which we may send our future value */
+ std::vector< ModelAction *, ModelAlloc<ModelAction *> > send_fv;
+
+ bool updated_mod_order = w_modification_order(curr, &send_fv);
+ int promise_idx = get_promise_to_resolve(curr);
+ const ModelAction *earliest_promise_reader;
+ bool updated_promises = false;
+
+ if (promise_idx >= 0) {
+ earliest_promise_reader = (*promises)[promise_idx]->get_reader(0);
+ updated_promises = resolve_promise(curr, promise_idx);
+ } else
+ earliest_promise_reader = NULL;
+
+ /* Don't send future values to reads after the Promise we resolve */
+ for (unsigned int i = 0; i < send_fv.size(); i++) {
+ ModelAction *read = send_fv[i];
+ if (!earliest_promise_reader || *read < *earliest_promise_reader)
+ futurevalues->push_back(PendingFutureValue(curr, read));
+ }
if (promises->size() == 0) {
for (unsigned int i = 0; i < futurevalues->size(); i++) {
bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
{
ASSERT(rf);
+ ASSERT(rf->is_write());
+
act->set_read_from(rf);
if (act->is_acquire()) {
rel_heads_list_t release_heads;
if (curr->is_lock()) {
std::mutex *lock = (std::mutex *)curr->get_location();
struct std::mutex_state *state = lock->get_state();
- if (state->islocked) {
+ if (state->locked) {
//Stick the action in the appropriate waiting queue
get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
return false;
wake_up_sleeping_actions(curr);
+ /* Compute fairness information for CHESS yield algorithm */
+ if (model->params.yieldon) {
+ curr->get_node()->update_yield(scheduler);
+ }
+
/* Add the action to lists before any other model-checking tasks */
if (!second_part_of_rmw)
add_action_to_lists(curr);
}
}
if (act->is_write()) {
- if (w_modification_order(act))
+ if (w_modification_order(act, NULL))
updated = true;
}
mo_graph->commitChanges();
}
/**
- * Checks whether a thread has read from the same write for too many times
- * without seeing the effects of a later write.
- *
- * Basic idea:
- * 1) there must a different write that we could read from that would satisfy the modification order,
- * 2) we must have read from the same value in excess of maxreads times, and
- * 3) that other write must have been in the reads_from set for maxreads times.
+ * A helper function for ModelChecker::check_recency, to check if the current
+ * thread is able to read from a different write/promise for 'params.maxreads'
+ * number of steps and if that write/promise should become visible (i.e., is
+ * ordered later in the modification order). This helps model memory liveness.
*
- * If so, we decide that the execution is no longer feasible.
+ * @param curr The current action. Must be a read.
+ * @param rf The write/promise from which we plan to read
+ * @param other_rf The write/promise from which we may read
+ * @return True if we were able to read from other_rf for params.maxreads steps
*/
-void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
+template <typename T, typename U>
+bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const
{
- if (params.maxreads != 0) {
- if (curr->get_node()->get_read_from_past_size() <= 1)
- return;
- //Must make sure that execution is currently feasible... We could
- //accidentally clear by rolling back
- 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());
-
- /* Skip checks */
- if ((int)thrd_lists->size() <= tid)
- return;
- action_list_t *list = &(*thrd_lists)[tid];
-
- action_list_t::reverse_iterator rit = list->rbegin();
- /* Skip past curr */
- for (; (*rit) != curr; rit++)
- ;
- /* go past curr now */
- rit++;
-
- action_list_t::reverse_iterator ritcopy = rit;
- //See if we have enough reads from the same value
- int count = 0;
- for (; count < params.maxreads; rit++, count++) {
- if (rit == list->rend())
- return;
- ModelAction *act = *rit;
- if (!act->is_read())
- return;
-
- if (act->get_reads_from() != rf)
- return;
- if (act->get_node()->get_read_from_past_size() <= 1)
- return;
- }
- for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
- /* Get write */
- const ModelAction *write = curr->get_node()->get_read_from_past(i);
+ /* Need a different write/promise */
+ if (other_rf->equals(rf))
+ return false;
- /* Need a different write */
- if (write == rf)
- continue;
+ /* Only look for "newer" writes/promises */
+ if (!mo_graph->checkReachable(rf, other_rf))
+ return false;
- /* Test to see whether this is a feasible write to read from */
- /** NOTE: all members of read-from set should be
- * feasible, so we no longer check it here **/
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())];
+ action_list_t::reverse_iterator rit = list->rbegin();
+ ASSERT((*rit) == curr);
+ /* Skip past curr */
+ rit++;
+
+ /* Does this write/promise work for everyone? */
+ for (int i = 0; i < params.maxreads; i++, rit++) {
+ ModelAction *act = *rit;
+ if (!act->may_read_from(other_rf))
+ return false;
+ }
+ return true;
+}
- rit = ritcopy;
+/**
+ * Checks whether a thread has read from the same write or Promise for too many
+ * times without seeing the effects of a later write/Promise.
+ *
+ * Basic idea:
+ * 1) there must a different write/promise that we could read from,
+ * 2) we must have read from the same write/promise in excess of maxreads times,
+ * 3) that other write/promise must have been in the reads_from set for maxreads times, and
+ * 4) that other write/promise must be mod-ordered after the write/promise we are reading.
+ *
+ * If so, we decide that the execution is no longer feasible.
+ *
+ * @param curr The current action. Must be a read.
+ * @param rf The ModelAction/Promise from which we might read.
+ * @return True if the read should succeed; false otherwise
+ */
+template <typename T>
+bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
+{
+ if (!params.maxreads)
+ return true;
- bool feasiblewrite = true;
- //new we need to see if this write works for everyone
+ //NOTE: Next check is just optimization, not really necessary....
+ if (curr->get_node()->get_read_from_past_size() +
+ curr->get_node()->get_read_from_promise_size() <= 1)
+ return true;
- for (int loop = count; loop > 0; loop--, rit++) {
- ModelAction *act = *rit;
- bool foundvalue = false;
- for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
- if (act->get_node()->get_read_from_past(j) == write) {
- foundvalue = true;
- break;
- }
- }
- if (!foundvalue) {
- feasiblewrite = false;
- break;
- }
- }
- if (feasiblewrite) {
- priv->too_many_reads = true;
- 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());
+ ASSERT(tid < (int)thrd_lists->size());
+ action_list_t *list = &(*thrd_lists)[tid];
+ action_list_t::reverse_iterator rit = list->rbegin();
+ ASSERT((*rit) == curr);
+ /* Skip past curr */
+ rit++;
+
+ action_list_t::reverse_iterator ritcopy = rit;
+ /* See if we have enough reads from the same value */
+ for (int count = 0; count < params.maxreads; ritcopy++, count++) {
+ if (ritcopy == list->rend())
+ return true;
+ ModelAction *act = *ritcopy;
+ if (!act->is_read())
+ return true;
+ if (act->get_reads_from_promise() && !act->get_reads_from_promise()->equals(rf))
+ return true;
+ if (act->get_reads_from() && !act->get_reads_from()->equals(rf))
+ return true;
+ if (act->get_node()->get_read_from_past_size() +
+ act->get_node()->get_read_from_promise_size() <= 1)
+ return true;
+ }
+ for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
+ const ModelAction *write = curr->get_node()->get_read_from_past(i);
+ if (should_read_instead(curr, rf, write))
+ return false; /* liveness failure */
}
+ for (int i = 0; i < curr->get_node()->get_read_from_promise_size(); i++) {
+ const Promise *promise = curr->get_node()->get_read_from_promise(i);
+ if (should_read_instead(curr, rf, promise))
+ return false; /* liveness failure */
+ }
+ return true;
}
/**
* (II) Sending the write back to non-synchronizing reads.
*
* @param curr The current action. Must be a write.
+ * @param send_fv A vector for stashing reads to which we may pass our future
+ * value. If NULL, then don't record any future values.
* @return True if modification order edges were added; false otherwise
*/
-bool ModelChecker::w_modification_order(ModelAction *curr)
+bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv)
{
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
pendingfuturevalue.
*/
- if (thin_air_constraint_may_allow(curr, act)) {
+ if (send_fv && thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible())
- futurevalues->push_back(PendingFutureValue(curr, act));
+ send_fv->push_back(act);
else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
add_future_value(curr, act);
}
int uninit_id = -1;
action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
if (list->empty() && act->is_atomic_var()) {
- uninit = new_uninitialized_action(act->get_location());
+ uninit = get_uninitialized_action(act);
uninit_id = id_to_int(uninit->get_tid());
- list->push_back(uninit);
+ list->push_front(uninit);
}
list->push_back(act);
}
/**
- * Resolve a set of Promises with a current write. The set is provided in the
- * Node corresponding to @a write.
+ * @brief Find the promise, if any to resolve for the current action
+ * @param curr The current ModelAction. Should be a write.
+ * @return The (non-negative) index for the Promise to resolve, if any;
+ * otherwise -1
+ */
+int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
+{
+ for (unsigned int i = 0; i < promises->size(); i++)
+ if (curr->get_node()->get_promise(i))
+ return i;
+ return -1;
+}
+
+/**
+ * Resolve a Promise with a current write.
* @param write The ModelAction that is fulfilling Promises
- * @return True if promises were resolved; false otherwise
+ * @param promise_idx The index corresponding to the promise
+ * @return True if the Promise was successfully resolved; false otherwise
*/
-bool ModelChecker::resolve_promises(ModelAction *write)
+bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
{
- bool haveResolved = false;
std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
- promise_list_t mustResolve, resolved;
-
- for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
- Promise *promise = (*promises)[promise_index];
- if (write->get_node()->get_promise(i)) {
- for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
- ModelAction *read = promise->get_reader(j);
- read_from(read, write);
- actions_to_check.push_back(read);
- }
- //Make sure the promise's value matches the write's value
- ASSERT(promise->is_compatible(write));
- mo_graph->resolvePromise(promise, write, &mustResolve);
+ Promise *promise = (*promises)[promise_idx];
- resolved.push_back(promise);
- promises->erase(promises->begin() + promise_index);
-
- haveResolved = true;
- } else
- promise_index++;
+ for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
+ ModelAction *read = promise->get_reader(i);
+ read_from(read, write);
+ actions_to_check.push_back(read);
}
+ /* Make sure the promise's value matches the write's value */
+ ASSERT(promise->is_compatible(write) && promise->same_value(write));
+ if (!mo_graph->resolvePromise(promise, write))
+ priv->failed_promise = true;
+
+ promises->erase(promises->begin() + promise_idx);
+ /**
+ * @todo It is possible to end up in an inconsistent state, where a
+ * "resolved" promise may still be referenced if
+ * CycleGraph::resolvePromise() failed, so don't delete 'promise'.
+ *
+ * Note that the inconsistency only matters when dumping mo_graph to
+ * file.
+ *
+ * delete promise;
+ */
- for (unsigned int i = 0; i < mustResolve.size(); i++) {
- if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
- == resolved.end())
- priv->failed_promise = true;
- }
- for (unsigned int i = 0; i < resolved.size(); i++)
- delete resolved[i];
//Check whether reading these writes has made threads unable to
//resolve promises
-
for (unsigned int i = 0; i < actions_to_check.size(); i++) {
ModelAction *read = actions_to_check[i];
mo_check_promises(read, true);
}
- return haveResolved;
+ return true;
}
/**
{
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
- if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value())
+ if (!promise->is_compatible(curr) || !promise->same_value(curr))
continue;
bool satisfy = true;
Promise *promise = (*promises)[i];
// Is this promise on the same location?
- if (promise->get_value() != write->get_value())
+ if (!promise->same_location(write))
continue;
for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
}
/**
- * @brief Create a new action representing an uninitialized atomic
- * @param location The memory location of the atomic object
- * @return A pointer to a new ModelAction
+ * @brief Get an action representing an uninitialized atomic
+ *
+ * This function may create a new one or try to retrieve one from the NodeStack
+ *
+ * @param curr The current action, which prompts the creation of an UNINIT action
+ * @return A pointer to the UNINIT ModelAction
*/
-ModelAction * ModelChecker::new_uninitialized_action(void *location) const
+ModelAction * ModelChecker::get_uninitialized_action(const ModelAction *curr) const
{
- ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
- act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
+ Node *node = curr->get_node();
+ ModelAction *act = node->get_uninit_action();
+ if (!act) {
+ act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), model->params.uninitvalue, model_thread);
+ node->set_uninit_action(act);
+ }
act->create_cv(NULL);
return act;
}
unsigned int hash = 0;
for (it = list->begin(); it != list->end(); it++) {
- (*it)->print();
+ const ModelAction *act = *it;
+ if (act->get_seq_number() > 0)
+ act->print();
hash = hash^(hash<<3)^((*it)->hash());
}
model_print("HASH %u\n", hash);
print_infeasibility(" INFEASIBLE");
print_list(action_trace);
model_print("\n");
+ if (!promises->empty()) {
+ model_print("Pending promises:\n");
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ model_print(" [P%u] ", i);
+ (*promises)[i]->print();
+ }
+ model_print("\n");
+ }
}
/**
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
- Thread *next_thrd = get_next_thread(curr);
+ Thread *next_thrd = NULL;
+ if (curr)
+ next_thrd = action_select_next_thread(curr);
+ if (!next_thrd)
+ next_thrd = get_next_thread();
DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
next_thrd ? id_to_int(next_thrd->get_id()) : -1);
Thread *thr = get_thread(tid);
if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
switch_from_master(thr);
+ if (is_circular_wait(thr))
+ assert_bug("Deadlock detected");
}
}
projects / model-checker.git / blobdiff