/** @brief Constructor */
ModelExecution::ModelExecution(ModelChecker *m,
- struct model_params *params,
+ const struct model_params *params,
Scheduler *scheduler,
NodeStack *node_stack) :
model(m),
model_thread = new Thread(get_next_id());
add_thread(model_thread);
scheduler->register_engine(this);
+ node_stack->register_engine(this);
}
/** @brief Destructor */
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
{
switch (act->get_type()) {
- /* case ATOMIC_FENCE: fences don't directly cause backtracking */
+ case ATOMIC_FENCE:
+ /* Only seq-cst fences can (directly) cause backtracking */
+ if (!act->is_seqcst())
+ break;
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
+ if (prev == act)
+ continue;
if (prev->could_synchronize_with(act)) {
ret = prev;
break;
*
* @param curr The current action to process
* @return The ModelAction that is actually executed; may be different than
- * curr; may be NULL, if the current action is not enabled to run
+ * curr
*/
ModelAction * ModelExecution::check_current_action(ModelAction *curr)
{
{
while (!pending_rel_seqs.empty() &&
is_feasible_prefix_ignore_relseq() &&
- !unrealizedraces.empty()) {
+ haveUnrealizedRaces()) {
model_print("*** WARNING: release sequence fixup action "
"(%zu pending release seuqence(s)) ***\n",
pending_rel_seqs.size());