#include "cyclegraph.h"
#include "action.h"
#include "common.h"
-#include "promise.h"
#include "threads-model.h"
/** Initializes a CycleGraph object. */
#endif
}
-/**
- * Add a CycleNode to the graph, corresponding to a Promise
- * @param promise The Promise that should be added
- * @param node The CycleNode that corresponds to the Promise
- */
-void CycleGraph::putNode(const Promise *promise, CycleNode *node)
-{
- promiseToNode.put(promise, node);
-#if SUPPORT_MOD_ORDER_DUMP
- nodeList.push_back(node);
-#endif
-}
-
-/**
- * @brief Remove the Promise node from the graph
- * @param promise The promise to remove from the graph
- */
-void CycleGraph::erasePromiseNode(const Promise *promise)
-{
- promiseToNode.put(promise, NULL);
-#if SUPPORT_MOD_ORDER_DUMP
- /* Remove the promise node from nodeList */
- CycleNode *node = getNode_noCreate(promise);
- for (unsigned int i = 0; i < nodeList.size(); )
- if (nodeList[i] == node)
- nodeList.erase(nodeList.begin() + i);
- else
- i++;
-#endif
-}
-
/** @return The corresponding CycleNode, if exists; otherwise NULL */
CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
{
return actionToNode.get(act);
}
-/** @return The corresponding CycleNode, if exists; otherwise NULL */
-CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const
-{
- return promiseToNode.get(promise);
-}
-
/**
* @brief Returns the CycleNode corresponding to a given ModelAction
*
return node;
}
-/**
- * @brief Returns a CycleNode corresponding to a promise
- *
- * Gets (or creates, if none exist) a CycleNode corresponding to a promised
- * value.
- *
- * @param promise The Promise generated by a reader
- * @return The CycleNode corresponding to the Promise
- */
-CycleNode * CycleGraph::getNode(const Promise *promise)
-{
- CycleNode *node = getNode_noCreate(promise);
- if (node == NULL) {
- node = new CycleNode(promise);
- putNode(promise, node);
- }
- return node;
-}
-
-/**
- * Resolve/satisfy a Promise with a particular store ModelAction, taking care
- * of the CycleGraph cleanups, including merging any necessary CycleNodes.
- *
- * @param promise The Promise to resolve
- * @param writer The store that will resolve this Promise
- * @return false if the resolution results in a cycle (or fails in some other
- * way); true otherwise
- */
-bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer)
-{
- CycleNode *promise_node = promiseToNode.get(promise);
- CycleNode *w_node = actionToNode.get(writer);
- ASSERT(promise_node);
-
- if (w_node)
- return mergeNodes(w_node, promise_node);
- /* No existing write-node; just convert the promise-node */
- promise_node->resolvePromise(writer);
- erasePromiseNode(promise_node->getPromise());
- putNode(writer, promise_node);
- return true;
-}
-
-/**
- * @brief Merge two CycleNodes that represent the same write
- *
- * Note that this operation cannot be rolled back.
- *
- * @param w_node The write ModelAction node with which to merge
- * @param p_node The Promise node to merge. Will be destroyed after this
- * function.
- *
- * @return false if the merge cannot succeed; true otherwise
- */
-bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node)
-{
- ASSERT(!w_node->is_promise());
- ASSERT(p_node->is_promise());
-
- const Promise *promise = p_node->getPromise();
- if (!promise->is_compatible(w_node->getAction()) ||
- !promise->same_value(w_node->getAction()))
- return false;
-
- /* Transfer the RMW */
- CycleNode *promise_rmw = p_node->getRMW();
- if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw))
- return false;
-
- /* Transfer back edges to w_node */
- while (p_node->getNumBackEdges() > 0) {
- CycleNode *back = p_node->removeBackEdge();
- if (back == w_node)
- continue;
- addNodeEdge(back, w_node);
- if (hasCycles)
- return false;
- }
-
- /* Transfer forward edges to w_node */
- while (p_node->getNumEdges() > 0) {
- CycleNode *forward = p_node->removeEdge();
- if (forward == w_node)
- continue;
- addNodeEdge(w_node, forward);
- if (hasCycles)
- return false;
- }
-
- erasePromiseNode(promise);
- /* Not deleting p_node, to maintain consistency if mergeNodes() fails */
-
- return !hasCycles;
-}
-
/**
* Adds an edge between two CycleNodes.
* @param fromnode The edge comes from this CycleNode
}
/* Instantiate two forms of CycleGraph::addRMWEdge */
template void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw);
-template void CycleGraph::addRMWEdge(const Promise *from, const ModelAction *rmw);
/**
* @brief Adds an edge between objects
}
/* Instantiate four forms of CycleGraph::addEdge */
template bool CycleGraph::addEdge(const ModelAction *from, const ModelAction *to);
-template bool CycleGraph::addEdge(const ModelAction *from, const Promise *to);
-template bool CycleGraph::addEdge(const Promise *from, const ModelAction *to);
-template bool CycleGraph::addEdge(const Promise *from, const Promise *to);
#if SUPPORT_MOD_ORDER_DUMP
static void print_node(FILE *file, const CycleNode *node, int label)
{
- if (node->is_promise()) {
- const Promise *promise = node->getPromise();
- int idx = promise->get_index();
- fprintf(file, "P%u", idx);
- if (label) {
- int first = 1;
- fprintf(file, " [label=\"P%d, T", idx);
- for (unsigned int i = 0 ; i < promise->max_available_thread_idx(); i++)
- if (promise->thread_is_available(int_to_id(i))) {
- fprintf(file, "%s%u", first ? "": ",", i);
- first = 0;
- }
- fprintf(file, "\"]");
- }
- } else {
const ModelAction *act = node->getAction();
modelclock_t idx = act->get_seq_number();
fprintf(file, "N%u", idx);
if (label)
fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid());
- }
}
static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, const char *prop)
print_edge(file, fromnode, tonode, prop);
}
/* Instantiate two forms of CycleGraph::dot_print_edge */
-template void CycleGraph::dot_print_edge(FILE *file, const Promise *from, const ModelAction *to, const char *prop);
template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, const ModelAction *to, const char *prop);
void CycleGraph::dumpNodes(FILE *file) const
/* Instantiate four forms of CycleGraph::checkReachable */
template bool CycleGraph::checkReachable(const ModelAction *from,
const ModelAction *to) const;
-template bool CycleGraph::checkReachable(const ModelAction *from,
- const Promise *to) const;
-template bool CycleGraph::checkReachable(const Promise *from,
- const ModelAction *to) const;
-template bool CycleGraph::checkReachable(const Promise *from,
- const Promise *to) const;
-
-/** @return True, if the promise has failed; false otherwise */
-bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
-{
- discovered->reset();
- queue->clear();
- CycleNode *from = actionToNode.get(fromact);
-
- queue->push_back(from);
- discovered->put(from, from);
- while (!queue->empty()) {
- const CycleNode *node = queue->back();
- queue->pop_back();
-
- if (node->getPromise() == promise)
- return true;
- if (!node->is_promise())
- promise->eliminate_thread(node->getAction()->get_tid());
-
- for (unsigned int i = 0; i < node->getNumEdges(); i++) {
- CycleNode *next = node->getEdge(i);
- if (!discovered->contains(next)) {
- discovered->put(next, next);
- queue->push_back(next);
- }
- }
- }
- return false;
-}
/** @brief Begin a new sequence of graph additions which can be rolled back */
void CycleGraph::startChanges()
*/
CycleNode::CycleNode(const ModelAction *act) :
action(act),
- promise(NULL),
- hasRMW(NULL)
-{
-}
-
-/**
- * @brief Constructor for a Promise CycleNode
- * @param promise The Promise which was generated
- */
-CycleNode::CycleNode(const Promise *promise) :
- action(NULL),
- promise(promise),
hasRMW(NULL)
{
}
hasRMW = node;
return false;
}
-
-/**
- * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be
- * used when there's no existing ModelAction CycleNode for this write.
- *
- * @param writer The ModelAction which wrote the future value represented by
- * this CycleNode
- */
-void CycleNode::resolvePromise(const ModelAction *writer)
-{
- ASSERT(is_promise());
- ASSERT(promise->is_compatible(writer));
- action = writer;
- promise = NULL;
- ASSERT(!is_promise());
-}
projects / c11tester.git / blobdiff