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 744fec5e17a27ef75b07a2bca068ff344e951ee8..e3d26d3261968ca4b4eefd3fd593767045b0687b 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-139,6
+139,9
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
+ if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+ earliest_diverge=diverge;
+
Node *nextnode = next->get_node();
/* Reached divergence point */
if (nextnode->increment_promise()) {
Node *nextnode = next->get_node();
/* Reached divergence point */
if (nextnode->increment_promise()) {
@@
-158,8
+161,12
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
Node *node = nextnode->get_parent();
tid = node->get_next_backtrack();
node_stack->pop_restofstack(1);
Node *node = nextnode->get_parent();
tid = node->get_next_backtrack();
node_stack->pop_restofstack(1);
+ if (diverge==earliest_diverge) {
+ earliest_diverge=node->get_action();
+ }
}
DEBUG("*** Divergence point ***\n");
}
DEBUG("*** Divergence point ***\n");
+
diverge = NULL;
} else {
tid = next->get_tid();
diverge = NULL;
} else {
tid = next->get_tid();
@@
-198,9
+205,6
@@
bool ModelChecker::next_execution()
if ((diverge = get_next_backtrack()) == NULL)
return false;
if ((diverge = get_next_backtrack()) == NULL)
return false;
- if (earliest_diverge == NULL || *diverge < *earliest_diverge)
- earliest_diverge=diverge;
-
if (DBG_ENABLED()) {
printf("Next execution will diverge at:\n");
diverge->print();
if (DBG_ENABLED()) {
printf("Next execution will diverge at:\n");
diverge->print();
@@
-471,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: {
@@
-487,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: {
@@
-497,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: {
@@
-507,7
+512,7
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
break;
}
break;
}
- return
synchroniz
ed;
+ return
updat
ed;
}
/**
}
/**