--- /dev/null
+\mysection{Implementation}\label{sec:implementation}
+
+The goal of the \TOOL specification language is to
+enable developers to write specifications against which concurrent data structures can be tested.
+We can ensure a concurrent data structure is correct with
+respect to an equivalent sequential data structure if for each
+execution of the concurrent data structure, the equivalent sequential
+history for the equivalent sequential data structure yields the same
+results.
+
+The execution space for many concurrent data
+structures is unbounded, meaning that in practice we cannot
+verify correctness by checking individual executions. However, the
+specifications can be used for unit testing. In practice,
+many bugs can be exposed by model checking unit tests for
+concurrent data structures. We have implemented the \TOOL checker as a
+unit testing tool built upon the \cdschecker framework. \TOOL
+can exhaustively explore all behaviors for unit tests and provide
+developers with diagnostic reports for executions that violate their
+specification.
+
+
+\mysubsection{Model Checker Framework}
+
+The \TOOL checker takes as input a complete execution from the
+\cdschecker model checker. The \cdschecker framework operates at the abstraction level of
+individual atomic operations and thus has neither information about
+method calls nor which atomic operations serve as ordering points.
+Thus, we extend the framework by adding {\it annotation} operations to
+\cdschecker's traces, which record the necessary information to check the specifications
+but have no effect on other operations. The \TOOL compiler
+inserts code to generate the annotation actions to communicate to the \TOOL checker
+plugin the critical events for checking the \TOOL specification.
+These annotation actions then appear in \cdschecker's list of atomic
+operations and make it convenient for \TOOL to construct
+a sequential history from the execution because for any given method
+call, its invocation event, its ordering points, and its response event are
+sequentially ordered in the list.
+
+\mysubsection{Specification Compiler}
+
+The specification compiler translates an annotated
+C/C++ program into an instrumented C/C++ program that will generate
+execution traces containing the dynamic information needed to construct the sequential history
+and check the specification assertions. We next
+describe the type of annotation actions that the \TOOL compiler
+inserts into the instrumented program.
+
+\mypara{\bf Ordering Points:} Ordering points have a conditional guard expression
+and a label. Potential ordering point annotation actions are
+inserted immediately after the atomic operation that serves as
+the potential ordering point. Ordering point check annotation actions are
+inserted where they appear.
+
+\mypara{\bf Method Boundary:} To identify a method's boundaries, \TOOL
+inserts {\it method\_begin} and {\it method\_end} annotations at the
+beginning and end of methods.
+
+\mypara{\bf Sequential States and Methods:} Since checking occurs
+after \cdschecker has completed an execution, the annotation
+actions stores the values of any variables in the concurrent data
+structure that the annotations reference.
+
+\mypara{\bf Side Effects and Assertions:} Side effects and assertions perform
+their checks after an execution. The side effects and assertions are compiled
+into methods and the equivalent sequential data structure's states are accessible to these methods.
+With this encapsulation,
+the \TOOL checker simply calls these functions to implement the side effects and assertions.
+
+\mypara{\bf Synchronization Checks:} The \TOOL checker performs
+synchronization checks in two parts: compiling the rules and runtime data
+collection. First, the \TOOL compiler numbers all methods and happens-before
+checks uniquely. For example, the rule ``\code{Update->Read}'' can be represented as (1, 0, 2, 0),
+which means instances of method 1 that satisfy condition 0 should {\it
+ synchronize with} instances method 2 that satisfy condition 0. In this case,
+ condition 0 means \code{true}. Then,
+the \TOOL compiler generates code that communicates the
+synchronization rules by passing an array of integer pairs. Runtime
+collection is then implemented by performing the condition check at
+each method invocation or response and then passing the method number
+and happens before condition if the check is satisfied.
+
+\mysubsection{Dynamic Checking}
+
+At this point, we have an execution trace with the necessary
+annotations to construct a sequential history and to check
+the execution's correctness. However, before constructing the
+sequential history, the \TOOL plugin first collects
+the necessary information for each method call, which is the {\it
+ method\_begin} annotation, the ordering point annotations, the
+happens-before checks, and the {\it method\_end} annotations. Since
+all of the operations in the trace have thread
+identifiers it is straightforward to extract the operations between the {\it
+ method\_begin} and {\it method\_end} annotations.
+
+\mypara{\bf Reorder Method Calls:} As discussed above, determining the
+ordering of the ordering points is non-trivial under the C/C++ memory
+model. This can be complicated by the fact that the C/C++ memory model
+allows atomic loads to read from atomic stores that appear later in
+the trace and that it is in general impossible to produce a sequential
+history that preserves program order for the C/C++ memory model.
+
+However, we can still leverage the reads-from relation and the
+modification-order relation to order the ordering points that appear
+in typical data structures. \TOOL uses the following rules to
+generate an ordering-point ordering $\reltext{opo}$ relation on
+ordering points. Given two operations $X$ and $Y$ that are both
+ordering points:
+
+\squishcount
+\item {\bf Reads-From:} $X \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
+
+\item {\bf Modification Order (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
+
+\item {\bf Modification Order (read-write):} $A \xrightarrow{mo} Y \ \wedge \ A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
+
+\item {\bf Modification Order (write-read):} $X \xrightarrow{mo} B \ \wedge \ B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
+
+\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$.
+\countend
+
+\mypara{\bf Generating the Reordering:}
+The \TOOL checker first builds an execution graph where the nodes are
+method calls and the edges represent the
+$\reltext{opo}$ ordering of the ordering points of the methods that
+correspond to the source and destination nodes. Assuming the absence
+of cycles in the execution graph,
+the $\reltext{opo}$ ordering is used to generate the sequential history.
+The \TOOL checker
+topologically sorts the graph to generate the equivalent sequential
+execution.
+
+When \TOOL fails to order two ordering points, the operations often commute. Thus,
+if multiple histories satisfy the constraints of \reltext{opo}, by default we generally randomly select one. However, when those operations
+do not commute, we provide developers with different options: (1) they can
+add additional ordering points to order the two nodes or
+(2) they can run \TOOL in either of the following modes: (a) \textit{loosely
+exhaustive} mode --- \TOOL explores
+all possible histories and only requires that there exists some history that passes the checks or
+(b) \textit{strictly exhaustive} mode --- \TOOL explores all possible histories and requires all histories pass the checks.
+
+
+\mypara{\bf Synchronization Checks:} Synchronization properties are
+specified using the IDs and conditions of method calls, and we have that information
+available after \TOOL constructs the sequential history and checks the preconditions
+and postconditions. For two specific method calls $c_1$ and $c_2$, we can ensure
+$c_1$ synchronizes with $c_2$ by ensuring the annotation \code{c1\_begin}
+happens-before the annotation \code{c2\_end} because any operations
+sequenced-before \code{c1\_begin} should happen-before any operations
+sequenced-after \code{c2\_end} according to the C/C++11 memory model.
+
projects / cdsspec-compiler.git / blobdiff