X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=main.cc;h=56eb311dd86f755d45989972d1fe165be74c60a2;hp=bff111f09dc28a99eff0ff2b70b4526141f39737;hb=a726f5f6e1e0731a0516be1e9e23397744734ef5;hpb=e60d8c23d30a0dfe66b8426f7f2ecf576e812028 diff --git a/main.cc b/main.cc index bff111f..56eb311 100644 --- a/main.cc +++ b/main.cc @@ -4,48 +4,75 @@ #include -#include "libthreads.h" #include "common.h" -#include "threads-model.h" +#include "output.h" #include "datarace.h" /* global "model" object */ #include "model.h" +#include "params.h" #include "snapshot-interface.h" +#include "scanalysis.h" -static void param_defaults(struct model_params * params) { +static void param_defaults(struct model_params *params) +{ params->maxreads = 0; - params->maxfuturedelay = 100; + params->maxfuturedelay = 6; params->fairwindow = 0; + params->yieldon = false; + params->sc_trace_analysis = false; params->enabledcount = 1; + params->bound = 0; + params->maxfuturevalues = 0; + params->expireslop = 4; + params->verbose = !!DBG_ENABLED(); + params->uninitvalue = 0; } -static void print_usage(struct model_params *params) { - printf( +static void print_usage(struct model_params *params) +{ + /* Reset defaults before printing */ + param_defaults(params); + + model_print( +"Copyright (c) 2013 Regents of the University of California. All rights reserved.\n" +"Distributed under the GPLv2\n" +"Written by Brian Norris and Brian Demsky\n" +"\n" "Usage: [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n" "\n" "Options:\n" "-h Display this help message and exit\n" "-m Maximum times a thread can read from the same write\n" " while other writes exist. Default: %d\n" +"-M Maximum number of future values that can be sent to\n" +" the same read. Default: %d\n" "-s Maximum actions that the model checker will wait for\n" " a write from the future past the expected number of\n" " actions. Default: %d\n" +"-S Future value expiration sloppiness. Default: %u\n" "-f Specify a fairness window in which actions that are\n" " enabled sufficiently many times should receive\n" " priority for execution. Default: %d\n" +"-y Turn on CHESS yield-based fairness support.\n" +" Default: %d\n" "-e Enabled count. Default: %d\n" +"-b Upper length bound. Default: %d\n" +"-v Print verbose execution information.\n" +"-u Value for uninitialized reads. Default: %u\n" +"-c Use SC Trace Analysis.\n" "-- Program arguments follow.\n\n", -params->maxreads, params->maxfuturedelay, params->fairwindow, params->enabledcount); +params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->enabledcount, params->bound, params->uninitvalue); exit(EXIT_SUCCESS); } -static void parse_options(struct model_params *params, int *argc, char ***argv) { - const char *shortopts = "hm:s:f:e:"; +static void parse_options(struct model_params *params, int argc, char **argv) +{ + const char *shortopts = "hycm:M:s:S:f:e:b:u:v"; int opt; bool error = false; - while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) { + while (!error && (opt = getopt(argc, argv, shortopts)) != -1) { switch (opt) { case 'h': print_usage(params); @@ -53,22 +80,51 @@ static void parse_options(struct model_params *params, int *argc, char ***argv) case 's': params->maxfuturedelay = atoi(optarg); break; + case 'S': + params->expireslop = atoi(optarg); + break; case 'f': params->fairwindow = atoi(optarg); break; case 'e': params->enabledcount = atoi(optarg); break; + case 'b': + params->bound = atoi(optarg); + break; case 'm': params->maxreads = atoi(optarg); break; + case 'M': + params->maxfuturevalues = atoi(optarg); + break; + case 'v': + params->verbose = 1; + break; + case 'u': + params->uninitvalue = atoi(optarg); + break; + case 'c': + params->sc_trace_analysis = true; + break; + case 'y': + params->yieldon = true; + break; default: /* '?' */ error = true; break; } } - (*argc) -= optind; - (*argv) += optind; + + /* Pass remaining arguments to user program */ + params->argc = argc - (optind - 1); + params->argv = argv + (optind - 1); + + /* Reset program name */ + params->argv[0] = argv[0]; + + /* Reset (global) optind for potential use by user program */ + optind = 1; if (error) print_usage(params); @@ -77,38 +133,31 @@ static void parse_options(struct model_params *params, int *argc, char ***argv) int main_argc; char **main_argv; -/** Wrapper to run the user's main function, with appropriate arguments */ -void wrapper_user_main(void *) +static void install_trace_analyses(const ModelExecution *execution) { - user_main(main_argc, main_argv); + if (model->params.sc_trace_analysis) + model->add_trace_analysis(new SCAnalysis(execution)); } /** The model_main function contains the main model checking loop. */ -static void model_main() { - thrd_t user_thread; +static void model_main() +{ struct model_params params; param_defaults(¶ms); - parse_options(¶ms, &main_argc, &main_argv); + parse_options(¶ms, main_argc, main_argv); //Initialize race detector initRaceDetector(); - //Create the singleton SnapshotStack object - snapshotObject = new SnapshotStack(); + snapshot_stack_init(); model = new ModelChecker(params); + install_trace_analyses(model->get_execution()); - snapshotObject->snapshotStep(0); - do { - /* Start user program */ - model->add_thread(new Thread(&user_thread, &wrapper_user_main, NULL)); - - /* Wait for all threads to complete */ - model->finish_execution(); - } while (model->next_execution()); - + snapshot_record(0); + model->run(); delete model; DEBUG("Exiting\n"); @@ -118,10 +167,14 @@ static void model_main() { * Main function. Just initializes snapshotting library and the * snapshotting library calls the model_main function. */ -int main(int argc, char ** argv) { +int main(int argc, char **argv) +{ main_argc = argc; main_argv = argv; + /* Configure output redirection for the model-checker */ + redirect_output(); + /* Let's jump in quickly and start running stuff */ - initSnapshotLibrary(10000, 1024, 1024, 4000, &model_main); + snapshot_system_init(10000, 1024, 1024, 4000, &model_main); }