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:
de3a958
)
model: some bug fixes to the model checker
author
Brian Demsky
<bdemsky@uci.edu>
Sun, 9 Sep 2012 09:25:47 +0000
(
02:25
-0700)
committer
Brian Norris
<banorris@uci.edu>
Tue, 11 Sep 2012 19:36:48 +0000
(12:36 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 36435d944cc028fa2bd5f8357d3e26407c5b712c..b5a29dd5ff16d6f430c5e6771bbc5c495e8c47d5 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-259,13
+259,13
@@
ModelAction * ModelChecker::get_next_backtrack()
*/
Thread * ModelChecker::check_current_action(ModelAction *curr)
{
*/
Thread * ModelChecker::check_current_action(ModelAction *curr)
{
- bool
already_added
= false;
+ bool
second_part_of_rmw
= false;
ASSERT(curr);
if (curr->is_rmwc() || curr->is_rmw()) {
ModelAction *tmp = process_rmw(curr);
ASSERT(curr);
if (curr->is_rmwc() || curr->is_rmw()) {
ModelAction *tmp = process_rmw(curr);
-
already_added
= true;
+
second_part_of_rmw
= true;
delete curr;
curr = tmp;
} else {
delete curr;
curr = tmp;
} else {
@@
-330,12
+330,12
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
value = reads_from->get_value();
/* Assign reads_from, perform release/acquire synchronization */
curr->read_from(reads_from);
value = reads_from->get_value();
/* Assign reads_from, perform release/acquire synchronization */
curr->read_from(reads_from);
- if (!
already_added
)
+ if (!
second_part_of_rmw
)
check_recency(curr,false);
bool r_status=r_modification_order(curr,reads_from);
check_recency(curr,false);
bool r_status=r_modification_order(curr,reads_from);
- if (!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
+ if (!
second_part_of_rmw&&!
isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
mo_graph->rollbackChanges();
too_many_reads=false;
continue;
mo_graph->rollbackChanges();
too_many_reads=false;
continue;
@@
-366,7
+366,7
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
th->set_return_value(value);
/* Add action to list. */
th->set_return_value(value);
/* Add action to list. */
- if (!
already_added
)
+ if (!
second_part_of_rmw
)
add_action_to_lists(curr);
Node *currnode = curr->get_node();
add_action_to_lists(curr);
Node *currnode = curr->get_node();