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:
247e28f
)
rmw example works
author
Brian Demsky
<bdemsky@uci.edu>
Fri, 20 Jul 2012 19:42:42 +0000
(12:42 -0700)
committer
Brian Norris
<banorris@uci.edu>
Thu, 2 Aug 2012 17:12:46 +0000
(10:12 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 59f148ef0f6c4a7b316a970bb1024d9e6aa0ed9a..e18fda15248399cda859339296447ca2b35bd9f5 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-118,7
+118,6
@@
Thread * ModelChecker::schedule_next_thread()
*/
thread_id_t ModelChecker::get_next_replay_thread()
{
*/
thread_id_t ModelChecker::get_next_replay_thread()
{
- ModelAction *next;
thread_id_t tid;
/* Have we completed exploring the preselected path? */
thread_id_t tid;
/* Have we completed exploring the preselected path? */
@@
-126,7
+125,7
@@
thread_id_t ModelChecker::get_next_replay_thread()
return THREAD_ID_T_NONE;
/* Else, we are trying to replay an execution */
return THREAD_ID_T_NONE;
/* Else, we are trying to replay an execution */
- next = node_stack->get_next()->get_action();
+
ModelAction *
next = node_stack->get_next()->get_action();
if (next == diverge) {
Node *nextnode = next->get_node();
if (next == diverge) {
Node *nextnode = next->get_node();
@@
-308,17
+307,16
@@
void ModelChecker::check_current_action(void)
if (!already_added)
add_action_to_lists(curr);
if (!already_added)
add_action_to_lists(curr);
- /* Do not split atomic actions. */
- if (curr->is_rmwr()) {
- nextThread = thread_current()->get_id();
- return;
- }
-
/* Is there a better interface for setting the next thread rather
than this field/convoluted approach? Perhaps like just returning
it or something? */
/* Is there a better interface for setting the next thread rather
than this field/convoluted approach? Perhaps like just returning
it or something? */
- nextThread = get_next_replay_thread();
+ /* Do not split atomic actions. */
+ if (curr->is_rmwr()) {
+ nextThread = thread_current()->get_id();
+ } else {
+ nextThread = get_next_replay_thread();
+ }
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();