{
char buf[100];
char *ptr = buf;
- if (mo_graph->checkForRMWViolation())
- ptr += sprintf(ptr, "[RMW atomicity]");
if (mo_graph->checkForCycles())
ptr += sprintf(ptr, "[mo cycle]");
if (priv->failed_promise)
*/
bool ModelChecker::is_infeasible() const
{
- return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
-}
-
-/**
- * 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
-{
- return mo_graph->checkForCycles() || priv->failed_promise ||
- priv->too_many_reads || priv->bad_synchronization ||
+ return mo_graph->checkForCycles() ||
+ priv->failed_promise ||
+ priv->too_many_reads ||
+ priv->bad_synchronization ||
promises_expired();
}
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);
+ delete promise;
promises->erase(promises->begin() + promise_index);
actions_to_check.push_back(read);
void ModelChecker::print_summary() const
{
#if SUPPORT_MOD_ORDER_DUMP
- scheduler->print();
char buffername[100];
sprintf(buffername, "exec%04u", stats.num_total);
mo_graph->dumpGraphToFile(buffername);