writeup/implementation.tex

   1 \mysection{Implementation}\label{sec:implementation}
   2
   3 The goal of the \TOOL specification language is to
   4 enable developers to write specifications against which concurrent data structures can be tested.
   5 We can ensure a concurrent data structure is correct with
   6 respect to an equivalent sequential data structure if for each
   7 execution of the concurrent data structure, the equivalent sequential
   8 history for the equivalent sequential data structure yields the same
   9 results.
  10
  11 The execution space for many concurrent data
  12 structures is unbounded, meaning that in practice we cannot
  13 verify correctness by checking individual executions. However, the
  14 specifications can be used for unit testing.  In practice,
  15 many bugs can be exposed by model checking unit tests for
  16 concurrent data structures.  We have implemented the \TOOL checker as a
  17 unit testing tool built upon the \cdschecker framework.  \TOOL
  18 can exhaustively explore all behaviors for unit tests and provide
  19 developers with diagnostic reports for executions that violate their
  20 specification.
  21
  22
  23 \mysubsection{Model Checker Framework}
  24
  25 The \TOOL checker takes as input a complete execution from the
  26 \cdschecker model checker.  The \cdschecker framework operates at the abstraction level of
  27 individual atomic operations and thus has neither information about
  28 method calls nor which atomic operations serve as ordering points.
  29 Thus, we extend the framework by adding {\it annotation} operations to
  30 \cdschecker's traces, which record the necessary information to check the specifications
  31 but have no effect on other operations.  The \TOOL compiler
  32 inserts code to generate the annotation actions to communicate to the \TOOL checker
  33 plugin the critical events for checking the \TOOL specification.
  34 These annotation actions then appear in \cdschecker's list of atomic
  35 operations and make it convenient for  \TOOL to construct
  36 a sequential history from the execution because for any given method
  37 call, its invocation event, its ordering points, and its response event are
  38 sequentially ordered in the list.
  39
  40 \mysubsection{Specification Compiler}
  41
  42 The specification compiler translates an annotated
  43 C/C++ program into an instrumented C/C++ program that will generate
  44 execution traces containing the dynamic information needed to construct the sequential history
  45 and check the specification assertions.  We next
  46 describe the type of annotation actions that the \TOOL compiler
  47 inserts into the instrumented program.
  48
  49 \mypara{\bf Ordering Points:} Ordering points have a conditional guard expression
  50 and a label. Potential ordering point annotation actions are
  51 inserted immediately after the atomic operation that serves as
  52 the potential ordering point.  Ordering point check annotation actions are
  53 inserted where they appear.
  54
  55 \mypara{\bf Method Boundary:} To identify a method's boundaries, \TOOL
  56 inserts {\it method\_begin} and {\it method\_end} annotations at the
  57 beginning and end of methods.
  58
  59 \mypara{\bf Sequential States and Methods:} Since checking occurs
  60 after \cdschecker has completed an execution, the annotation
  61 actions stores the values of any variables in the concurrent data
  62 structure that the annotations reference.
  63
  64 \mypara{\bf Side Effects and Assertions:} Side effects and assertions perform
  65 their checks after an execution.  The side effects and assertions are compiled
  66 into methods and the equivalent sequential data structure's states are accessible to these methods.
  67 With this encapsulation,
  68 the \TOOL checker simply calls these functions to implement the side effects and assertions.
  69
  70 \mypara{\bf Synchronization Checks:} The \TOOL checker performs
  71 synchronization checks in two parts: compiling the rules and runtime data
  72 collection.  First, the \TOOL compiler numbers all methods and happens-before
  73 checks uniquely. For example, the rule ``\code{Update->Read}'' can be represented as (1, 0, 2, 0),
  74 which means instances of method 1 that satisfy condition 0 should {\it
  75   synchronize with} instances method 2 that satisfy condition 0. In this case,
  76   condition 0 means \code{true}. Then,
  77 the \TOOL compiler generates code that communicates the
  78 synchronization rules by passing an array of integer pairs.  Runtime
  79 collection is then implemented by performing the condition check at
  80 each method invocation or response and then passing the method number
  81 and happens before condition if the check is satisfied.
  82
  83 \mysubsection{Dynamic Checking}
  84
  85 At this point, we have an execution trace with the necessary
  86 annotations to construct a sequential history and to check
  87 the execution's correctness.  However, before constructing the
  88 sequential history, the \TOOL plugin first collects
  89 the necessary information for each method call, which is the {\it
  90   method\_begin} annotation, the ordering point annotations, the
  91 happens-before checks, and the {\it method\_end} annotations.  Since
  92 all of the operations in the trace have thread
  93 identifiers it is straightforward to extract the operations between the {\it
  94   method\_begin} and {\it method\_end} annotations.
  95
  96 \mypara{\bf Reorder Method Calls:} As discussed above, determining the
  97 ordering of the ordering points is non-trivial under the C/C++ memory
  98 model. This can be complicated by the fact that the C/C++ memory model
  99 allows atomic loads to read from atomic stores that appear later in
 100 the trace and that it is in general impossible to produce a sequential
 101 history that preserves program order for the C/C++ memory model.
 102
 103 However, we can still leverage the reads-from relation and the
 104 modification-order relation to order the ordering points that appear
 105 in typical data structures.  \TOOL uses the following rules to
 106 generate an ordering-point ordering $\reltext{opo}$ relation on
 107 ordering points. Given two operations $X$ and $Y$ that are both
 108 ordering points:
 109
 110 \squishcount
 111 \item {\bf Reads-From:} $X \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
 112
 113 \item {\bf Modification Order (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
 114
 115 \item {\bf Modification Order (read-write):} $A \xrightarrow{mo} Y \ \wedge \  A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
 116
 117 \item {\bf Modification Order (write-read):} $X \xrightarrow{mo} B \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
 118
 119 \item {\bf Modification Order (read-read):} $A \xrightarrow{mo} B \ \wedge \  A \xrightarrow{rf} X \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
 120 \countend
 121
 122 \mypara{\bf Generating the Reordering:}
 123 The \TOOL checker first builds an execution graph where the nodes are
 124 method calls and the edges represent the
 125 $\reltext{opo}$ ordering of the ordering points of the methods that
 126 correspond to the source and destination nodes.  Assuming the absence
 127 of cycles in the execution graph,
 128 the $\reltext{opo}$ ordering is used to generate the sequential history.
 129 The \TOOL checker
 130 topologically sorts the graph to generate the equivalent sequential
 131 execution.
 132
 133 When \TOOL fails to order two ordering points, the operations often commute. Thus,
 134 if multiple histories satisfy the constraints of \reltext{opo}, by default we generally randomly select one.  However, when those operations
 135 do not commute, we provide developers with different options: (1) they can
 136 add additional ordering points to order the two nodes or
 137 (2) they can run \TOOL in either of the following modes: (a) \textit{loosely
 138 exhaustive} mode --- \TOOL explores
 139 all possible histories and only requires that there exists some history that passes the checks or
 140 (b) \textit{strictly exhaustive} mode --- \TOOL explores all possible histories and requires all histories pass the checks.
 141
 142
 143 \mypara{\bf Synchronization Checks:} Synchronization properties are
 144 specified using the IDs and conditions of method calls, and we have that information
 145 available after \TOOL constructs the sequential history and checks the preconditions
 146 and postconditions. For two specific method calls $c_1$ and $c_2$, we can ensure
 147 $c_1$ synchronizes with $c_2$ by ensuring the annotation \code{c1\_begin}
 148 happens-before the annotation \code{c2\_end} because any operations
 149 sequenced-before \code{c1\_begin} should happen-before any operations
 150 sequenced-after \code{c2\_end} according to the C/C++11 memory model.
 151