From 7921811e8bd7bba2cdd892434a58ec7254ae0f99 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 10 Apr 2013 11:26:19 -0700 Subject: [PATCH] add some support for traceanalysis plugins --- model.cc | 15 +++++++++++++++ model.h | 5 ++++- traceanalysis.h | 9 +++++++++ 3 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 traceanalysis.h diff --git a/model.cc b/model.cc index 5941cf2..0f2f036 100644 --- a/model.cc +++ b/model.cc @@ -16,6 +16,7 @@ #include "datarace.h" #include "threads-model.h" #include "output.h" +#include "traceanalysis.h" #define INITIAL_THREAD_ID 0 @@ -92,6 +93,7 @@ ModelChecker::ModelChecker(struct model_params params) : thrd_last_action(new SnapVector(1)), thrd_last_fence_release(new SnapVector()), node_stack(new NodeStack()), + trace_analyses(new ModelVector()), priv(new struct model_snapshot_members()), mo_graph(new CycleGraph()) { @@ -121,6 +123,9 @@ ModelChecker::~ModelChecker() delete thrd_last_action; delete thrd_last_fence_release; delete node_stack; + for (unsigned int i = 0; i size();i++) + delete (*trace_analyses)[i]; + delete trace_analyses; delete scheduler; delete mo_graph; delete priv; @@ -553,6 +558,7 @@ bool ModelChecker::next_execution() assert_bug("Deadlock detected"); checkDataRaces(); + run_trace_analyses(); } record_stats(); @@ -578,6 +584,15 @@ bool ModelChecker::next_execution() 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 * diff --git a/model.h b/model.h index 8fdfc47..90c8a55 100644 --- a/model.h +++ b/model.h @@ -24,6 +24,7 @@ class Promise; class Scheduler; class Thread; class ClockVector; +class Trace_Analysis; struct model_snapshot_members; /** @brief Shorthand for a list of release sequence heads */ @@ -246,6 +247,8 @@ private: SnapVector * const thrd_last_action; SnapVector * const thrd_last_fence_release; NodeStack * const node_stack; + ModelVector * trace_analyses; + /** Private data members that should be snapshotted. They are grouped * together for efficiency and maintainability. */ @@ -274,7 +277,7 @@ private: /** @brief The cumulative execution stats */ struct execution_stats stats; void record_stats(); - + void run_trace_analyses(); void print_infeasibility(const char *prefix) const; bool is_feasible_prefix_ignore_relseq() const; bool is_infeasible() const; diff --git a/traceanalysis.h b/traceanalysis.h new file mode 100644 index 0000000..5c63cfd --- /dev/null +++ b/traceanalysis.h @@ -0,0 +1,9 @@ +#ifndef TRACE_ANALYSIS_H +#define TRACE_ANALYSIS_H +#include "model.h" + +class Trace_Analysis { + public: + virtual void analyze(action_list_t *); +}; +#endif -- 2.34.1