projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model: THREAD_FINISH triggers release sequence check
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index 4f600a91f5eab4bb65420974e78651f0e53cfcfb..e3d26d3261968ca4b4eefd3fd593767045b0687b 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-475,11
+475,11
@@
bool ModelChecker::process_write(ModelAction *curr)
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated
or a thread completed
*/
bool ModelChecker::process_thread_action(ModelAction *curr)
{
*/
bool ModelChecker::process_thread_action(ModelAction *curr)
{
- bool
synchroniz
ed = false;
+ bool
updat
ed = false;
switch (curr->get_type()) {
case THREAD_CREATE: {
switch (curr->get_type()) {
case THREAD_CREATE: {
@@
-491,7
+491,7
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
Thread *blocking = (Thread *)curr->get_location();
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
Thread *blocking = (Thread *)curr->get_location();
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
- synchronized = true;
+ updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_FINISH: {
break;
}
case THREAD_FINISH: {
@@
-501,6
+501,7
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
scheduler->wake(get_thread(act));
}
th->complete();
scheduler->wake(get_thread(act));
}
th->complete();
+ updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
break;
}
case THREAD_START: {
@@
-511,7
+512,7
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
break;
}
break;
}
- return
synchroniz
ed;
+ return
updat
ed;
}
/**
}
/**