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