unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
- std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
+ SnapVector<bug_message *> bugs;
struct execution_stats stats;
bool failed_promise;
bool too_many_reads;
obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
- obj_thrd_map(new HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 >()),
- promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
- futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
- pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
- thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
- thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
+ obj_thrd_map(new HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4 >()),
+ promises(new SnapVector<Promise *>()),
+ futurevalues(new SnapVector<struct PendingFutureValue>()),
+ pending_rel_seqs(new SnapVector<struct release_seq *>()),
+ thrd_last_action(new SnapVector<ModelAction *>(1)),
+ thrd_last_fence_release(new SnapVector<ModelAction *>()),
node_stack(new NodeStack()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
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)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
{
- std::vector<action_list_t> *tmp = hash->get(ptr);
+ SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
- tmp = new std::vector<action_list_t>();
+ tmp = new SnapVector<action_list_t>();
hash->put(ptr, tmp);
}
return tmp;
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
{
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();
* load-acquire
* or
* load --sb-> fence-acquire */
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
+ ModelVector<ModelAction *> acquire_fences(get_num_threads(), NULL);
+ ModelVector<ModelAction *> prior_loads(get_num_threads(), NULL);
bool found_acquire_fences = false;
for ( ; rit != list->rend(); rit++) {
ModelAction *prev = *rit;
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;
while (true) {
bool updated = false;
switch (node->get_read_from_status()) {
}
updated = r_modification_order(curr, rf);
- value = rf->get_write_value();
read_from(curr, rf);
mo_graph->commitChanges();
mo_check_promises(curr, true);
Promise *promise = curr->get_node()->get_read_from_promise();
if (promise->add_reader(curr))
priv->failed_promise = true;
- value = promise->get_value();
curr->set_read_from_promise(promise);
mo_graph->startChanges();
if (!check_recency(curr, promise))
/* 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();
- state = mutex->get_state();
- } else if (curr->is_wait()) {
- mutex = (std::mutex *)curr->get_value();
+ if (mutex)
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
return false;
}
+/**
+ * @brief Check if the current pending promises allow a future value to be sent
+ *
+ * If one of the following is true:
+ * (a) there are no pending promises
+ * (b) the reader and writer do not cross any promises
+ * Then, it is safe to pass a future value back now.
+ *
+ * Otherwise, we must save the pending future value until (a) or (b) is true
+ *
+ * @param writer The operation which sends the future value. Must be a write.
+ * @param reader The operation which will observe the value. Must be a read.
+ * @return True if the future value can be sent now; false if it must wait.
+ */
+bool ModelChecker::promises_may_allow(const ModelAction *writer,
+ const ModelAction *reader) const
+{
+ if (promises->empty())
+ return true;
+ for(int i=promises->size()-1;i>=0;i--) {
+ ModelAction *pr=(*promises)[i]->get_reader(0);
+ //reader is after promise...doesn't cross any promise
+ if (*reader > *pr)
+ return true;
+ //writer is after promise, reader before...bad...
+ if (*writer > *pr)
+ return false;
+ }
+ return true;
+}
+
+/**
+ * @brief Add a future value to a reader
+ *
+ * This function performs a few additional checks to ensure that the future
+ * value can be feasibly observed by the reader
+ *
+ * @param writer The operation whose value is sent. Must be a write.
+ * @param reader The read operation which may read the future value. Must be a read.
+ */
void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
{
/* Do more ambitious checks now that mo is more complete */
- if (mo_may_allow(writer, reader)) {
- Node *node = reader->get_node();
-
- /* Find an ancestor thread which exists at the time of the reader */
- Thread *write_thread = get_thread(writer);
- while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
- write_thread = write_thread->get_parent();
-
- struct future_value fv = {
- writer->get_write_value(),
- writer->get_seq_number() + params.maxfuturedelay,
- write_thread->get_id(),
- };
- if (node->add_future_value(fv))
- set_latest_backtrack(reader);
- }
+ if (!mo_may_allow(writer, reader))
+ return;
+
+ Node *node = reader->get_node();
+
+ /* Find an ancestor thread which exists at the time of the reader */
+ Thread *write_thread = get_thread(writer);
+ while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
+ write_thread = write_thread->get_parent();
+
+ struct future_value fv = {
+ writer->get_write_value(),
+ writer->get_seq_number() + params.maxfuturedelay,
+ write_thread->get_id(),
+ };
+ if (node->add_future_value(fv))
+ set_latest_backtrack(reader);
}
/**
bool ModelChecker::process_write(ModelAction *curr)
{
/* Readers to which we may send our future value */
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > send_fv;
+ ModelVector<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);
+ bool updated_mod_order = w_modification_order(curr, &send_fv);
+ Promise *promise = pop_promise_to_resolve(curr);
+
+ if (promise) {
+ earliest_promise_reader = promise->get_reader(0);
+ updated_promises = resolve_promise(curr, promise);
} 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));
+
+ /* Don't send future values to reads after the Promise we resolve */
+ if (!earliest_promise_reader || *read < *earliest_promise_reader) {
+ /* Check if future value can be sent immediately */
+ if (promises_may_allow(curr, read)) {
+ add_future_value(curr, read);
+ } else {
+ futurevalues->push_back(PendingFutureValue(curr, read));
+ }
+ }
}
- if (promises->size() == 0) {
- for (unsigned int i = 0; i < futurevalues->size(); i++) {
- struct PendingFutureValue pfv = (*futurevalues)[i];
- add_future_value(pfv.writer, pfv.act);
+ /* Check the pending future values */
+ for (int i = (int)futurevalues->size() - 1; i >= 0; i--) {
+ struct PendingFutureValue pfv = (*futurevalues)[i];
+ if (promises_may_allow(pfv.writer, pfv.reader)) {
+ add_future_value(pfv.writer, pfv.reader);
+ futurevalues->erase(futurevalues->begin() + i);
}
- futurevalues->clear();
}
mo_graph->commitChanges();
* use in later synchronization
* fence-acquire (this function): search for hypothetical release
* sequences
+ * fence-seq-cst: MO constraints formed in {r,w}_modification_order
*/
bool updated = false;
if (curr->is_acquire()) {
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 (!mo_graph->checkReachable(rf, other_rf))
return false;
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ SnapVector<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);
curr->get_node()->get_read_from_promise_size() <= 1)
return true;
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ SnapVector<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];
template <typename rf_type>
bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
{
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ SnapVector<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());
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+ ModelAction *last_sc_write = NULL;
+ if (curr->is_seqcst())
+ last_sc_write = get_last_seq_cst_write(curr);
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (act->is_write() && !act->equals(rf) && act != curr) {
+ /* Skip curr */
+ if (act == curr)
+ continue;
+ /* Don't want to add reflexive edges on 'rf' */
+ if (act->equals(rf)) {
+ if (act->happens_before(curr))
+ break;
+ else
+ continue;
+ }
+
+ if (act->is_write()) {
/* C++, Section 29.3 statement 5 */
if (curr->is_seqcst() && last_sc_fence_thread_local &&
*act < *last_sc_fence_thread_local) {
}
}
+ /* C++, Section 29.3 statement 3 (second subpoint) */
+ if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
+ added = mo_graph->addEdge(act, rf) || added;
+ break;
+ }
+
/*
* Include at most one act per-thread that "happens
- * before" curr. Don't consider reflexively.
+ * before" curr
*/
- if (act->happens_before(curr) && act != curr) {
+ if (act->happens_before(curr)) {
if (act->is_write()) {
- if (!act->equals(rf)) {
- added = mo_graph->addEdge(act, rf) || added;
- }
+ added = mo_graph->addEdge(act, rf) || added;
} else {
const ModelAction *prevrf = act->get_reads_from();
const Promise *prevrf_promise = act->get_reads_from_promise();
* 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, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv)
+bool ModelChecker::w_modification_order(ModelAction *curr, ModelVector<ModelAction *> *send_fv)
{
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ SnapVector<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());
/** Arbitrary reads from the future are not allowed. Section 29.3
* part 9 places some constraints. This method checks one result of constraint
* constraint. Others require compiler support. */
-bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
+bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const
{
if (!writer->is_rmw())
return true;
*/
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
{
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
+ SnapVector<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++) {
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());
+ SnapVector<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;
bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
{
bool updated = false;
- std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
+ SnapVector<struct release_seq *>::iterator it = pending_rel_seqs->begin();
while (it != pending_rel_seqs->end()) {
struct release_seq *pending = *it;
ModelAction *acquire = pending->acquire;
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);
if (uninit)
action_trace->push_front(uninit);
- std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
+ SnapVector<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);
void *mutex_loc = (void *) act->get_value();
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);
+ SnapVector<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);
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++)
- if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
+ for (rit = list->rbegin(); (*rit) != curr; rit++)
+ ;
+ rit++; /* Skip past curr */
+ for ( ; rit != list->rend(); rit++)
+ if ((*rit)->is_write() && (*rit)->is_seqcst())
return *rit;
return NULL;
}
}
/**
- * @brief Find the promise, if any to resolve for the current action
+ * @brief Find the promise (if any) to resolve for the current action and
+ * remove it from the pending promise vector
* @param curr The current ModelAction. Should be a write.
- * @return The (non-negative) index for the Promise to resolve, if any;
- * otherwise -1
+ * @return The Promise to resolve, if any; otherwise NULL
*/
-int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
+Promise * ModelChecker::pop_promise_to_resolve(const ModelAction *curr)
{
for (unsigned int i = 0; i < promises->size(); i++)
- if (curr->get_node()->get_promise(i))
- return i;
- return -1;
+ if (curr->get_node()->get_promise(i)) {
+ Promise *ret = (*promises)[i];
+ promises->erase(promises->begin() + i);
+ return ret;
+ }
+ return NULL;
}
/**
* Resolve a Promise with a current write.
* @param write The ModelAction that is fulfilling Promises
- * @param promise_idx The index corresponding to the promise
+ * @param promise The Promise to resolve
* @return True if the Promise was successfully resolved; false otherwise
*/
-bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
+bool ModelChecker::resolve_promise(ModelAction *write, Promise *promise)
{
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
- Promise *promise = (*promises)[promise_idx];
+ ModelVector<ModelAction *> actions_to_check;
for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
ModelAction *read = promise->get_reader(i);
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
*/
void ModelChecker::build_may_read_from(ModelAction *curr)
{
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ SnapVector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
}
/**
- * @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");
+ }
}
/**
scheduler->add_thread(t);
}
-/**
- * Removes a thread from the scheduler.
- * @param the thread to remove.
- */
-void ModelChecker::remove_thread(Thread *t)
-{
- scheduler->remove_thread(t);
-}
-
/**
* @brief Get a Thread reference by its ID
* @param tid The Thread's ID
{
DBG();
Thread *old = thread_current();
+ scheduler->set_current_thread(NULL);
ASSERT(!old->get_pending());
old->set_pending(act);
if (Thread::swap(old, &system_context) < 0) {
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 (thr->is_waiting_on(thr))
+ assert_bug("Deadlock detected");
}
}