projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
d70f6f2
)
model: add PendingFutureValue constructor
author
Brian Norris
<banorris@uci.edu>
Tue, 8 Jan 2013 01:38:25 +0000
(17:38 -0800)
committer
Brian Norris
<banorris@uci.edu>
Tue, 8 Jan 2013 02:00:12 +0000
(18:00 -0800)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 98df8f316106a5f4cce404f4cada60ee35c5898a..bc17a882c56f38c7bab1a71064f584ca285e6171 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-871,7
+871,7
@@
bool ModelChecker::process_write(ModelAction *curr)
pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
set_latest_backtrack(pfv.act);
}
pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
set_latest_backtrack(pfv.act);
}
- futurevalues->
resize(0
);
+ futurevalues->
clear(
);
}
mo_graph->commitChanges();
}
mo_graph->commitChanges();
@@
-1773,8
+1773,7
@@
bool ModelChecker::w_modification_order(ModelAction *curr)
if (thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible() ||
(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
if (thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible() ||
(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
- struct PendingFutureValue pfv = {curr, act};
- futurevalues->push_back(pfv);
+ futurevalues->push_back(PendingFutureValue(curr, act));
}
}
}
}
}
}
diff --git
a/model.h
b/model.h
index c97cbf1a05f905fb79087c21b91401548b5ecf2e..414cf9337c4ba638198688a8586e4eb6681fb953 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-67,7
+67,8
@@
struct execution_stats {
};
struct PendingFutureValue {
};
struct PendingFutureValue {
- ModelAction *writer;
+ PendingFutureValue(ModelAction *writer, ModelAction *act) : writer(writer), act(act) { }
+ const ModelAction *writer;
ModelAction *act;
};
ModelAction *act;
};