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:
cf29a02
)
model: trivial - rename 'updated' -> 'update'
author
Brian Norris
<banorris@uci.edu>
Tue, 25 Sep 2012 23:50:59 +0000
(16:50 -0700)
committer
Brian Norris
<banorris@uci.edu>
Tue, 25 Sep 2012 23:52:54 +0000
(16:52 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index a9d94776cc3ec090d821caad3133441f2d2e2bcc..e7ab3bbed4298fb943e9704095ba3e0b58f109ab 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-617,20
+617,20
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
switch (work.type) {
case WORK_CHECK_CURR_ACTION: {
ModelAction *act = work.action;
switch (work.type) {
case WORK_CHECK_CURR_ACTION: {
ModelAction *act = work.action;
- bool update
d = false;
+ bool update
= false; /* update this location's release seq's */
process_thread_action(curr);
if (act->is_read() && process_read(act, second_part_of_rmw))
process_thread_action(curr);
if (act->is_read() && process_read(act, second_part_of_rmw))
- update
d
= true;
+ update = true;
if (act->is_write() && process_write(act))
if (act->is_write() && process_write(act))
- update
d
= true;
+ update = true;
if (act->is_mutex_op())
process_mutex(act);
if (act->is_mutex_op())
process_mutex(act);
- if (update
d
)
+ if (update)
work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
break;
}
work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
break;
}