#include "datarace.h"
#include "threads-model.h"
#include "output.h"
+#include "traceanalysis.h"
#define INITIAL_THREAD_ID 0
thrd_last_action(new SnapVector<ModelAction *>(1)),
thrd_last_fence_release(new SnapVector<ModelAction *>()),
node_stack(new NodeStack()),
+ trace_analyses(new ModelVector<Trace_Analysis *>()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
{
delete thrd_last_action;
delete thrd_last_fence_release;
delete node_stack;
+ for (unsigned int i = 0; i <trace_analyses->size();i++)
+ delete (*trace_analyses)[i];
+ delete trace_analyses;
delete scheduler;
delete mo_graph;
delete priv;
assert_bug("Deadlock detected");
checkDataRaces();
+ run_trace_analyses();
}
record_stats();
return true;
}
+/**
+ * @brief Run trace analyses on complete trace. */
+
+void ModelChecker::run_trace_analyses() {
+ for(unsigned int i=0; i < trace_analyses->size(); i++) {
+ (*trace_analyses)[i]->analyze(action_trace);
+ }
+}
+
/**
* @brief Find the last fence-related backtracking conflict for a ModelAction
*
bool newly_explored = initialize_curr_action(&curr);
DBG();
- if (DBG_ENABLED())
- curr->print();
wake_up_sleeping_actions(curr);
}
/**
- * Updates the mo_graph with the constraints imposed from the current
+ * @brief Updates the mo_graph with the constraints imposed from the current
* read.
*
* Basic idea is the following: Go through each other thread and find
* the last action that happened before our read. Two cases:
*
- * (1) The action is a write => that write must either occur before
+ * -# The action is a write: that write must either occur before
* the write we read from or be the write we read from.
- *
- * (2) The action is a read => the write that that action read from
+ * -# The action is a read: the write that that action read from
* must occur before the write we read from or be the same write.
*
* @param curr The current action. Must be a read.
if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
switch_from_master(thr);
if (thr->is_waiting_on(thr))
- assert_bug("Deadlock detected");
+ assert_bug("Deadlock detected (thread %u)", i);
}
}