{
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() ||
- mo_graph->checkForCycles() ||
+ return mo_graph->checkForCycles() ||
priv->failed_promise ||
priv->too_many_reads ||
priv->bad_synchronization ||
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);