projects
/
c11tester.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model: rename 'reads_from' to 'rf'
[c11tester.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index bfb63e48ddd5d0d9ac0bc096b3604d3e6d9e640d..0c201fd381aa239eeaa060d6e46f22aae9023579 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-259,7
+259,7
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
/* The next node will try to satisfy a different set of promises. */
tid = next->get_tid();
node_stack->pop_restofstack(2);
/* The next node will try to satisfy a different set of promises. */
tid = next->get_tid();
node_stack->pop_restofstack(2);
- } else if (nextnode->increment_read_from()) {
+ } else if (nextnode->increment_read_from
_past
()) {
/* The next node will read from a different value. */
tid = next->get_tid();
node_stack->pop_restofstack(2);
/* The next node will read from a different value. */
tid = next->get_tid();
node_stack->pop_restofstack(2);
@@
-842,40
+842,36
@@
ModelAction * ModelChecker::get_next_backtrack()
}
/**
}
/**
- * Processes a read
or rmw
model action.
+ * Processes a read model action.
* @param curr is the read model action to process.
* @param curr is the read model action to process.
- * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
* @return True if processing this read updates the mo_graph.
*/
* @return True if processing this read updates the mo_graph.
*/
-bool ModelChecker::process_read(ModelAction *curr
, bool second_part_of_rmw
)
+bool ModelChecker::process_read(ModelAction *curr)
{
uint64_t value = VALUE_NONE;
bool updated = false;
while (true) {
{
uint64_t value = VALUE_NONE;
bool updated = false;
while (true) {
- const ModelAction *r
eads_from = curr->get_node()->get_read_from
();
- if (r
eads_from
!= NULL) {
+ const ModelAction *r
f = curr->get_node()->get_read_from_past
();
+ if (r
f
!= NULL) {
mo_graph->startChanges();
mo_graph->startChanges();
- value = reads_from->get_value();
- bool r_status = false;
+ value = rf->get_value();
- if (!second_part_of_rmw) {
- check_recency(curr, reads_from);
- r_status = r_modification_order(curr, reads_from);
- }
+ check_recency(curr, rf);
+ bool r_status = r_modification_order(curr, rf);
- if (
!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from
() || curr->get_node()->increment_future_value())) {
+ if (
is_infeasible() && (curr->get_node()->increment_read_from_past
() || curr->get_node()->increment_future_value())) {
mo_graph->rollbackChanges();
priv->too_many_reads = false;
continue;
}
mo_graph->rollbackChanges();
priv->too_many_reads = false;
continue;
}
- read_from(curr, r
eads_from
);
+ read_from(curr, r
f
);
mo_graph->commitChanges();
mo_check_promises(curr, true);
updated |= r_status;
mo_graph->commitChanges();
mo_check_promises(curr, true);
updated |= r_status;
- } else
if (!second_part_of_rmw)
{
+ } else {
/* Read from future value */
struct future_value fv = curr->get_node()->get_future_value();
Promise *promise = new Promise(curr, fv);
/* Read from future value */
struct future_value fv = curr->get_node()->get_future_value();
Promise *promise = new Promise(curr, fv);
@@
-1437,7
+1433,7
@@
ModelAction * ModelChecker::check_current_action(ModelAction *curr)
if (process_thread_action(curr))
update_all = true;
if (process_thread_action(curr))
update_all = true;
- if (act->is_read() &&
process_read(act, second_part_of_rmw
))
+ if (act->is_read() &&
!second_part_of_rmw && process_read(act
))
update = true;
if (act->is_write() && process_write(act))
update = true;
if (act->is_write() && process_write(act))
@@
-1505,7
+1501,7
@@
void ModelChecker::check_curr_backtracking(ModelAction *curr)
if ((parnode && !parnode->backtrack_empty()) ||
!currnode->misc_empty() ||
if ((parnode && !parnode->backtrack_empty()) ||
!currnode->misc_empty() ||
- !currnode->read_from_empty() ||
+ !currnode->read_from_
past_
empty() ||
!currnode->future_value_empty() ||
!currnode->promise_empty() ||
!currnode->relseq_break_empty()) {
!currnode->future_value_empty() ||
!currnode->promise_empty() ||
!currnode->relseq_break_empty()) {
@@
-1613,7
+1609,7
@@
ModelAction * ModelChecker::process_rmw(ModelAction *act) {
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
{
if (params.maxreads != 0) {
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
{
if (params.maxreads != 0) {
- if (curr->get_node()->get_read_from_size() <= 1)
+ if (curr->get_node()->get_read_from_
past_
size() <= 1)
return;
//Must make sure that execution is currently feasible... We could
//accidentally clear by rolling back
return;
//Must make sure that execution is currently feasible... We could
//accidentally clear by rolling back
@@
-1646,12
+1642,12
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
if (act->get_reads_from() != rf)
return;
if (act->get_reads_from() != rf)
return;
- if (act->get_node()->get_read_from_size() <= 1)
+ if (act->get_node()->get_read_from_
past_
size() <= 1)
return;
}
return;
}
- for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
+ for (int i = 0; i < curr->get_node()->get_read_from_
past_
size(); i++) {
/* Get write */
/* Get write */
- const ModelAction *write = curr->get_node()->get_read_from_
a
t(i);
+ const ModelAction *write = curr->get_node()->get_read_from_
pas
t(i);
/* Need a different write */
if (write == rf)
/* Need a different write */
if (write == rf)
@@
-1669,8
+1665,8
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
for (int loop = count; loop > 0; loop--, rit++) {
ModelAction *act = *rit;
bool foundvalue = false;
for (int loop = count; loop > 0; loop--, rit++) {
ModelAction *act = *rit;
bool foundvalue = false;
- for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
- if (act->get_node()->get_read_from_
a
t(j) == write) {
+ for (int j = 0; j < act->get_node()->get_read_from_
past_
size(); j++) {
+ if (act->get_node()->get_read_from_
pas
t(j) == write) {
foundvalue = true;
break;
}
foundvalue = true;
break;
}
@@
-1770,7
+1766,7
@@
bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
if (prevrf) {
if (!prevrf->equals(rf))
added = mo_graph->addEdge(prevrf, rf) || added;
if (prevrf) {
if (!prevrf->equals(rf))
added = mo_graph->addEdge(prevrf, rf) || added;
- } else if (!prevrf->equals(rf)) {
+ } else if (!prevrf
_promise
->equals(rf)) {
added = mo_graph->addEdge(prevrf_promise, rf) || added;
}
}
added = mo_graph->addEdge(prevrf_promise, rf) || added;
}
}
@@
-2635,7
+2631,7
@@
void ModelChecker::build_may_read_from(ModelAction *curr)
mo_graph->startChanges();
r_modification_order(curr, act);
if (!is_infeasible())
mo_graph->startChanges();
r_modification_order(curr, act);
if (!is_infeasible())
- curr->get_node()->add_read_from(act);
+ curr->get_node()->add_read_from
_past
(act);
mo_graph->rollbackChanges();
}
mo_graph->rollbackChanges();
}
@@
-2662,7
+2658,7
@@
void ModelChecker::build_may_read_from(ModelAction *curr)
}
/* We may find no valid may-read-from only if the execution is doomed */
}
/* We may find no valid may-read-from only if the execution is doomed */
- if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) {
+ if (!curr->get_node()->get_read_from_
past_
size() && curr->get_node()->future_value_empty()) {
priv->no_valid_reads = true;
set_assert();
}
priv->no_valid_reads = true;
set_assert();
}
@@
-2670,9
+2666,9
@@
void ModelChecker::build_may_read_from(ModelAction *curr)
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
curr->print();
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
curr->print();
- model_print("Printing
may_read_from
\n");
- curr->get_node()->print_
may_read_from
();
- model_print("End printing
may_read_from
\n");
+ model_print("Printing
read_from_past
\n");
+ curr->get_node()->print_
read_from_past
();
+ model_print("End printing
read_from_past
\n");
}
}
}
}