Because we've removed some of the special-casing for RMW atomicity
violations, we don't need the separate 'hasRMWViolation' condition;
instead, we should explicitly flag atomicity violations as a cycle.
Previously, there was a subtle bug related to this issue, where cycles
were flagged only as RMW violations and did not show up to the
model-checker at the appropriate points.
CycleGraph::CycleGraph() :
discovered(new HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
hasCycles(false),
CycleGraph::CycleGraph() :
discovered(new HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
hasCycles(false),
- oldCycles(false),
- hasRMWViolation(false),
- oldRMWViolation(false)
CycleNode *rmwnode = getNode(rmw);
/* Two RMW actions cannot read from the same write. */
CycleNode *rmwnode = getNode(rmw);
/* Two RMW actions cannot read from the same write. */
- if (fromnode->setRMW(rmwnode)) {
- hasRMWViolation = true;
- } else {
+ if (fromnode->setRMW(rmwnode))
+ hasCycles = true;
+ else
rmwrollbackvector.push_back(fromnode);
rmwrollbackvector.push_back(fromnode);
/* Transfer all outgoing edges from the from node to the rmw node */
/* This process should not add a cycle because either:
/* Transfer all outgoing edges from the from node to the rmw node */
/* This process should not add a cycle because either:
ASSERT(rollbackvector.size() == 0);
ASSERT(rmwrollbackvector.size() == 0);
ASSERT(oldCycles == hasCycles);
ASSERT(rollbackvector.size() == 0);
ASSERT(rmwrollbackvector.size() == 0);
ASSERT(oldCycles == hasCycles);
- ASSERT(oldRMWViolation == hasRMWViolation);
}
/** Commit changes to the cyclegraph. */
}
/** Commit changes to the cyclegraph. */
rollbackvector.resize(0);
rmwrollbackvector.resize(0);
oldCycles = hasCycles;
rollbackvector.resize(0);
rmwrollbackvector.resize(0);
oldCycles = hasCycles;
- oldRMWViolation = hasRMWViolation;
}
/** Rollback changes to the previous commit. */
}
/** Rollback changes to the previous commit. */
- hasRMWViolation = oldRMWViolation;
rollbackvector.resize(0);
rmwrollbackvector.resize(0);
}
rollbackvector.resize(0);
rmwrollbackvector.resize(0);
}
-bool CycleGraph::checkForRMWViolation() const
-{
- return hasRMWViolation;
-}
-
/**
* @brief Constructor for a CycleNode
* @param act The ModelAction for this node
/**
* @brief Constructor for a CycleNode
* @param act The ModelAction for this node
~CycleGraph();
void addEdge(const ModelAction *from, const ModelAction *to);
bool checkForCycles() const;
~CycleGraph();
void addEdge(const ModelAction *from, const ModelAction *to);
bool checkForCycles() const;
- bool checkForRMWViolation() const;
void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
bool checkPromise(const ModelAction *from, Promise *p) const;
bool checkReachable(const ModelAction *from, const ModelAction *to) const;
void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
bool checkPromise(const ModelAction *from, Promise *p) const;
bool checkReachable(const ModelAction *from, const ModelAction *to) const;
bool hasCycles;
bool oldCycles;
bool hasCycles;
bool oldCycles;
- bool hasRMWViolation;
- bool oldRMWViolation;
-
std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > rollbackvector;
std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > rmwrollbackvector;
};
std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > rollbackvector;
std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > rmwrollbackvector;
};
{
char buf[100];
char *ptr = buf;
{
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)
if (mo_graph->checkForCycles())
ptr += sprintf(ptr, "[mo cycle]");
if (priv->failed_promise)
*/
bool ModelChecker::is_infeasible() const
{
*/
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 ||
priv->failed_promise ||
priv->too_many_reads ||
priv->bad_synchronization ||