}
/** @return the number of user threads created during this execution */
-unsigned int ModelChecker::get_num_threads()
+unsigned int ModelChecker::get_num_threads() const
{
return priv->next_thread_id;
}
return thread_map->get(id_to_int(tid));
}
-/**
+/**
* We need to know what the next actions of all threads in the sleep
* set will be. This method computes them and stores the actions at
* the corresponding thread object's pending action.
for(unsigned int i=0;i<get_num_threads();i++) {
thread_id_t tid=int_to_id(i);
Thread *thr=get_thread(tid);
- if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
+ if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
+ thr->get_pending() == NULL ) {
thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
Thread *thr=get_thread(tid);
if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
ModelAction *pending_act=thr->get_pending();
- if (pending_act->could_synchronize_with(curr)) {
+ if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) {
//Remove this thread from sleep set
scheduler->remove_sleep(thr);
}
}
- }
+ }
+}
+
+/**
+ * Check if we are in a deadlock. Should only be called at the end of an
+ * execution, although it should not give false positives in the middle of an
+ * execution (there should be some ENABLED thread).
+ *
+ * @return True if program is in a deadlock; false otherwise
+ */
+bool ModelChecker::is_deadlocked() const
+{
+ bool blocking_threads = false;
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *t = get_thread(int_to_id(i));
+ if (scheduler->is_enabled(t) != THREAD_DISABLED)
+ return false;
+ else if (!t->is_model_thread() && t->get_pending())
+ blocking_threads = true;
+ }
+ return blocking_threads;
}
/**
num_executions++;
+ if (is_deadlocked())
+ printf("ERROR: DEADLOCK\n");
if (isfinalfeasible()) {
printf("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
pending_rel_seqs->size());
- if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
+ if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+ checkDataRaces();
print_summary();
+ }
if ((diverge = get_next_backtrack()) == NULL)
return false;
for(int i = low_tid; i < high_tid; i++) {
thread_id_t tid = int_to_id(i);
+ /* Make sure this thread can be enabled here. */
+ if (i >= node->get_num_threads())
+ break;
+
/* Don't backtrack into a point where the thread is disabled or sleeping. */
- if (node->get_enabled_array()[i]!=THREAD_ENABLED)
+ if (node->enabled_status(tid)!=THREAD_ENABLED)
continue;
-
+
/* Check if this has been explored already */
if (node->has_been_explored(tid))
continue;
*/
bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
{
- uint64_t value;
+ uint64_t value = VALUE_NONE;
bool updated = false;
while (true) {
const ModelAction *reads_from = curr->get_node()->get_read_from();
* initializing clock vectors, and computing the promises to fulfill.
*
* @param curr The current action, as passed from the user context; may be
- * freed/invalidated after the execution of this function
- * @return The current action, as processed by the ModelChecker. Is only the
- * same as the parameter @a curr if this is a newly-explored action.
+ * freed/invalidated after the execution of this function, with a different
+ * action "returned" its place (pass-by-reference)
+ * @return True if curr is a newly-explored action; false otherwise
*/
-ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
+bool ModelChecker::initialize_curr_action(ModelAction **curr)
{
ModelAction *newcurr;
- if (curr->is_rmwc() || curr->is_rmw()) {
- newcurr = process_rmw(curr);
- delete curr;
+ if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
+ newcurr = process_rmw(*curr);
+ delete *curr;
if (newcurr->is_rmw())
compute_promises(newcurr);
- return newcurr;
+
+ *curr = newcurr;
+ return false;
}
- curr->set_seq_number(get_next_seq_num());
+ (*curr)->set_seq_number(get_next_seq_num());
- newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
+ newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
if (newcurr) {
/* First restore type and order in case of RMW operation */
- if (curr->is_rmwr())
- newcurr->copy_typeandorder(curr);
+ if ((*curr)->is_rmwr())
+ newcurr->copy_typeandorder(*curr);
- ASSERT(curr->get_location() == newcurr->get_location());
- newcurr->copy_from_new(curr);
+ ASSERT((*curr)->get_location() == newcurr->get_location());
+ newcurr->copy_from_new(*curr);
/* Discard duplicate ModelAction; use action from NodeStack */
- delete curr;
+ delete *curr;
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ *curr = newcurr;
+ return false; /* Action was explored previously */
} else {
- newcurr = curr;
+ newcurr = *curr;
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
else if (newcurr->is_notify_one()) {
newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
}
+ return true; /* This was a new ModelAction */
}
- return newcurr;
}
/**
return get_next_thread(NULL);
}
- ModelAction *newcurr = initialize_curr_action(curr);
+ bool newly_explored = initialize_curr_action(&curr);
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
if (!second_part_of_rmw)
- add_action_to_lists(newcurr);
+ add_action_to_lists(curr);
/* Build may_read_from set for newly-created actions */
- if (curr == newcurr && curr->is_read())
+ if (newly_explored && curr->is_read())
build_reads_from_past(curr);
- curr = newcurr;
/* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
/** @return whether the current partial trace must be a prefix of a
* feasible trace. */
bool ModelChecker::isfeasibleprefix() {
- return promises->size() == 0 && pending_rel_seqs->size() == 0;
+ return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
}
/** @return whether the current partial trace is feasible. */
ModelAction *act = *rit;
if (!act->is_read())
return;
-
+
if (act->get_reads_from() != rf)
return;
if (act->get_node()->get_read_from_size() <= 1)
ModelAction *act=*rit;
bool foundvalue = false;
for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
- if (act->get_node()->get_read_from_at(i)==write) {
+ if (act->get_node()->get_read_from_at(j)==write) {
foundvalue = true;
break;
}
* 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.
*
if (curr->is_rmw()) {
if (curr->get_reads_from()!=NULL)
break;
- else
+ else
continue;
} else
continue;
*/
if (act->is_write())
mo_graph->addEdge(act, curr);
- else if (act->is_read()) {
+ else if (act->is_read()) {
//if previous read accessed a null, just keep going
if (act->get_reads_from() == NULL)
continue;
return true;
}
-/** 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::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
+/**
+ * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
+ * some constraints. This method checks one the following constraint (others
+ * require compiler support):
+ *
+ * If X --hb-> Y --mo-> Z, then X should not read from Z.
+ */
+bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
+{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+ unsigned int i;
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ const ModelAction *write_after_read = NULL;
- //Get write that follows reader action
- action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
- action_list_t::reverse_iterator rit;
- ModelAction *first_write_after_read=NULL;
-
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
- if (act==reader)
- break;
- if (act->is_write())
- first_write_after_read=act;
- }
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
- if (first_write_after_read==NULL)
- return true;
+ if (!reader->happens_before(act))
+ break;
+ else if (act->is_write())
+ write_after_read = act;
+ else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
+ write_after_read = act->get_reads_from();
+ }
+ }
- return !mo_graph->checkReachable(first_write_after_read, writer);
+ if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
+ return false;
+ }
+ return true;
}
-
-
/**
* Finds the head(s) of the release sequence(s) containing a given ModelAction.
* The ModelAction under consideration is expected to be taking part in
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
obj_map->get_safe_ptr(mutex_loc)->push_back(act);
-
+
std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
//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);
threads_to_check.push_back(read->get_tid());
!act->same_thread(curr) &&
act->get_location() == curr->get_location() &&
promise->get_value() == curr->get_value()) {
- curr->get_node()->set_promise(i);
+ curr->get_node()->set_promise(i, act->is_rmw());
}
}
}
}
}
+void ModelChecker::check_promises_thread_disabled() {
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ if (promise->check_promise()) {
+ failed_promise = true;
+ return;
+ }
+ }
+}
+
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
- *
+ *
* pread is the read that created the promise
*
* pwrite is either the first write to same location as pread by
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
const ModelAction *act = promise->get_action();
-
+
//Is this promise on the same location?
if ( act->get_location() != location )
continue;
return;
}
}
-
+
//Don't do any lookups twice for the same thread
if (promise->has_sync_thread(tid))
continue;
-
- if (mo_graph->checkReachable(promise->get_write(), write)) {
+
+ if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
failed_promise = true;
return;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
- DEBUG("Adding action to may_read_from:\n");
- if (DBG_ENABLED()) {
- act->print();
- curr->print();
- }
-
- if (curr->get_sleep_flag() && ! curr->is_seqcst()) {
- if (sleep_can_read_from(curr, act))
- curr->get_node()->add_read_from(act);
- } else
+ if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
+ DEBUG("Adding action to may_read_from:\n");
+ if (DBG_ENABLED()) {
+ act->print();
+ curr->print();
+ }
curr->get_node()->add_read_from(act);
+ }
}
/* Include at most one act per-thread that "happens before" curr */
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
while(true) {
Node *prevnode=write->get_node()->get_parent();
- bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+
+ bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
if (write->is_release()&&thread_sleep)
return true;
if (!write->is_rmw()) {
printf("---------------------------------------------------------------------\n");
printf("Trace:\n");
unsigned int hash=0;
-
+
for (it = list->begin(); it != list->end(); it++) {
(*it)->print();
hash=hash^(hash<<3)^((*it)->hash());
#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);
+ 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()) {
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");
+ fprintf(file,"}\n");
model_free(thread_array);
- fclose(file);
+ fclose(file);
}
#endif
sprintf(buffername, "exec%04u", num_executions);
mo_graph->dumpGraphToFile(buffername);
sprintf(buffername, "graph%04u", num_executions);
- dumpGraph(buffername);
+ dumpGraph(buffername);
#endif
if (!isfinalfeasible())
}
/**
- * Removes a thread from the scheduler.
+ * Removes a thread from the scheduler.
* @param the thread to remove.
*/
void ModelChecker::remove_thread(Thread *t)
projects / c11tester.git / blobdiff