void ModelAction::create_cv(const ModelAction *parent)
{
- ASSERT(cv == NULL);
+ if (cv)
+ delete cv;
if (parent)
cv = new ClockVector(parent->cv, this);
void ModelAction::read_from(const ModelAction *act)
{
ASSERT(cv);
- if (act->is_release() && this->is_acquire()) {
+ if (act!=NULL && act->is_release() && this->is_acquire()) {
synchronized(act);
cv->merge(act->cv);
}
num_executions++;
- if (isfeasible() || DBG_ENABLED())
+ if (isfinalfeasible() || DBG_ENABLED())
print_summary();
if ((diverge = model->get_next_backtrack()) == NULL)
/* First restore type and order in case of RMW operation */
if (curr->is_rmwr())
tmp->copy_typeandorder(curr);
+
+ /* If we have diverged, we need to reset the clock vector. */
+ if (diverge==NULL) {
+ tmp->create_cv(get_parent_action(tmp->get_tid()));
+ }
+
delete curr;
curr = tmp;
} else {
return !cyclegraph->checkForCycles() && !failed_promise;
}
+/** Returns whether the current trace is feasible. */
+bool ModelChecker::isfinalfeasible() {
+ return isfeasible() && promises->size()==0;
+}
+
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
ModelAction * ModelChecker::process_rmw(ModelAction * act) {
int tid = id_to_int(act->get_tid());
=>
that read could potentially read from our write.
*/
-
if (act->get_node()->add_future_value(curr->get_value())&&
(!next_backtrack || *act > * next_backtrack))
next_backtrack = act;
/** Resolve promises. */
void ModelChecker::resolve_promises(ModelAction *write) {
- for(unsigned int i=0;i<promises->size();i++) {
- Promise * promise=(*promises)[i];
+ for(unsigned int i=0, promise_index=0;promise_index<promises->size(); i++) {
+ Promise * promise=(*promises)[promise_index];
if (write->get_node()->get_promise(i)) {
ModelAction * read=promise->get_action();
read->read_from(write);
r_modification_order(read, write);
- }
+ promises->erase(promises->begin()+promise_index);
+ } else
+ promise_index++;
}
}
scheduler->print();
- if (!isfeasible())
+ if (!isfinalfeasible())
printf("INFEASIBLE EXECUTION!\n");
print_list(action_trace);
printf("\n");