DBG();
num_executions++;
+
if (isfinalfeasible()) {
printf("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
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();
//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
* 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)