return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == NONATOMIC_WRITE;
}
+bool ModelAction::is_create() const
+{
+ return type == THREAD_CREATE || type == PTHREAD_CREATE;
+}
+
bool ModelAction::is_free() const
{
return type == READY_FREE;
bool is_trylock() const;
bool is_unlock() const;
bool is_wait() const;
+ bool is_create() const;
bool is_notify() const;
bool is_notify_one() const;
bool is_success_lock() const;
CycleNode *dst = cn->edges[i];
dst->removeInEdge(cn);
}
+ for(unsigned int i=0;i<cn->inedges.size();i++) {
+ CycleNode *src = cn->inedges[i];
+ src->removeEdge(cn);
+ }
delete cn;
}
}
}
+void CycleNode::removeEdge(CycleNode *dst) {
+ for(unsigned int i=0;i < edges.size();i++) {
+ if (edges[i] == dst) {
+ edges[i] = edges[edges.size()-1];
+ edges.pop_back();
+ break;
+ }
+ }
+}
+
/**
* @param i The index of the edge to return
* @returns The CycleNode edge indexed by i
void clearRMW() { hasRMW = NULL; }
ModelAction * getAction() const { return action; }
void removeInEdge(CycleNode *src);
+ void removeEdge(CycleNode *dst);
~CycleNode();
SNAPSHOTALLOC
thrd_last_fence_release(),
priv(new struct model_snapshot_members ()),
mo_graph(new CycleGraph()),
- fuzzer(new NewFuzzer()),
+ fuzzer(new Fuzzer()),
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
removeAction(act);
delete act;
}
+ } else if (act->is_create()) {
+ if (act->get_thread_operand()->get_state()==THREAD_COMPLETED) {
+ removeAction(act);
+ delete act;
+ }
} else {
removeAction(act);
delete act;