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 *, SnapVector<action_list_t> *, uintptr_t, 4 >()),
promises(new SnapVector<Promise *>()),
delete obj_thrd_map;
delete obj_map;
- delete lock_waiters_map;
delete condvar_waiters_map;
delete action_trace;
DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
- /* Print all model-checker output before rollback */
- fflush(model_out);
-
/**
* FIXME: if we utilize partial rollback, we will need to free only
* those pending actions which were NOT pending before the rollback
scheduler->update_sleep_set(prevnode);
/* Reached divergence point */
- if (nextnode->increment_misc()) {
- /* The next node will try to satisfy a different misc_index values. */
- tid = next->get_tid();
- node_stack->pop_restofstack(2);
- } else if (nextnode->increment_promise()) {
- /* The next node will try to satisfy a different set of promises. */
- tid = next->get_tid();
- node_stack->pop_restofstack(2);
- } else if (nextnode->increment_read_from()) {
- /* The next node will read from a different value. */
- tid = next->get_tid();
- node_stack->pop_restofstack(2);
- } else if (nextnode->increment_relseq_break()) {
- /* The next node will try to resolve a release sequence differently */
+ if (nextnode->increment_behaviors()) {
+ /* Execute the same thread with a new behavior */
tid = next->get_tid();
node_stack->pop_restofstack(2);
} else {
}
DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
ASSERT(tid != THREAD_ID_T_NONE);
- return thread_map->get(id_to_int(tid));
+ return get_thread(id_to_int(tid));
}
/**
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
Node *node = prev->get_node()->get_parent();
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
int low_tid, high_tid;
if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
low_tid = id_to_int(act->get_tid());
if (i >= node->get_num_threads())
break;
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
/* Don't backtrack into a point where the thread is disabled or sleeping. */
if (node->enabled_status(tid) != THREAD_ENABLED)
continue;
}
break;
}
+ case ATOMIC_WAIT:
case ATOMIC_UNLOCK: {
- //unlock the lock
- 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
- for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
- scheduler->wake(get_thread(*rit));
+ /* wake up the other threads */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *t = get_thread(int_to_id(i));
+ Thread *curr_thrd = get_thread(curr);
+ if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+ scheduler->wake(t);
}
- waiters->clear();
- break;
- }
- case ATOMIC_WAIT: {
- //unlock the lock
+
+ /* unlock the lock - after checking who was waiting on it */
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
- 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->is_wait())
+ break; /* The rest is only for ATOMIC_WAIT */
+
+ /* Should we go to sleep? (simulate spurious failures) */
if (curr->get_node()->get_misc() == 0) {
get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
- //disable us
+ /* disable us */
scheduler->sleep(get_thread(curr));
}
break;
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);
}
/**
} 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->empty()) {
- for (unsigned int i = 0; i < futurevalues->size(); i++) {
- struct PendingFutureValue pfv = (*futurevalues)[i];
+ /* 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();
}
case THREAD_FINISH: {
Thread *th = get_thread(curr);
- while (!th->wait_list_empty()) {
- ModelAction *act = th->pop_wait_list();
- scheduler->wake(get_thread(act));
+ /* Wake up any joining threads */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *waiting = get_thread(int_to_id(i));
+ if (waiting->waiting_on() == th &&
+ waiting->get_pending()->is_thread_join())
+ scheduler->wake(waiting);
}
th->complete();
/* Completed thread can't satisfy promises */
*/
bool ModelChecker::check_action_enabled(ModelAction *curr) {
if (curr->is_lock()) {
- std::mutex *lock = (std::mutex *)curr->get_location();
+ std::mutex *lock = curr->get_mutex();
struct std::mutex_state *state = lock->get_state();
- if (state->locked) {
- //Stick the action in the appropriate waiting queue
- get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
+ if (state->locked)
return false;
- }
- } else if (curr->get_type() == THREAD_JOIN) {
- Thread *blocking = (Thread *)curr->get_location();
+ } else if (curr->is_thread_join()) {
+ Thread *blocking = curr->get_thread_operand();
if (!blocking->is_complete()) {
- blocking->push_wait_list(curr);
thread_blocking_check_promises(blocking, get_thread(curr));
return false;
}
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))
+ if (thr->is_waiting_on(thr))
assert_bug("Deadlock detected");
}
}
projects / model-checker.git / blobdiff