+++ /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