\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.

