projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
0959253
)
lots of debugging here... finally working with my rmw example...
author
Brian Demsky
<bdemsky@uci.edu>
Thu, 13 Sep 2012 08:33:24 +0000
(
01:33
-0700)
committer
Brian Demsky
<bdemsky@uci.edu>
Thu, 13 Sep 2012 08:33:24 +0000
(
01:33
-0700)
cyclegraph.cc
patch
|
blob
|
history
model.cc
patch
|
blob
|
history
diff --git
a/cyclegraph.cc
b/cyclegraph.cc
index 62330624d6f08a233292ddfee1269380e8869beb..0a3d8858e795849f16ab1cae667b2e34bb1367cc 100644
(file)
--- a/
cyclegraph.cc
+++ b/
cyclegraph.cc
@@
-55,7
+55,11
@@
void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
//If the fromnode has a rmwnode that is not the tonode, we
//should add an edge between its rmwnode and the tonode
//If the fromnode has a rmwnode that is not the tonode, we
//should add an edge between its rmwnode and the tonode
- if (rmwnode!=NULL&&rmwnode!=tonode) {
+ //If tonode is also a rmw, don't do this check as the execution is
+ //doomed and we'll catch the problem elsewhere, but we want to allow
+ //for the possibility of sending to's write value to rmwnode
+
+ if (rmwnode!=NULL&&!to->is_rmw()) {
if (!hasCycles) {
// Check for Cycles
hasCycles=checkReachable(tonode, rmwnode);
if (!hasCycles) {
// Check for Cycles
hasCycles=checkReachable(tonode, rmwnode);
@@
-94,8
+98,10
@@
void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
std::vector<CycleNode *> * edges=fromnode->getEdges();
for(unsigned int i=0;i<edges->size();i++) {
CycleNode * tonode=(*edges)[i];
std::vector<CycleNode *> * edges=fromnode->getEdges();
for(unsigned int i=0;i<edges->size();i++) {
CycleNode * tonode=(*edges)[i];
- rollbackvector.push_back(rmwnode);
- rmwnode->addEdge(tonode);
+ if (tonode!=rmwnode) {
+ rollbackvector.push_back(rmwnode);
+ rmwnode->addEdge(tonode);
+ }
}
rollbackvector.push_back(fromnode);
}
rollbackvector.push_back(fromnode);
diff --git
a/model.cc
b/model.cc
index 795c4a99fea347b1d610c62df8172c55c447f91d..50317d07daa539d8f6643f16c3892c89aaddf60e 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-277,14
+277,15
@@
bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
mo_graph->startChanges();
value = reads_from->get_value();
mo_graph->startChanges();
value = reads_from->get_value();
+ bool r_status=false;
if (!second_part_of_rmw) {
check_recency(curr,false);
if (!second_part_of_rmw) {
check_recency(curr,false);
+ r_status=r_modification_order(curr, reads_from);
}
}
- bool r_status=r_modification_order(curr,reads_from);
- if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||
!curr->get_node()->future_value_empty
())) {
+ if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||
curr->get_node()->increment_future_value
())) {
mo_graph->rollbackChanges();
too_many_reads=false;
continue;
mo_graph->rollbackChanges();
too_many_reads=false;
continue;
@@
-611,16
+612,19
@@
bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr)) {
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr)) {
- if (act->is_read()) {
+ if (act->is_write()) {
+ if (rf != act && act != curr) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ } else {
const ModelAction *prevreadfrom = act->get_reads_from();
if (prevreadfrom != NULL && rf != prevreadfrom) {
mo_graph->addEdge(prevreadfrom, rf);
added = true;
}
const ModelAction *prevreadfrom = act->get_reads_from();
if (prevreadfrom != NULL && rf != prevreadfrom) {
mo_graph->addEdge(prevreadfrom, rf);
added = true;
}
- } else if (rf != act) {
- mo_graph->addEdge(act, rf);
- added = true;
- }
+ }
+
break;
}
}
break;
}
}