projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
ef1f3e3
)
cyclegraph: small cleanup
author
Brian Norris
<banorris@uci.edu>
Thu, 3 Jan 2013 22:00:37 +0000
(14:00 -0800)
committer
Brian Norris
<banorris@uci.edu>
Thu, 3 Jan 2013 22:32:46 +0000
(14:32 -0800)
cyclegraph.cc
patch
|
blob
|
history
cyclegraph.h
patch
|
blob
|
history
diff --git
a/cyclegraph.cc
b/cyclegraph.cc
index 2eaec3689d51b1b9f2f40b3eb48da182ec6d6bd7..edf582b318d05bc731fb1fee943589fbd373610e 100644
(file)
--- a/
cyclegraph.cc
+++ b/
cyclegraph.cc
@@
-135,12
+135,12
@@
void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
}
#if SUPPORT_MOD_ORDER_DUMP
}
#if SUPPORT_MOD_ORDER_DUMP
-void CycleGraph::dumpNodes(FILE *file)
+void CycleGraph::dumpNodes(FILE *file)
const
{
for (unsigned int i = 0; i < nodeList.size(); i++) {
CycleNode *cn = nodeList[i];
const ModelAction *action = cn->getAction();
{
for (unsigned int i = 0; i < nodeList.size(); i++) {
CycleNode *cn = nodeList[i];
const ModelAction *action = cn->getAction();
- fprintf(file, "N%u [label=\"%u, T%u\"];\n",
action->get_seq_number(),
action->get_seq_number(), action->get_tid());
+ fprintf(file, "N%u [label=\"%u, T%u\"];\n",
action->get_seq_number(),
action->get_seq_number(), action->get_tid());
if (cn->getRMW() != NULL) {
fprintf(file, "N%u -> N%u[style=dotted];\n", action->get_seq_number(), cn->getRMW()->getAction()->get_seq_number());
}
if (cn->getRMW() != NULL) {
fprintf(file, "N%u -> N%u[style=dotted];\n", action->get_seq_number(), cn->getRMW()->getAction()->get_seq_number());
}
@@
-152,7
+152,7
@@
void CycleGraph::dumpNodes(FILE *file)
}
}
}
}
-void CycleGraph::dumpGraphToFile(const char *filename)
+void CycleGraph::dumpGraphToFile(const char *filename)
const
{
char buffer[200];
sprintf(buffer, "%s.dot", filename);
{
char buffer[200];
sprintf(buffer, "%s.dot", filename);
@@
-170,7
+170,7
@@
void CycleGraph::dumpGraphToFile(const char *filename)
* @param to The ModelAction to reach
* @return True, @a from can reach @a to; otherwise, false
*/
* @param to The ModelAction to reach
* @return True, @a from can reach @a to; otherwise, false
*/
-bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to)
+bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to)
const
{
CycleNode *fromnode = actionToNode.get(from);
CycleNode *tonode = actionToNode.get(to);
{
CycleNode *fromnode = actionToNode.get(from);
CycleNode *tonode = actionToNode.get(to);
@@
-187,7
+187,7
@@
bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to)
* @param to The CycleNode to reach
* @return True, @a from can reach @a to; otherwise, false
*/
* @param to The CycleNode to reach
* @return True, @a from can reach @a to; otherwise, false
*/
-bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to)
+bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to)
const
{
std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
discovered->reset();
{
std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
discovered->reset();
@@
-211,7
+211,7
@@
bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to)
return false;
}
return false;
}
-bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise)
+bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise)
const
{
std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
discovered->reset();
{
std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
discovered->reset();
@@
-256,7
+256,8
@@
void CycleGraph::commitChanges()
}
/** Rollback changes to the previous commit. */
}
/** Rollback changes to the previous commit. */
-void CycleGraph::rollbackChanges() {
+void CycleGraph::rollbackChanges()
+{
for (unsigned int i = 0; i < rollbackvector.size(); i++) {
rollbackvector[i]->popEdge();
}
for (unsigned int i = 0; i < rollbackvector.size(); i++) {
rollbackvector[i]->popEdge();
}
@@
-272,20
+273,22
@@
void CycleGraph::rollbackChanges() {
}
/** @returns whether a CycleGraph contains cycles. */
}
/** @returns whether a CycleGraph contains cycles. */
-bool CycleGraph::checkForCycles() {
+bool CycleGraph::checkForCycles() const
+{
return hasCycles;
}
return hasCycles;
}
-bool CycleGraph::checkForRMWViolation() {
+bool CycleGraph::checkForRMWViolation() const
+{
return hasRMWViolation;
}
/**
return hasRMWViolation;
}
/**
- *
Constructor for a CycleNode.
- * @param
modelaction
The ModelAction for this node
+ *
@brief Constructor for a CycleNode
+ * @param
act
The ModelAction for this node
*/
*/
-CycleNode::CycleNode(const ModelAction *
modelaction
) :
- action(
modelaction
),
+CycleNode::CycleNode(const ModelAction *
act
) :
+ action(
act
),
hasRMW(NULL)
{
}
hasRMW(NULL)
{
}
diff --git
a/cyclegraph.h
b/cyclegraph.h
index 0a6f7382a69cf78dae9b4d2bf995864b599b3912..dcdeb3f217deced343e4ee227741040bfc733e1e 100644
(file)
--- a/
cyclegraph.h
+++ b/
cyclegraph.h
@@
-1,9
+1,13
@@
-/** @file cyclegraph.h @brief Data structure to track ordering
- * constraints on modification order. The idea is to see whether a
- * total order exists that satisfies the ordering constriants.*/
+/**
+ * @file cyclegraph.h
+ * @brief Data structure to track ordering constraints on modification order
+ *
+ * Used to determine whether a total order exists that satisfies the ordering
+ * constraints.
+ */
-#ifndef
CYCLEGRAPH_H
-#define
CYCLEGRAPH_H
+#ifndef
__CYCLEGRAPH_H__
+#define
__CYCLEGRAPH_H__
#include "hashtable.h"
#include <vector>
#include "hashtable.h"
#include <vector>
@@
-21,17
+25,17
@@
class CycleGraph {
CycleGraph();
~CycleGraph();
void addEdge(const ModelAction *from, const ModelAction *to);
CycleGraph();
~CycleGraph();
void addEdge(const ModelAction *from, const ModelAction *to);
- bool checkForCycles();
- bool checkForRMWViolation();
+ bool checkForCycles()
const
;
+ bool checkForRMWViolation()
const
;
void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
- bool checkPromise(const ModelAction *from, Promise *p);
- bool checkReachable(const ModelAction *from, const ModelAction *to);
+ bool checkPromise(const ModelAction *from, Promise *p)
const
;
+ bool checkReachable(const ModelAction *from, const ModelAction *to)
const
;
void startChanges();
void commitChanges();
void rollbackChanges();
#if SUPPORT_MOD_ORDER_DUMP
void startChanges();
void commitChanges();
void rollbackChanges();
#if SUPPORT_MOD_ORDER_DUMP
- void dumpNodes(FILE *file);
- void dumpGraphToFile(const char *filename);
+ void dumpNodes(FILE *file)
const
;
+ void dumpGraphToFile(const char *filename)
const
;
#endif
SNAPSHOTALLOC
#endif
SNAPSHOTALLOC
@@
-45,7
+49,7
@@
class CycleGraph {
std::vector<CycleNode *> nodeList;
#endif
std::vector<CycleNode *> nodeList;
#endif
- bool checkReachable(CycleNode *from, CycleNode *to);
+ bool checkReachable(CycleNode *from, CycleNode *to)
const
;
/** @brief A flag: true if this graph contains cycles */
bool hasCycles;
/** @brief A flag: true if this graph contains cycles */
bool hasCycles;
@@
-61,7
+65,7
@@
class CycleGraph {
/** @brief A node within a CycleGraph; corresponds to one ModelAction */
class CycleNode {
public:
/** @brief A node within a CycleGraph; corresponds to one ModelAction */
class CycleNode {
public:
- CycleNode(const ModelAction *act
ion
);
+ CycleNode(const ModelAction *act);
bool addEdge(CycleNode *node);
CycleNode * getEdge(unsigned int i) const;
unsigned int getNumEdges() const;
bool addEdge(CycleNode *node);
CycleNode * getEdge(unsigned int i) const;
unsigned int getNumEdges() const;
@@
-89,4
+93,4
@@
class CycleNode {
CycleNode *hasRMW;
};
CycleNode *hasRMW;
};
-#endif
+#endif
/* __CYCLEGRAPH_H__ */