+++ /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. The \TOOL checker
-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 trace 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 check
-assertions and construct the sequential history. 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 we do not maintain program order in our
-correctness 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:
-
-\begin{enumerate}
-\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$.
-
-\end{enumerate}
-
-\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.
-If two methods are not ordered by the
-$\reltext{opo}$ order, we assume that they commute and select an
-arbitrary ordering for the methods. The \TOOL checker
-topologically sorts the graph to generate the equivalent sequential
-execution.
-
-When \TOOL fails to order ordering points, the operations often commute. Thus,
-if multiple histories satisfy the constraints of \reltext{opo}, we generally
-pick a random one for most data structures. However, when those operations
-do not commute, we provide developers with different options: (1) they can
-add additional ordering points to allow \TOOL to order the two nodes or
-(2) they run \TOOL in either of the following modes: (a) \textit{loosely
-exhaustive} mode --- \TOOL explores
-all possible histories and only requires some history to be correct or
-(b) \textit{strictly exhaustive} mode --- \TOOL explores all possible histories and requires all histories to
-be correct. With these options, developers are able to balance the
-tradeoff between specifying more ordering points and the searching
-space. For example, for a single producer single
-consumer queue based on a linked-list (maintaing \code{head} and \code{tail} pointer), if we only
-specify the update and load of the next field of a linked-list node as ordering points for
-\code{enqueue} and \code{dequeue}, \TOOL will fail to order a dequeue
-returning \code{NULL} and another enqueue because dequeue does not have the
-ordering point of loading the next field. In this case, developers can either
-add extra ordering points to order the dequeue before the enqueue or simply run it in the
-\textit{loosely exhaustive} mode and that mode will produce at least one correct
-history.
-
-\mypara{\bf Check Synchronization Properties:} Synchronization properties are
-specified using the IDs and conditions of method calls, and we have that information
-ready 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