From: Brian Demsky Date: Mon, 6 May 2013 09:50:49 +0000 (-0700) Subject: add traceanalysis support X-Git-Tag: oopsla2013~18 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=b090a4abc4915a9aa2a29787f76a6add79f838e2;hp=6a2d1dcdcff89e68d8a2fe9de1f38ecfac345caf add traceanalysis support --- diff --git a/Makefile b/Makefile index 26aadc9..acd281b 100644 --- a/Makefile +++ b/Makefile @@ -4,7 +4,7 @@ OBJECTS = libthreads.o schedule.o model.o threads.o librace.o action.o \ nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \ datarace.o impatomic.o cmodelint.o \ snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \ - context.o scanalysis.o execution.o + context.o scanalysis.o execution.o plugins.o CPPFLAGS += -Iinclude -I. LDFLAGS = -ldl -lrt -rdynamic diff --git a/main.cc b/main.cc index 0ca78b9..c8417c0 100644 --- a/main.cc +++ b/main.cc @@ -4,6 +4,7 @@ #include #include +#include #include "common.h" #include "output.h" @@ -15,6 +16,7 @@ #include "params.h" #include "snapshot-interface.h" #include "scanalysis.h" +#include "plugins.h" static void param_defaults(struct model_params *params) { @@ -23,7 +25,6 @@ static void param_defaults(struct model_params *params) params->fairwindow = 0; params->yieldon = false; params->yieldblock = false; - params->sc_trace_analysis = false; params->enabledcount = 1; params->bound = 0; params->maxfuturevalues = 0; @@ -77,7 +78,7 @@ static void print_usage(const char *program_name, struct model_params *params) "-u, --uninitialized=VALUE Return VALUE any load which may read from an\n" " uninitialized atomic.\n" " Default: %u\n" -"-c, --analysis Use SC Trace Analysis.\n" +"-t, --analysis=NAME Use Trace Analysis.\n" " -- Program arguments follow.\n\n", program_name, params->maxreads, @@ -93,9 +94,24 @@ static void print_usage(const char *program_name, struct model_params *params) exit(EXIT_SUCCESS); } +bool install_plugin(char * name) { + ModelVector * registeredanalysis=getRegisteredTraceAnalysis(); + ModelVector * installedanalysis=getInstalledTraceAnalysis(); + + for(unsigned int i=0;isize();i++) { + TraceAnalysis * analysis=(*registeredanalysis)[i]; + if (strcmp(name, analysis->name())==0) { + installedanalysis->push_back(analysis); + return false; + } + } + model_print("Analysis %s Not Found\n", name); + return true; +} + static void parse_options(struct model_params *params, int argc, char **argv) { - const char *shortopts = "hyYcm:M:s:S:f:e:b:u:v::"; + const char *shortopts = "hyYt:m:M:s:S:f:e:b:u:v::"; const struct option longopts[] = { {"help", no_argument, NULL, 'h'}, {"liveness", required_argument, NULL, 'm'}, @@ -109,7 +125,7 @@ static void parse_options(struct model_params *params, int argc, char **argv) {"bound", required_argument, NULL, 'b'}, {"verbose", optional_argument, NULL, 'v'}, {"uninitialized", optional_argument, NULL, 'u'}, - {"analysis", optional_argument, NULL, 'c'}, + {"analysis", optional_argument, NULL, 't'}, {0, 0, 0, 0} /* Terminator */ }; int opt, longindex; @@ -146,12 +162,13 @@ static void parse_options(struct model_params *params, int argc, char **argv) case 'u': params->uninitvalue = atoi(optarg); break; - case 'c': - params->sc_trace_analysis = true; - break; case 'y': params->yieldon = true; break; + case 't': + if (install_plugin(optarg)) + error = true; + break; case 'Y': params->yieldblock = true; break; @@ -178,10 +195,14 @@ static void parse_options(struct model_params *params, int argc, char **argv) int main_argc; char **main_argv; -static void install_trace_analyses(const ModelExecution *execution) +static void install_trace_analyses(ModelExecution *execution) { - if (model->params.sc_trace_analysis) - model->add_trace_analysis(new SCAnalysis(execution)); + ModelVector * installedanalysis=getInstalledTraceAnalysis(); + for(unsigned int i=0;isize();i++) { + TraceAnalysis * ta=(*installedanalysis)[i]; + ta->setExecution(execution); + model->add_trace_analysis(ta); + } } /** The model_main function contains the main model checking loop. */ @@ -190,6 +211,7 @@ static void model_main() struct model_params params; param_defaults(¶ms); + register_plugins(); parse_options(¶ms, main_argc, main_argv); diff --git a/model.h b/model.h index 77db6aa..25e20b1 100644 --- a/model.h +++ b/model.h @@ -50,7 +50,7 @@ public: /** @returns the context for the main model-checking system thread */ ucontext_t * get_system_context() { return &system_context; } - const ModelExecution * get_execution() const { return execution; } + ModelExecution * get_execution() const { return execution; } int get_execution_number() const { return execution_number; } diff --git a/params.h b/params.h index 043b2a5..0eda8bf 100644 --- a/params.h +++ b/params.h @@ -10,7 +10,6 @@ struct model_params { int maxfuturedelay; bool yieldon; bool yieldblock; - bool sc_trace_analysis; unsigned int fairwindow; unsigned int enabledcount; unsigned int bound; diff --git a/plugins.cc b/plugins.cc new file mode 100644 index 0000000..b1d3cfb --- /dev/null +++ b/plugins.cc @@ -0,0 +1,19 @@ +#include "plugins.h" +#include "scanalysis.h" + +ModelVector * registered_analysis; +ModelVector * installed_analysis; + +void register_plugins() { + registered_analysis=new ModelVector(); + installed_analysis=new ModelVector(); + registered_analysis->push_back(new SCAnalysis()); +} + +ModelVector * getRegisteredTraceAnalysis() { + return registered_analysis; +} + +ModelVector * getInstalledTraceAnalysis() { + return installed_analysis; +} diff --git a/plugins.h b/plugins.h new file mode 100644 index 0000000..ce0f529 --- /dev/null +++ b/plugins.h @@ -0,0 +1,10 @@ +#ifndef PLUGINS_H +#define PLUGINS_H +#include "traceanalysis.h" +#include "stl-model.h" + +void register_plugins(); +ModelVector * getRegisteredTraceAnalysis(); +ModelVector * getInstalledTraceAnalysis(); + +#endif diff --git a/scanalysis.cc b/scanalysis.cc index 98dd8eb..265c84c 100644 --- a/scanalysis.cc +++ b/scanalysis.cc @@ -4,19 +4,28 @@ #include "clockvector.h" #include "execution.h" -SCAnalysis::SCAnalysis(const ModelExecution *execution) : +SCAnalysis::SCAnalysis() : cvmap(), cyclic(false), badrfset(), lastwrmap(), threadlists(1), - execution(execution) + execution(NULL) { } SCAnalysis::~SCAnalysis() { } +void SCAnalysis::setExecution(ModelExecution * execution) { + this->execution=execution; +} + +char * SCAnalysis::name() { + char * name = "SC"; + return name; +} + void SCAnalysis::print_list(action_list_t *list) { model_print("---------------------------------------------------------------------\n"); if (cyclic) diff --git a/scanalysis.h b/scanalysis.h index 3b9fed3..ffa933a 100644 --- a/scanalysis.h +++ b/scanalysis.h @@ -5,9 +5,12 @@ class SCAnalysis : public TraceAnalysis { public: - SCAnalysis(const ModelExecution *execution); + SCAnalysis(); ~SCAnalysis(); + virtual void setExecution(ModelExecution * execution); virtual void analyze(action_list_t *); + virtual char * name(); + SNAPSHOTALLOC private: @@ -29,6 +32,6 @@ class SCAnalysis : public TraceAnalysis { HashTable badrfset; HashTable lastwrmap; SnapVector threadlists; - const ModelExecution *execution; + ModelExecution *execution; }; #endif diff --git a/traceanalysis.h b/traceanalysis.h index 8376bbc..43c6eba 100644 --- a/traceanalysis.h +++ b/traceanalysis.h @@ -4,7 +4,9 @@ class TraceAnalysis { public: + virtual void setExecution(ModelExecution * execution) = 0; virtual void analyze(action_list_t *) = 0; + virtual char * name() = 0; SNAPSHOTALLOC }; #endif