The output of check_recency is actually a boolean (failure => "too many
reads"), so make that explicit.
Also, rework a little more logic to make the structure a little more
obvious.
{
Node *node = curr->get_node();
uint64_t value = VALUE_NONE;
{
Node *node = curr->get_node();
uint64_t value = VALUE_NONE;
switch (node->get_read_from_status()) {
case READ_FROM_PAST: {
const ModelAction *rf = node->get_read_from_past();
ASSERT(rf);
mo_graph->startChanges();
switch (node->get_read_from_status()) {
case READ_FROM_PAST: {
const ModelAction *rf = node->get_read_from_past();
ASSERT(rf);
mo_graph->startChanges();
- value = rf->get_value();
- check_recency(curr, rf);
- bool r_status = r_modification_order(curr, rf);
+
+ ASSERT(!is_infeasible());
+ if (!check_recency(curr, rf))
+ priv->too_many_reads = true;
+ updated = r_modification_order(curr, rf);
if (is_infeasible() && node->increment_read_from()) {
mo_graph->rollbackChanges();
if (is_infeasible() && node->increment_read_from()) {
mo_graph->rollbackChanges();
+ value = rf->get_value();
read_from(curr, rf);
mo_graph->commitChanges();
mo_check_promises(curr, true);
read_from(curr, rf);
mo_graph->commitChanges();
mo_check_promises(curr, true);
break;
}
case READ_FROM_PROMISE: {
break;
}
case READ_FROM_PROMISE: {
* 3) that other write must have been in the reads_from set for maxreads times.
*
* If so, we decide that the execution is no longer feasible.
* 3) that other write must have been in the reads_from set for maxreads times.
*
* If so, we decide that the execution is no longer feasible.
+ *
+ * @param curr The current action. Must be a read.
+ * @param rf The store from which we might read.
+ * @return True if the read should succeed; false otherwise
-void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
+bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const
//NOTE: Next check is just optimization, not really necessary....
if (curr->get_node()->get_read_from_past_size() <= 1)
//NOTE: Next check is just optimization, not really necessary....
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 */
- if (is_infeasible())
- return;
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
int tid = id_to_int(curr->get_tid());
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
int tid = id_to_int(curr->get_tid());
/* See if we have enough reads from the same value */
for (int count = 0; count < params.maxreads; ritcopy++, count++) {
if (ritcopy == list->rend())
/* See if we have enough reads from the same value */
for (int count = 0; count < params.maxreads; ritcopy++, count++) {
if (ritcopy == list->rend())
ModelAction *act = *ritcopy;
if (!act->is_read())
ModelAction *act = *ritcopy;
if (!act->is_read())
if (act->get_reads_from() != rf)
if (act->get_reads_from() != rf)
if (act->get_node()->get_read_from_past_size() <= 1)
if (act->get_node()->get_read_from_past_size() <= 1)
}
for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
/* Get write */
}
for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
/* Get write */
- if (feasiblewrite) {
- priv->too_many_reads = true;
- return;
- }
+ if (feasiblewrite)
+ return false;
Thread * take_step(ModelAction *curr);
Thread * take_step(ModelAction *curr);
- void check_recency(ModelAction *curr, const ModelAction *rf);
+ bool check_recency(ModelAction *curr, const ModelAction *rf) const;
ModelAction * get_last_fence_conflict(ModelAction *act) const;
ModelAction * get_last_conflict(ModelAction *act) const;
void set_backtracking(ModelAction *act);
ModelAction * get_last_fence_conflict(ModelAction *act) const;
ModelAction * get_last_conflict(ModelAction *act) const;
void set_backtracking(ModelAction *act);