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:
92c453e
)
model: add todo synchronization comment
author
Brian Norris
<banorris@uci.edu>
Mon, 8 Oct 2012 06:24:21 +0000
(23:24 -0700)
committer
Brian Norris
<banorris@uci.edu>
Mon, 8 Oct 2012 06:24:53 +0000
(23:24 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index e23e9ec0a990b38e962b249f4d32c666f9885689..8267377faa791a2cfbc85f9027949c7338186635 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-576,6
+576,16
@@
void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
ASSERT(release->same_thread(rf));
if (write == NULL) {
ASSERT(release->same_thread(rf));
if (write == NULL) {
+ /**
+ * @todo Forcing a synchronization requires that we set
+ * modification order constraints. For instance, we can't allow
+ * a fixup sequence in which two separate read-acquire
+ * operations read from the same sequence, where the first one
+ * synchronizes and the other doesn't. Essentially, we can't
+ * allow any writes to insert themselves between 'release' and
+ * 'rf'
+ */
+
/* Must synchronize */
if (!acquire->synchronize_with(release)) {
set_bad_synchronization();
/* Must synchronize */
if (!acquire->synchronize_with(release)) {
set_bad_synchronization();