The build_reads_from_past calculation shouldn't be part of the action
initialization. It requires more information from the ModelChecker.
In the future, we will assume that all check_curren_action code (after
initialization) may include the current action in the model-checker lists. So
this also fixes up the build_reads_from_past code so that it skips the current
action.
* NodeStack
*/
curr->create_cv(get_parent_action(curr->get_tid()));
* NodeStack
*/
curr->create_cv(get_parent_action(curr->get_tid()));
- if (curr->is_read())
- build_reads_from_past(curr);
if (curr->is_write())
compute_promises(curr);
}
if (curr->is_write())
compute_promises(curr);
}
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
- curr = initialize_curr_action(curr);
+ ModelAction *newcurr = initialize_curr_action(curr);
+
+ /* Build may_read_from set for newly-created actions */
+ if (curr == newcurr && curr->is_read())
+ build_reads_from_past(curr);
+ curr = newcurr;
/* Thread specific actions */
switch (curr->get_type()) {
/* Thread specific actions */
switch (curr->get_type()) {
ModelAction *act = *rit;
/* Only consider 'write' actions */
ModelAction *act = *rit;
/* Only consider 'write' actions */
+ if (!act->is_write() || act == curr)
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */