ATOMIC_WAIT, // < A wait action
ATOMIC_TIMEDWAIT, // < A timed wait action
ATOMIC_ANNOTATION, // < An annotation action to pass information to a trace analysis
+ READY_FREE
} action_type_t;
thread_id_t get_tid() const { return tid; }
action_type get_type() const { return type; }
+ void set_free() { type = READY_FREE; }
memory_order get_mo() const { return order; }
memory_order get_original_mo() const { return original_order; }
void set_mo(memory_order order) { this->order = order; }
* @param action The ModelAction to find a node for
* @return The CycleNode paired with this action
*/
-CycleNode * CycleGraph::getNode(const ModelAction *action)
+CycleNode * CycleGraph::getNode(ModelAction *action)
{
CycleNode *node = getNode_noCreate(action);
if (node == NULL) {
* @param rmw The edge points to this ModelAction; this action must read from
* the ModelAction from
*/
-void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
+void CycleGraph::addRMWEdge(ModelAction *from, ModelAction *rmw)
{
ASSERT(from);
ASSERT(rmw);
addNodeEdge(fromnode, rmwnode, true);
}
-void CycleGraph::addEdges(SnapList<ModelAction *> * edgeset, const ModelAction *to) {
+void CycleGraph::addEdges(SnapList<ModelAction *> * edgeset, ModelAction *to) {
for(sllnode<ModelAction*> * it = edgeset->begin();it!=NULL;) {
ModelAction *act = it->getVal();
CycleNode *node = getNode(act);
* @return True, if new edge(s) are added; otherwise false
*/
-void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
+void CycleGraph::addEdge(ModelAction *from, ModelAction *to)
{
ASSERT(from);
ASSERT(to);
addNodeEdge(fromnode, tonode, false);
}
-void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to, bool forceedge)
+void CycleGraph::addEdge(ModelAction *from, ModelAction *to, bool forceedge)
{
ASSERT(from);
ASSERT(to);
* @brief Constructor for a CycleNode
* @param act The ModelAction for this node
*/
-CycleNode::CycleNode(const ModelAction *act) :
+CycleNode::CycleNode(ModelAction *act) :
action(act),
hasRMW(NULL),
cv(new ClockVector(NULL, act))
return edges.size();
}
+/**
+ * @param i The index of the edge to return
+ * @returns The CycleNode edge indexed by i
+ */
+CycleNode * CycleNode::getInEdge(unsigned int i) const
+{
+ return inedges[i];
+}
+
+/** @returns The number of edges leaving this CycleNode */
+unsigned int CycleNode::getNumInEdges() const
+{
+ return inedges.size();
+}
+
/**
* Adds an edge from this CycleNode to another CycleNode.
* @param node The node to which we add a directed edge
public:
CycleGraph();
~CycleGraph();
- void addEdges(SnapList<ModelAction *> * edgeset, const ModelAction *to);
- void addEdge(const ModelAction *from, const ModelAction *to);
- void addEdge(const ModelAction *from, const ModelAction *to, bool forceedge);
- void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
+ void addEdges(SnapList<ModelAction *> * edgeset, ModelAction *to);
+ void addEdge(ModelAction *from, ModelAction *to);
+ void addEdge(ModelAction *from, ModelAction *to, bool forceedge);
+ void addRMWEdge(ModelAction *from, ModelAction *rmw);
bool checkReachable(const ModelAction *from, const ModelAction *to) const;
void freeAction(const ModelAction * act);
#if SUPPORT_MOD_ORDER_DUMP
private:
void addNodeEdge(CycleNode *fromnode, CycleNode *tonode, bool forceedge);
void putNode(const ModelAction *act, CycleNode *node);
- CycleNode * getNode(const ModelAction *act);
+ CycleNode * getNode(ModelAction *act);
/** @brief A table for mapping ModelActions to CycleNodes */
HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
*/
class CycleNode {
public:
- CycleNode(const ModelAction *act);
+ CycleNode(ModelAction *act);
void addEdge(CycleNode *node);
CycleNode * getEdge(unsigned int i) const;
unsigned int getNumEdges() const;
+ CycleNode * getInEdge(unsigned int i) const;
+ unsigned int getNumInEdges() const;
bool setRMW(CycleNode *);
CycleNode * getRMW() const;
void clearRMW() { hasRMW = NULL; }
- const ModelAction * getAction() const { return action; }
+ ModelAction * getAction() const { return action; }
void removeInEdge(CycleNode *src);
~CycleNode();
SNAPSHOTALLOC
private:
/** @brief The ModelAction that this node represents */
- const ModelAction *action;
+ ModelAction *action;
/** @brief The edges leading out from this node */
SnapVector<CycleNode *> edges;
*/
bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
{
- SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
+ SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
if (hasnonatomicstore) {
ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
*/
bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
- SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
+ SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
if (!check_only)
priorset->push_back(act);
} else {
- const ModelAction *prevrf = act->get_reads_from();
+ ModelAction *prevrf = act->get_reads_from();
if (!prevrf->equals(rf)) {
if (mo_graph->checkReachable(rf, prevrf))
return false;
void ModelExecution::collectActions() {
//Compute minimal clock vector for all live threads
ClockVector *cvmin = computeMinimalCV();
-
+ SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
//walk action trace... When we hit an action ,see if it is
//invisible (e.g., earlier than the first before the minimum
//clock for the thread... if so erase it and all previous
//actions in cyclegraph
for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
ModelAction *act = it->getVal();
+ modelclock_t actseq = act->get_seq_number();
+ thread_id_t act_tid = act->get_tid();
+ modelclock_t tid_clock = cvmin->getClock(act_tid);
+ if (actseq <= tid_clock) {
+ ModelAction * write;
+ if (act->is_write()) {
+ write = act;
+ } else if (act->is_read()) {
+ write = act->get_reads_from();
+ } else
+ continue;
+ //Mark everything earlier in MO graph to be freed
+ queue->push_back(mo_graph->getNode_noCreate(write));
+ while(!queue->empty()) {
+ CycleNode * node = queue->back();
+ queue->pop_back();
+ for(unsigned int i=0;i<node->getNumInEdges();i++) {
+ CycleNode * prevnode = node->getInEdge(i);
+ ModelAction * prevact = prevnode->getAction();
+ if (prevact->get_type() != READY_FREE) {
+ prevact->set_free();
+ queue->push_back(prevnode);
+ }
+ }
+ }
+ }
}
-
delete cvmin;
+ delete queue;
}
+
+
Fuzzer * ModelExecution::getFuzzer() {
return fuzzer;
}
ModelAction * get_last_unlock(ModelAction *curr) const;
SnapVector<ModelAction *> * build_may_read_from(ModelAction *curr);
ModelAction * process_rmw(ModelAction *curr);
- bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset, bool *canprune, bool check_only = false);
+ bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<ModelAction *> *priorset, bool *canprune, bool check_only = false);
void w_modification_order(ModelAction *curr);
ClockVector * get_hb_from_write(ModelAction *rf) const;
ModelAction * convertNonAtomicStore(void*);