projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
promise: add const
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index cb78f030a3ff3d730d11e6748935797d0aee4d59..6739d2c85ee2ca51dd3963c471c811e12f0711b3 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-739,6
+739,9
@@
bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
value = fv.value;
curr->set_read_from_promise(promise);
promises->push_back(promise);
value = fv.value;
curr->set_read_from_promise(promise);
promises->push_back(promise);
+ mo_graph->startChanges();
+ updated = r_modification_order(curr, promise);
+ mo_graph->commitChanges();
}
get_thread(curr)->set_return_value(value);
return updated;
}
get_thread(curr)->set_return_value(value);
return updated;
@@
-1304,8
+1307,14
@@
ModelAction * ModelChecker::check_current_action(ModelAction *curr)
if (act->is_read()) {
const ModelAction *rf = act->get_reads_from();
if (act->is_read()) {
const ModelAction *rf = act->get_reads_from();
- if (rf != NULL && r_modification_order(act, rf))
- updated = true;
+ const Promise *promise = act->get_reads_from_promise();
+ if (rf) {
+ if (r_modification_order(act, rf))
+ updated = true;
+ } else if (promise) {
+ if (r_modification_order(act, promise))
+ updated = true;
+ }
}
if (act->is_write()) {
if (w_modification_order(act))
}
if (act->is_write()) {
if (w_modification_order(act))
@@
-1521,7
+1530,7
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
* read.
*
* Basic idea is the following: Go through each other thread and find
* read.
*
* Basic idea is the following: Go through each other thread and find
- * the last
est
action that happened before our read. Two cases:
+ * the last action that happened before our read. Two cases:
*
* (1) The action is a write => that write must either occur before
* the write we read from or be the write we read from.
*
* (1) The action is a write => that write must either occur before
* the write we read from or be the write we read from.
@@
-1530,10
+1539,11
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
* must occur before the write we read from or be the same write.
*
* @param curr The current action. Must be a read.
* must occur before the write we read from or be the same write.
*
* @param curr The current action. Must be a read.
- * @param rf The
action
that curr reads from. Must be a write.
+ * @param rf The
ModelAction or Promise
that curr reads from. Must be a write.
* @return True if modification order edges were added; false otherwise
*/
* @return True if modification order edges were added; false otherwise
*/
-bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
+template <typename rf_type>
+bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
{
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
{
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
@@
-1561,26
+1571,23
@@
bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (act->is_write() &&
act != rf
&& act != curr) {
+ if (act->is_write() &&
!act->equals(rf)
&& act != curr) {
/* C++, Section 29.3 statement 5 */
if (curr->is_seqcst() && last_sc_fence_thread_local &&
*act < *last_sc_fence_thread_local) {
/* C++, Section 29.3 statement 5 */
if (curr->is_seqcst() && last_sc_fence_thread_local &&
*act < *last_sc_fence_thread_local) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
/* C++, Section 29.3 statement 4 */
else if (act->is_seqcst() && last_sc_fence_local &&
*act < *last_sc_fence_local) {
break;
}
/* C++, Section 29.3 statement 4 */
else if (act->is_seqcst() && last_sc_fence_local &&
*act < *last_sc_fence_local) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
/* C++, Section 29.3 statement 6 */
else if (last_sc_fence_thread_before &&
*act < *last_sc_fence_thread_before) {
break;
}
/* C++, Section 29.3 statement 6 */
else if (last_sc_fence_thread_before &&
*act < *last_sc_fence_thread_before) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
}
break;
}
}
@@
-1591,9
+1598,8
@@
bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
*/
if (act->happens_before(curr) && act != curr) {
if (act->is_write()) {
*/
if (act->happens_before(curr) && act != curr) {
if (act->is_write()) {
- if (rf != act) {
- mo_graph->addEdge(act, rf);
- added = true;
+ if (!act->equals(rf)) {
+ added = mo_graph->addEdge(act, rf) || added;
}
} else {
const ModelAction *prevreadfrom = act->get_reads_from();
}
} else {
const ModelAction *prevreadfrom = act->get_reads_from();
@@
-1601,9
+1607,8
@@
bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
if (prevreadfrom == NULL)
continue;
if (prevreadfrom == NULL)
continue;
- if (rf != prevreadfrom) {
- mo_graph->addEdge(prevreadfrom, rf);
- added = true;
+ if (!prevreadfrom->equals(rf)) {
+ added = mo_graph->addEdge(prevreadfrom, rf) || added;
}
}
break;
}
}
break;
@@
-1712,8
+1717,7
@@
bool ModelChecker::w_modification_order(ModelAction *curr)
so we are initialized. */
ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
if (last_seq_cst != NULL) {
so we are initialized. */
ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
if (last_seq_cst != NULL) {
- mo_graph->addEdge(last_seq_cst, curr);
- added = true;
+ added = mo_graph->addEdge(last_seq_cst, curr) || added;
}
}
}
}
@@
-1756,8
+1760,7
@@
bool ModelChecker::w_modification_order(ModelAction *curr)
/* C++, Section 29.3 statement 7 */
if (last_sc_fence_thread_before && act->is_write() &&
*act < *last_sc_fence_thread_before) {
/* C++, Section 29.3 statement 7 */
if (last_sc_fence_thread_before && act->is_write() &&
*act < *last_sc_fence_thread_before) {
- mo_graph->addEdge(act, curr);
- added = true;
+ added = mo_graph->addEdge(act, curr) || added;
break;
}
break;
}
@@
-1773,14
+1776,13
@@
bool ModelChecker::w_modification_order(ModelAction *curr)
* readfrom(act) --mo--> act
*/
if (act->is_write())
* readfrom(act) --mo--> act
*/
if (act->is_write())
-
mo_graph->addEdge(act, curr)
;
+
added = mo_graph->addEdge(act, curr) || added
;
else if (act->is_read()) {
//if previous read accessed a null, just keep going
if (act->get_reads_from() == NULL)
continue;
else if (act->is_read()) {
//if previous read accessed a null, just keep going
if (act->get_reads_from() == NULL)
continue;
-
mo_graph->addEdge(act->get_reads_from(), curr)
;
+
added = mo_graph->addEdge(act->get_reads_from(), curr) || added
;
}
}
- added = true;
break;
} else if (act->is_read() && !act->could_synchronize_with(curr) &&
!act->same_thread(curr)) {
break;
} else if (act->is_read() && !act->could_synchronize_with(curr) &&
!act->same_thread(curr)) {