projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
c7f10b7
)
add comments
author
Brian Demsky
<bdemsky@uci.edu>
Tue, 25 Sep 2012 17:12:38 +0000
(10:12 -0700)
committer
Brian Demsky
<bdemsky@uci.edu>
Tue, 25 Sep 2012 17:12:38 +0000
(10:12 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 03a0c689431c90720ec56a1020ef21344920ac08..8a8007097da391e039128cdd1c5a850c229d0f59 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-1097,8
+1097,15
@@
bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
/** @todo Need to be smarter here... In the linux lock
* example, this will run to the beginning of the program for
* every acquire. */
/** @todo Need to be smarter here... In the linux lock
* example, this will run to the beginning of the program for
* every acquire. */
+ /** @todo The way to be smarter here is to keep going until 1
+ * thread has a release preceded by an acquire and you've seen
+ * both. */
+
if (rf->is_acquire() && rf->is_release())
return true; /* complete */
if (rf->is_acquire() && rf->is_release())
return true; /* complete */
+
+ /** @todo Might it be better to make this into a loop... */
+
return release_seq_head(rf->get_reads_from(), release_heads);
}
if (rf->is_release())
return release_seq_head(rf->get_reads_from(), release_heads);
}
if (rf->is_release())