From: Brian Norris Date: Wed, 29 May 2013 02:03:14 +0000 (-0700) Subject: Merge remote-tracking branch 'origin/master' X-Git-Tag: oopsla2013~7 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=f2325500e8d1264ea811d5e68419b28d154b54ca;hp=93221839adb57ec10dd80f42be3963732cd2e236 Merge remote-tracking branch 'origin/master' --- diff --git a/README b/README index dcabe6f..93d9723 100644 --- a/README +++ b/README @@ -1,11 +1,21 @@ **************************************** -CDSChecker Readme + CDSChecker Readme **************************************** Copyright (c) 2013 Regents of the University of California. All rights reserved. CDSChecker is distributed under the GPL v2. +This README is divided into sections as follows: + + I. Overview + II. Reading an execution trace + A. References + +---------------------------------------- + I. Overview +---------------------------------------- + CDSChecker compiles as a dynamically-linked shared library by simply running 'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM (clang/clang++) and GCC. @@ -70,7 +80,9 @@ Model-checker options: -u, --uninitialized=VALUE Return VALUE any load which may read from an uninitialized atomic. Default: 0 --c, --analysis Use SC Trace Analysis. +-t, --analysis=NAME Use Analysis Plugin. +-o, --options=NAME Option for previous analysis plugin. + -o help for a list of options -- Program arguments follow. @@ -82,3 +94,98 @@ you can build and run the benchmarks as follows: make ./run.sh barrier/barrier -y -m 2 # runs barrier test with fairness/memory liveness ./bench.sh # run all benchmarks twice, with timing results + + +---------------------------------------- + II. Reading an execution trace +---------------------------------------- + +When CDSChecker detects a bug in your program (or when run with the --verbose +flag), it prints the output of the program run (STDOUT) along with some summary +trace information. The trace is given as a sequence of lines, where each line +represents an operation in the execution trace. These lines are ordered by the +order in which they were run by CDSChecker (i.e., the "execution order"), which +does not necessarily align with the "order" of the values observed (i.e., the +modification order and the reads-from relation). + +Columns: + + o #: The sequence number within the execution. That is, sequence number "9" + means the operation was the 9th operation executed by CDSChecker. Note that + this represents the execution order, not necessarily any other order (e.g., + modification order or reads-from). + + o t: The thread number + + o Action type: The type of operation performed + + o MO: The memory-order for this operation (i.e., memory_order_XXX, where XXX is + relaxed, release, acquire, rel_acq, or seq_cst) + + o Location: The memory location on which this operation is operating. This is + well-defined for atomic write/read/RMW, but other operations are subject to + CDSChecker implementation details. + + o Value: For reads/writes/RMW, the value returned by the operation. Note that + for RMW, this is the value that is *read*, not the value that was *written*. + For other operations, 'value' may have some CDSChecker-internal meaning. + + o Rf: For reads, the sequence number of the operation from which it reads. + [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE), + as printed during --verbose execution, reads may not be resolved and so may + have Rf=? or Rf=Px, where x is a promised future value.] + + o CV: The clock vector, encapsulating the happens-before relation (see our + paper, or the C/C++ memory model itself). We use a Lamport-style clock vector + similar to [1]. The "clock" is just the sequence number (#). The clock vector + can be read as follows: + + Each entry is indexed as CV[i], where + + i = 0, 1, 2, ..., + + So for any thread i, we say CV[i] is the sequence number of the most recent + operation in thread i such that operation i happens-before this operation. + Notably, thread 0 is reserved as a dummy thread for certain CDSChecker + operations. + +See the following example trace: + +------------------------------------------------------------------------------------ +# t Action type MO Location Value Rf CV +------------------------------------------------------------------------------------ +1 1 thread start seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 1) +2 1 init atomic relaxed 0x601068 0 ( 0, 2) +3 1 init atomic relaxed 0x60106c 0 ( 0, 3) +4 1 thread create seq_cst 0x7f68fe51c710 0x7f68fe51c6e0 ( 0, 4) +5 2 thread start seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 5) +6 2 atomic read relaxed 0x60106c 0 3 ( 0, 4, 6) +7 1 thread create seq_cst 0x7f68fe51c720 0x7f68fe51c6e0 ( 0, 7) +8 3 thread start seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 8) +9 2 atomic write relaxed 0x601068 0 ( 0, 4, 9) +10 3 atomic read relaxed 0x601068 0 2 ( 0, 7, 0, 10) +11 2 thread finish seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 11) +12 3 atomic write relaxed 0x60106c 0x2a ( 0, 7, 0, 12) +13 1 thread join seq_cst 0x7f68ff11ebc0 0x2 ( 0, 13, 11) +14 3 thread finish seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 14) +15 1 thread join seq_cst 0x7f68ff11efc0 0x3 ( 0, 15, 11, 14) +16 1 thread finish seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 16, 11, 14) +HASH 4073708854 +------------------------------------------------------------------------------------ + +Now consider, for example, operation 10: + +This is the 10th operation in the execution order. It is an atomic read-relaxed +operation performed by thread 3 at memory address 0x601068. It reads the value +"0", which was written by the 2nd operation in the execution order. Its clock +vector consists of the following values: + + CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10 + + +---------------------------------------- + A. References +---------------------------------------- + +[1] L. Lamport. Time, clocks, and the ordering of events in a distributed + system. CACM, 21(7):558–565, July 1978. diff --git a/action.cc b/action.cc index 14ad71d..3d38e81 100644 --- a/action.cc +++ b/action.cc @@ -569,25 +569,25 @@ void ModelAction::print() const { const char *type_str = get_type_str(), *mo_str = get_mo_str(); - model_print("(%4d) Thread: %-2d Action: %-13s MO: %7s Loc: %14p Value: %-#18" PRIx64, + model_print("%-4d %-2d %-13s %7s %14p %-#18" PRIx64, seq_number, id_to_int(tid), type_str, mo_str, location, get_return_value()); if (is_read()) { if (reads_from) - model_print(" Rf: %-3d", reads_from->get_seq_number()); + model_print(" %-3d", reads_from->get_seq_number()); else if (reads_from_promise) { int idx = reads_from_promise->get_index(); if (idx >= 0) - model_print(" Rf: P%-2d", idx); + model_print(" P%-2d", idx); else - model_print(" Rf: P? "); + model_print(" P? "); } else - model_print(" Rf: ? "); + model_print(" ? "); } if (cv) { if (is_read()) model_print(" "); else - model_print(" "); + model_print(" "); cv->print(); } else model_print("\n"); diff --git a/clockvector.cc b/clockvector.cc index 0b32528..5f068e9 100644 --- a/clockvector.cc +++ b/clockvector.cc @@ -95,7 +95,7 @@ modelclock_t ClockVector::getClock(thread_id_t thread) { void ClockVector::print() const { int i; - model_print("CV: ("); + model_print("("); for (i = 0; i < num_threads; i++) model_print("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", "); } diff --git a/execution.cc b/execution.cc index 4496b9c..403d70f 100644 --- a/execution.cc +++ b/execution.cc @@ -2630,7 +2630,9 @@ static void print_list(const action_list_t *list) { action_list_t::const_iterator it; - model_print("---------------------------------------------------------------------\n"); + model_print("------------------------------------------------------------------------------------\n"); + model_print("# t Action type MO Location Value Rf CV\n"); + model_print("------------------------------------------------------------------------------------\n"); unsigned int hash = 0; @@ -2641,7 +2643,7 @@ static void print_list(const action_list_t *list) hash = hash^(hash<<3)^((*it)->hash()); } model_print("HASH %u\n", hash); - model_print("---------------------------------------------------------------------\n"); + model_print("------------------------------------------------------------------------------------\n"); } #if SUPPORT_MOD_ORDER_DUMP diff --git a/main.cc b/main.cc index 1245b60..32c153d 100644 --- a/main.cc +++ b/main.cc @@ -94,7 +94,7 @@ static void print_usage(const char *program_name, struct model_params *params) params->enabledcount, params->bound, params->uninitvalue); - model_print("Analysis plug ins:\n"); + model_print("Analysis plugins:\n"); for(unsigned int i=0;isize();i++) { TraceAnalysis * analysis=(*registeredanalysis)[i]; model_print("%s\n", analysis->name());