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:
ca6361d
)
model: THREAD_JOIN synchronizes with THREAD_FINISH
author
Brian Norris
<banorris@uci.edu>
Wed, 19 Sep 2012 01:45:17 +0000
(18:45 -0700)
committer
Brian Norris
<banorris@uci.edu>
Wed, 19 Sep 2012 01:45:17 +0000
(18:45 -0700)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index e41bc4e926f39c42487fd833bfd7e6c57d8a0baf..2b295dea1b24d631ce2a0da7942aeed734c8fc46 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-423,6
+423,8
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
if (!blocking->is_complete()) {
blocking->push_wait_list(curr);
scheduler->sleep(waiting);
if (!blocking->is_complete()) {
blocking->push_wait_list(curr);
scheduler->sleep(waiting);
+ } else {
+ do_complete_join(curr);
}
break;
}
}
break;
}
@@
-432,6
+434,7
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
ModelAction *act = th->pop_wait_list();
Thread *wake = get_thread(act);
scheduler->wake(wake);
ModelAction *act = th->pop_wait_list();
Thread *wake = get_thread(act);
scheduler->wake(wake);
+ do_complete_join(act);
}
th->complete();
break;
}
th->complete();
break;
@@
-498,6
+501,19
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
return get_next_thread(curr);
}
return get_next_thread(curr);
}
+/**
+ * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
+ * operation from the Thread it is joining with. Must be called after the
+ * completion of the Thread in question.
+ * @param join The THREAD_JOIN action
+ */
+void ModelChecker::do_complete_join(ModelAction *join)
+{
+ Thread *blocking = (Thread *)join->get_location();
+ ModelAction *act = get_last_action(blocking->get_id());
+ join->synchronize_with(act);
+}
+
void ModelChecker::check_curr_backtracking(ModelAction * curr) {
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
void ModelChecker::check_curr_backtracking(ModelAction * curr) {
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
diff --git
a/model.h
b/model.h
index b8a485931882f119ff5b70140c63f213fb79658f..b2b312f890328e5606887e73a62018eced76ba87 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-139,6
+139,7
@@
private:
bool release_seq_head(const ModelAction *rf,
std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
bool release_seq_head(const ModelAction *rf,
std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
+ void do_complete_join(ModelAction *join);
ModelAction *diverge;
ModelAction *diverge;