void ModelChecker::record_stats()
{
stats.num_total++;
- if (!isfinalfeasible())
+ if (!isfeasibleprefix())
stats.num_infeasible++;
else if (have_bug_reports())
stats.num_buggy_executions++;
{
DBG();
/* Is this execution a feasible execution that's worth bug-checking? */
- bool complete = isfinalfeasible() && (is_complete_execution() ||
+ bool complete = isfeasibleprefix() && (is_complete_execution() ||
have_bug_reports());
/* End-of-execution bug checks */
}
- if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
+ if (!second_part_of_rmw&&is_infeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
mo_graph->rollbackChanges();
priv->too_many_reads = false;
continue;
return false;
}
-/** @return whether the current partial trace must be a prefix of a
- * feasible trace. */
+/**
+ * This is the strongest feasibility check available.
+ * @return whether the current trace (partial or complete) must be a prefix of
+ * a feasible trace.
+ */
bool ModelChecker::isfeasibleprefix() const
{
- return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
+ return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
+}
+
+/**
+ * Returns whether the current completed trace is feasible, except for pending
+ * release sequences.
+ */
+bool ModelChecker::is_feasible_prefix_ignore_relseq() const
+{
+ if (DBG_ENABLED() && promises->size() != 0)
+ DEBUG("Infeasible: unrevolved promises\n");
+
+ return !is_infeasible() && promises->size() == 0;
}
-/** @return whether the current partial trace is feasible. */
-bool ModelChecker::isfeasible() const
+/**
+ * Check if the current partial trace is infeasible. Does not check any
+ * end-of-execution flags, which might rule out the execution. Thus, this is
+ * useful only for ruling an execution as infeasible.
+ * @return whether the current partial trace is infeasible.
+ */
+bool ModelChecker::is_infeasible() const
{
if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
DEBUG("Infeasible: RMW violation\n");
- return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
+ return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
}
-/** @return whether the current partial trace is feasible other than
- * multiple RMW reading from the same store. */
-bool ModelChecker::isfeasibleotherthanRMW() const
+/**
+ * Check If the current partial trace is infeasible, while ignoring
+ * infeasibility related to 2 RMW's reading from the same store. It does not
+ * check end-of-execution feasibility.
+ * @see ModelChecker::is_infeasible
+ * @return whether the current partial trace is infeasible, ignoring multiple
+ * RMWs reading from the same store.
+ * */
+bool ModelChecker::is_infeasible_ignoreRMW() const
{
if (DBG_ENABLED()) {
if (mo_graph->checkForCycles())
if (promises_expired())
DEBUG("Infeasible: promises expired\n");
}
- return !mo_graph->checkForCycles() && !priv->failed_promise && !priv->too_many_reads && !priv->bad_synchronization && !promises_expired();
-}
-
-/** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() const
-{
- if (DBG_ENABLED() && promises->size() != 0)
- DEBUG("Infeasible: unrevolved promises\n");
-
- return isfeasible() && promises->size() == 0;
+ return mo_graph->checkForCycles() || priv->failed_promise ||
+ priv->too_many_reads || priv->bad_synchronization ||
+ promises_expired();
}
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
return;
//Must make sure that execution is currently feasible... We could
//accidentally clear by rolling back
- if (!isfeasible())
+ 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());
/* Test to see whether this is a feasible write to read from*/
mo_graph->startChanges();
r_modification_order(curr, write);
- bool feasiblereadfrom = isfeasible();
+ bool feasiblereadfrom = !is_infeasible();
mo_graph->rollbackChanges();
if (!feasiblereadfrom)
*/
if (thin_air_constraint_may_allow(curr, act)) {
- if (isfeasible() ||
- (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
+ if (!is_infeasible() ||
+ (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
struct PendingFutureValue pfv = {curr,act};
futurevalues->push_back(pfv);
}
dumpGraph(buffername);
#endif
- if (!isfinalfeasible())
+ if (!isfeasibleprefix())
model_print("INFEASIBLE EXECUTION!\n");
print_list(action_trace, stats.num_total);
model_print("\n");
Thread *next = scheduler->next_thread(priv->nextThread);
/* Infeasible -> don't take any more steps */
- if (!isfeasible())
+ if (is_infeasible())
return false;
else if (isfeasibleprefix() && have_bug_reports()) {
set_assert();
* (4) no pending promises
*/
if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
- isfinalfeasible() && !unrealizedraces.empty()) {
+ is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
pending_rel_seqs->size());
ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
return (Thread::swap(&system_context, next) == 0);
}
-/** Runs the current execution until threre are no more steps to take. */
-void ModelChecker::finish_execution() {
- DBG();
-
- while (take_step());
-}
-
/** Wrapper to run the user's main function, with appropriate arguments */
void user_main_wrapper(void *)
{
add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
/* Wait for all threads to complete */
- finish_execution();
+ while (take_step());
} while (next_execution());
print_stats();
projects / c11tester.git / blobdiff