#include "promise.h"
#include "datarace.h"
#include "mutex.h"
+#include "threads.h"
#define INITIAL_THREAD_ID 0
num_executions(0),
num_feasible_executions(0),
diverge(NULL),
+ earliest_diverge(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>()),
mo_graph(new CycleGraph()),
failed_promise(false),
too_many_reads(false),
- asserted(false)
+ asserted(false),
+ bad_synchronization(false)
{
/* Allocate this "size" on the snapshotting heap */
priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
node_stack->reset_execution();
failed_promise = false;
too_many_reads = false;
+ bad_synchronization = false;
reset_asserted();
snapshotObject->backTrackBeforeStep(0);
}
return priv->next_thread_id;
}
+/** @return The currently executing Thread. */
+Thread * ModelChecker::get_current_thread()
+{
+ return scheduler->get_current_thread();
+}
+
/** @return a sequence number for a new ModelAction */
modelclock_t ModelChecker::get_next_seq_num()
{
ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
+ if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+ earliest_diverge=diverge;
+
Node *nextnode = next->get_node();
/* Reached divergence point */
if (nextnode->increment_promise()) {
Node *node = nextnode->get_parent();
tid = node->get_next_backtrack();
node_stack->pop_restofstack(1);
+ if (diverge==earliest_diverge) {
+ earliest_diverge=node->get_action();
+ }
}
DEBUG("*** Divergence point ***\n");
+
diverge = NULL;
} else {
tid = next->get_tid();
DBG();
num_executions++;
- if (isfinalfeasible())
+
+ if (isfinalfeasible()) {
+ printf("Earliest divergence point since last feasible execution:\n");
+ if (earliest_diverge)
+ earliest_diverge->print(false);
+ else
+ printf("(Not set)\n");
+
+ earliest_diverge = NULL;
num_feasible_executions++;
+ }
+
+ DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+ pending_acq_rel_seq->size());
if (isfinalfeasible() || DBG_ENABLED())
print_summary();
*
* @param the ModelAction to find backtracking points for.
*/
-
-
void ModelChecker::set_backtracking(ModelAction *act)
{
Thread *t = get_thread(act);
bool r_status = false;
if (!second_part_of_rmw) {
- check_recency(curr);
+ check_recency(curr, reads_from);
r_status = r_modification_order(curr, reads_from);
}
*
* The unlock operation has to re-enable all of the threads that are
* waiting on the lock.
+ *
+ * @return True if synchronization was updated; false otherwise
*/
-void ModelChecker::process_mutex(ModelAction *curr) {
+bool ModelChecker::process_mutex(ModelAction *curr) {
std::mutex *mutex = (std::mutex *)curr->get_location();
struct std::mutex_state *state = mutex->get_state();
switch (curr->get_type()) {
state->islocked = true;
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
- if (unlock != NULL)
+ if (unlock != NULL) {
curr->synchronize_with(unlock);
+ return true;
+ }
break;
}
case ATOMIC_UNLOCK: {
action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
- scheduler->add_thread(get_thread((*rit)->get_tid()));
+ scheduler->wake(get_thread(*rit));
}
waiters->clear();
break;
default:
ASSERT(0);
}
+ return false;
}
/**
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated or a thread completed
*/
bool ModelChecker::process_thread_action(ModelAction *curr)
{
- bool synchronized = false;
+ bool updated = false;
switch (curr->get_type()) {
case THREAD_CREATE: {
scheduler->sleep(waiting);
} else {
do_complete_join(curr);
- synchronized = true;
+ updated = true; /* trigger rel-seq checks */
}
break;
}
Thread *wake = get_thread(act);
scheduler->wake(wake);
do_complete_join(act);
- synchronized = true;
+ updated = true; /* trigger rel-seq checks */
}
th->complete();
+ updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
break;
}
- return synchronized;
+ return updated;
}
/**
if (curr->is_rmwc() || curr->is_rmw()) {
newcurr = process_rmw(curr);
delete curr;
- compute_promises(newcurr);
+
+ if (newcurr->is_rmw())
+ compute_promises(newcurr);
return newcurr;
}
+ curr->set_seq_number(get_next_seq_num());
+
newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
if (newcurr) {
/* First restore type and order in case of RMW operation */
/* Discard duplicate ModelAction; use action from NodeStack */
delete curr;
- /* If we have diverged, we need to reset the clock vector. */
- if (diverge == NULL)
- newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+ /* Always compute new clock vector */
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
} else {
newcurr = curr;
+
+ /* Always compute new clock vector */
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
/*
* Perform one-time actions when pushing new ModelAction onto
* NodeStack
*/
- curr->create_cv(get_parent_action(curr->get_tid()));
- if (curr->is_write())
- compute_promises(curr);
+ if (newcurr->is_write())
+ compute_promises(newcurr);
}
return newcurr;
}
* @param curr is the ModelAction to check whether it is enabled.
* @return a bool that indicates whether the action is enabled.
*/
-
bool ModelChecker::check_action_enabled(ModelAction *curr) {
if (curr->is_lock()) {
std::mutex * lock = (std::mutex *)curr->get_location();
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
if (!check_action_enabled(curr)) {
- //we'll make the execution look like we chose to run this action
- //much later...when a lock is actually available to relese
+ /* Make the execution look like we chose to run this action
+ * much later, when a lock is actually available to release */
get_current_thread()->set_pending(curr);
- remove_thread(get_current_thread());
+ scheduler->sleep(get_current_thread());
return get_next_thread(NULL);
}
build_reads_from_past(curr);
curr = newcurr;
+ /* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
while (!work_queue.empty()) {
switch (work.type) {
case WORK_CHECK_CURR_ACTION: {
ModelAction *act = work.action;
- bool updated = false;
+ bool update = false; /* update this location's release seq's */
+ bool update_all = false; /* update all release seq's */
- process_thread_action(curr);
+ if (process_thread_action(curr))
+ update_all = true;
if (act->is_read() && process_read(act, second_part_of_rmw))
- updated = true;
+ update = true;
if (act->is_write() && process_write(act))
- updated = true;
+ update = true;
- if (act->is_mutex_op())
- process_mutex(act);
+ if (act->is_mutex_op() && process_mutex(act))
+ update_all = true;
- if (updated)
+ if (update_all)
+ work_queue.push_back(CheckRelSeqWorkEntry(NULL));
+ else if (update)
work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
break;
}
bool updated = false;
if (act->is_read()) {
- if (r_modification_order(act, act->get_reads_from()))
+ const ModelAction *rf = act->get_reads_from();
+ if (rf != NULL && r_modification_order(act, rf))
updated = true;
}
if (act->is_write()) {
if (w_modification_order(act))
updated = true;
}
+ mo_graph->commitChanges();
if (updated)
work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
/** @return whether the current partial trace is feasible. */
bool ModelChecker::isfeasible() {
+ if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
+ DEBUG("Infeasible: RMW violation\n");
+
return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
}
DEBUG("Infeasible: failed promise\n");
if (too_many_reads)
DEBUG("Infeasible: too many reads\n");
+ if (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 && !promises_expired();
+ return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
}
/** Returns whether the current completed trace is feasible. */
*
* If so, we decide that the execution is no longer feasible.
*/
-void ModelChecker::check_recency(ModelAction *curr) {
+void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
if (params.maxreads != 0) {
+
if (curr->get_node()->get_read_from_size() <= 1)
return;
-
//Must make sure that execution is currently feasible... We could
//accidentally clear by rolling back
if (!isfeasible())
return;
-
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(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();
ModelAction *act = *rit;
if (!act->is_read())
return;
- if (act->get_reads_from() != curr->get_reads_from())
+
+ if (act->get_reads_from() != rf)
return;
if (act->get_node()->get_read_from_size() <= 1)
return;
}
-
for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
//Get write
const ModelAction * write = curr->get_node()->get_read_from_at(i);
+
//Need a different write
- if (write==curr->get_reads_from())
+ if (write==rf)
continue;
/* Test to see whether this is a feasible write to read from*/
}
} else {
const ModelAction *prevreadfrom = act->get_reads_from();
- if (prevreadfrom != NULL && rf != prevreadfrom) {
+ //if the previous read is unresolved, keep going...
+ if (prevreadfrom == NULL)
+ continue;
+
+ if (rf != prevreadfrom) {
mo_graph->addEdge(prevreadfrom, rf);
added = true;
}
* @param rf is the write ModelAction that curr reads from.
*
*/
-
void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
action_list_t::reverse_iterator rit;
ModelAction *lastact = NULL;
- /* Find last action that happens after curr */
+ /* Find last action that happens after curr that is either not curr or a rmw */
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (curr->happens_before(act)) {
+ if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
lastact = act;
} else
break;
/* Include at most one act per-thread that "happens before" curr */
if (lastact != NULL) {
- if (lastact->is_read()) {
+ if (lastact==curr) {
+ //Case 1: The resolved read is a RMW, and we need to make sure
+ //that the write portion of the RMW mod order after rf
+
+ mo_graph->addEdge(rf, lastact);
+ } else if (lastact->is_read()) {
+ //Case 2: The resolved read is a normal read and the next
+ //operation is a read, and we need to make sure the value read
+ //is mod ordered after rf
+
const ModelAction *postreadfrom = lastact->get_reads_from();
if (postreadfrom != NULL&&rf != postreadfrom)
mo_graph->addEdge(rf, postreadfrom);
- } else if (rf != lastact) {
- mo_graph->addEdge(rf, lastact);
+ } else {
+ //Case 3: The resolved read is a normal read and the next
+ //operation is a write, and we need to make sure that the
+ //write is mod ordered after rf
+ if (lastact!=rf)
+ mo_graph->addEdge(rf, lastact);
}
break;
}
ModelAction *act = *rit;
if (act == curr) {
/*
- * If RMW, we already have all relevant edges,
- * so just skip to next thread.
- * If normal write, we need to look at earlier
- * actions, so continue processing list.
+ * 1) If RMW and it actually read from something, then we
+ * already have all relevant edges, so just skip to next
+ * thread.
+ *
+ * 2) If RMW and it didn't read from anything, we should
+ * whatever edge we can get to speed up convergence.
+ *
+ * 3) If normal write, we need to look at earlier actions, so
+ * continue processing list.
*/
- if (curr->is_rmw())
- break;
- else
+ if (curr->is_rmw()) {
+ if (curr->get_reads_from()!=NULL)
+ break;
+ else
+ continue;
+ } else
continue;
}
*/
if (act->is_write())
mo_graph->addEdge(act, curr);
- else if (act->is_read() && act->get_reads_from() != NULL)
+ else if (act->is_read()) {
+ //if previous read accessed a null, just keep going
+ if (act->get_reads_from() == NULL)
+ continue;
mo_graph->addEdge(act->get_reads_from(), curr);
+ }
added = true;
break;
} else if (act->is_read() && !act->is_synchronizing(curr) &&
/** 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) {
if (!writer->is_rmw())
return true;
*/
bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
{
+ /* Only check for release sequences if there are no cycles */
+ if (mo_graph->checkForCycles())
+ return false;
+
while (rf) {
ASSERT(rf->is_write());
bool future_ordered = false;
ModelAction *last = get_last_action(int_to_id(i));
- if (last && rf->happens_before(last))
+ if (last && (rf->happens_before(last) ||
+ last->get_type() == THREAD_FINISH))
future_ordered = true;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
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 (act->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));
/* propagate synchronization to later actions */
- action_list_t::reverse_iterator it = action_trace->rbegin();
- for (; (*it) != act; it++) {
- ModelAction *propagate = *it;
+ action_list_t::reverse_iterator rit = action_trace->rbegin();
+ for (; (*rit) != act; rit++) {
+ ModelAction *propagate = *rit;
if (act->happens_before(propagate)) {
propagate->synchronize_with(act);
/* Re-check 'propagate' for mo_graph edges */
Promise *promise = (*promises)[promise_index];
if (write->get_node()->get_promise(i)) {
ModelAction *read = promise->get_action();
- read->read_from(write);
if (read->is_rmw()) {
mo_graph->addRMWEdge(write, read);
}
+ read->read_from(write);
//First fix up the modification order for actions that happened
//before the read
r_modification_order(read, write);
//Next fix up the modification order for actions that happened
//after the read.
post_r_modification_order(read, write);
+ //Make sure the promise's value matches the write's value
+ ASSERT(promise->get_value() == write->get_value());
+
+ delete(promise);
promises->erase(promises->begin() + promise_index);
resolved = true;
} else
printf("---------------------------------------------------------------------\n");
}
+#if SUPPORT_MOD_ORDER_DUMP
+void ModelChecker::dumpGraph(char *filename) {
+ char buffer[200];
+ sprintf(buffer, "%s.dot",filename);
+ FILE *file=fopen(buffer, "w");
+ fprintf(file, "digraph %s {\n",filename);
+ mo_graph->dumpNodes(file);
+ ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
+
+ for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
+ ModelAction *action=*it;
+ if (action->is_read()) {
+ fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
+ if (action->get_reads_from()!=NULL)
+ fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+ }
+ if (thread_array[action->get_tid()] != NULL) {
+ fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
+ }
+
+ thread_array[action->get_tid()]=action;
+ }
+ fprintf(file,"}\n");
+ model_free(thread_array);
+ fclose(file);
+}
+#endif
+
void ModelChecker::print_summary()
{
printf("\n");
char buffername[100];
sprintf(buffername, "exec%04u", num_executions);
mo_graph->dumpGraphToFile(buffername);
+ sprintf(buffername, "graph%04u", num_executions);
+ dumpGraph(buffername);
#endif
if (!isfinalfeasible())
* 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
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(thread_id_t tid)
+{
+ return thread_map->get(id_to_int(tid));
+}
+
+/**
+ * @brief Get a reference to the Thread in which a ModelAction was executed
+ * @param act The ModelAction
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(ModelAction *act)
+{
+ return get_thread(act->get_tid());
+}
+
/**
* Switch from a user-context to the "master thread" context (a.k.a. system
* 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. Must not be NULL.
+ *
+ * @param act The current action that will be explored. May be NULL only if
+ * trace is exiting via an assertion (see ModelChecker::set_assert and
+ * ModelChecker::has_asserted).
* @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
*/
int ModelChecker::switch_to_master(ModelAction *act)
priv->nextThread = check_current_action(priv->current_action);
priv->current_action = NULL;
+
if (curr->is_blocked() || curr->is_complete())
scheduler->remove_thread(curr);
} else {
projects / model-checker.git / blobdiff