correctness-model/writeup/.#implementation.tex.1.9

   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.  The \TOOL checker
  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 trace 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 method
  28 calls nor which atomic operations serve as ordering points.  Thus, we
  29 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 check
  45 assertions and construct the sequential history.  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
  98 C/C++ memory model. This can be complicated by the fact
  99 that the C/C++ memory model allows atomic loads to read from atomic
 100 stores that appear later in the trace and that we do not maintain program order in our
 101 correctness model.
 102
 103 However, we can still leverage the reads-from relation and the modification-order
 104 relation to order the ordering points that appear in typical data
 105 structures.  \TOOL uses the following rules to generate an ordering-point
 106 ordering $\reltext{opo}$ relation on ordering points. Given two operations $X$ and $Y$ that are both ordering points:
 107
 108 \begin{enumerate}
 109 \item {\bf Reads-From:} $X \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
 110
 111 \item {\bf Modification Order (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
 112
 113 \item {\bf Modification Order (read-write):} $A \xrightarrow{mo} Y \ \wedge \  A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
 114
 115 \item {\bf Modification Order (write-read):} $X \xrightarrow{mo} B \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
 116
 117 \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$.
 118
 119 \end{enumerate}
 120
 121 \mypara{\bf Generating the Reordering:}
 122 The \TOOL checker first builds an execution graph where the nodes are
 123 method calls and the edges represent the
 124 $\reltext{opo}$ ordering of the ordering points of the methods that
 125 correspond to the source and destination nodes.  Assuming the absence
 126 of cycles in the execution graph,
 127 the $\reltext{opo}$ ordering is used to generate the sequential history.
 128 If two methods are not ordered by the
 129 $\reltext{opo}$ order, we assume that they commute and select an
 130 arbitrary ordering for the methods.  The \TOOL checker
 131 topologically sorts the graph to generate the equivalent sequential
 132 execution.
 133
 134 When \TOOL fails to order ordering points, the operations often commute. Thus,
 135 if multiple histories satisfy the constraints of \reltext{opo}, we generally
 136 pick a random one for most data structures. However, when those operations
 137 do not commute, we provide developers with different options: (1) they can
 138 add additional ordering points to allow \TOOL to order the two nodes or
 139 (2) they run \TOOL in either of the following modes: (a) \textit{loosely
 140 exhaustive} mode --- \TOOL explores
 141 all possible histories and only requires some history to be correct or
 142 (b) \textit{strictly exhaustive} mode --- \TOOL explores all possible histories and requires all histories to
 143 be correct. With these options, developers are able to balance the
 144 tradeoff between specifying more ordering points and the searching
 145 space. For example, for a single producer single
 146 consumer queue based on a linked-list (maintaing \code{head} and \code{tail} pointer), if we only
 147 specify the update and load of the next field of a linked-list node as ordering points for
 148 \code{enqueue} and \code{dequeue}, \TOOL will fail to order a dequeue
 149 returning \code{NULL} and another enqueue because dequeue does not have the
 150 ordering point of loading the next field. In this case, developers can either
 151 add extra ordering points to order the dequeue before the enqueue or simply run it in the
 152 \textit{loosely exhaustive} mode and that mode will produce at least one correct
 153 history.
 154
 155 \mypara{\bf Check Synchronization Properties:} Synchronization properties are
 156 specified using the IDs and conditions of method calls, and we have that information
 157 ready after \TOOL constructs the sequential history and checks the preconditions
 158 and postconditions. For two specific method calls $c_1$ and $c_2$, we can ensure
 159 $c_1$ synchronizes with $c_2$ by ensuring the annotation \code{c1\_begin}
 160 happens-before the annotation \code{c2\_end} because any operations
 161 sequenced-before \code{c1\_begin} should happen-before any operations
 162 sequenced-after \code{c2\_end} according to the C/C++11 memory model.
 163