+++ /dev/null
-\mysection{Specification Language Design}\label{sec:specification}
-
-We begin by briefly overviewing \TOOL's basic approach. The \TOOL
-specification language specifies the correctness properties for
-concurrent data structures by establishing a correspondence with an
-equivalent sequential data structure, which requires: (1) defining the
-equivalent sequential data structure; (2) establishing an equivalent
-sequential history; (3) relating the behavior of the concurrent
-execution to the sequential history; and (4) specifying the
-synchronization properties between method invocations. The \TOOL
-specification language has the following key components:
-
-\mypara{\bf 1. Equivalent Sequential Data Structure:} This component defines a
-sequential data structure against which the concurrent data structure
-will be checked.
-
-\mypara{\bf 2. Defining the Equivalent Sequential History:}
-For real-world data structures, generally there exist two types of API methods,
-\textit{primitive} API methods and \textit{aggregate} API methods. Take
-concurrent hashtables as an example, it provides primitive API methods
-such as \code{put} and \code{get} that implement the core functionality of the
-data structure, and it also has aggregate API methods such
-as \code{putAll} that calls primitive API methods internally. From our
-experience working with our benchmark set, it is generally possible to
-generate a sequential history of primitive API method invocations for
-real-world data structures as they generally serialize on a single memory
-location --- while it is possible to observe partially completed aggregate
-API method invocations. Therefore, our specifications will focus on the
-correctness of primitive API methods.
-
-Borrowing from VYRD~\cite{vyrd} the concept of commit points, we allow
-developers to specify \textit{ordering points} --- the specific atomic
-operations between method invocation and response events that are used for
-ordering method calls. Ordering points are a generalization of the commit
-points as they also use memory operations that do not commit the data structure
-operation to order method calls. Developers then specify ordering points to
-generate the equivalent sequential history.
-
-\mypara{\bf 3. Specifying Correct Behaviors:} Developers use
-the \TOOL specification to provide a set of \textit{side effects}
-and \textit{assertions} to describe the desired behavior of each API
-method. Side effects capture how a method updates the equivalent
-sequential data structure. Assertions include both preconditions and
-postconditions which specify what conditions each method must satisfy
-before and after the method call, respectively. The specification of
-the side effects and assertions may make use of the states of the
-equivalent sequential data structure, meaning that these components
-can access the internal variables and methods of the equivalent sequential data
-structure. Additionally, they can reference the values available at
-the method invocation and response, i.e., the parameter values and the
-return value.
-
-\mypara{\bf 4. Synchronization:} The synchronization specification
-describes the desired happens before relations between API method
-invocations. \TOOL specifications allow developers to specify the
-properties at the abstraction of methods. This makes specifications
-cleaner, more understandable, and less error-prone because the
-properties do not rely on low-level implementation
-details. Moreover, \TOOL specifications allow developers to attach
-conditions to methods when specifying synchronization properties so
-that a method call might synchronize with another only under a
-specific condition. For example, consider a spin lock with
-a \code{try\_lock()} method, we need to specify that only a
-successful \code{try\_lock()} method invocation must synchronize with the
-previous \code{unlock()} method invocation.
-
-Figure~\ref{fig:speccfg} presents the grammar for the \TOOL specification
-language. The grammar defines three types of specification annotations:
-\textit{structure annotations}, \textit{method annotations}, and
-\textit{ordering point annotations}.
-In the grammar, \textit{code} means legal C/C++ source code; and
-\textit{label} means legal C/C++ variable name.
-Annotations are embedded in C/C++ comments.
-This format does not affect the semantics of the original
-program and allows for the same source to be used by both a standard C/C++
-compiler to generate production code and for the \TOOL specification compiler to
-extract the \TOOL specification from the comments. We discuss these constructs in more detail throughout the remainder of this section.
-
-\begin{figure}[!tb]
-\vspace{-.2cm}
-{\scriptsize
- \begin{eqnarray*}
- \textit{\textbf{structureSpec}} & \rightarrow & \code{"@Structure\_Define"}\\
- && \textit{structureDefine} \ \ \ (\textit{happensBefore})?\\
- \textit{structureDefine} & \rightarrow &
-(\code{"@DeclareStruct:"} \
- \textit{code})\text{*}\\
- && \code{"@DeclareVar:"} \ \textit{code}\\
- && \code{"@InitVar:"} \ \textit{code}\\
- && (\code{"@DefineFunc:"} \ \textit{code})\text{*}\\
- \textit{happensBefore} & \rightarrow & \code{"@Happens\_Before:"} \
- (\textit{invocation} \ \code{"->"} \
- \textit{invocation})\textsuperscript{+}\\
- \textit{invocation} & \rightarrow & \textit{label} \ (\ \ \code{"("} \
- \textit{label} \code{")"} \ \ )?\\
- \textit{\textbf{methodSpec}} & \rightarrow & \code{"@Method:"} \ \textit{label}\\
- && \code{"@Ordering\_Point\_Set:"} \ \textit{label} \ (\code{"|"} \
- \textit{label})\text{*}\\
- && (\code{"@HB\_Condition:"} \ \textit{label} \ \code{"::"} \ \textit{code})\text{*}\\
- && (\code{"@ID:"} \ \textit{code})?\\
- && (\code{"@PreCondition:"} \ \textit{code})?\\
- && (\code{"@SideEffect:"} \ \textit{code})?\\
- && (\code{"@PostCondition:"} \ \textit{code})?\\
- \textit{\textbf{potentialOP}} & \rightarrow & \code{"@Potential\_Ordering\_Point:"} \ \textit{code}\\
- && \code{"@Label:"} \ \ \textit{label}\\
- \textit{\textbf{opCheck}} & \rightarrow & \code{"@Ordering\_Point\_Check:"} \ \textit{code}\\
- && \code{"@Potential\_Ordering\_Point\_Label:"} \ \textit{label}\\
- && \code{"@Label:"} \ \ \textit{label}\\
- \textit{\textbf{opLabelCheck}} & \rightarrow & \code{"@Ordering\_Point\_Label\_Check:"} \ \textit{code}\\
- && \code{"@Label:"} \ \ \textit{label}\\
- \textit{\textbf{opClear}} & \rightarrow & \code{"@Ordering\_Point\_Clear:"} \ \textit{code}\\
- && \code{"@Label:"} \ \ \textit{label}\\
- \textit{code} & \rightarrow & \code{<Legal C/C++ code>}
- \end{eqnarray*}}
-\vspace{-.7cm}
-\caption{\label{fig:speccfg}Grammar for \TOOL specification language}
-\vspace{-.3cm}
-\end{figure}
-
-
-\mysubsection{Example}
-
-To make the \TOOL specification language more concrete,
-Figure~\ref{fig:rcuSpecExample} presents the annotated RCU example. We
-use {\it ordering points} to order the method invocations to construct
-the equivalent sequential history for the concurrent execution. We
-first specify the ordering points for the \code{read}
-and \code{update} methods to help define the equivalent sequential
-history. For the
-\code{read} method, the load access of the \code{node} field in
-Line~\ref{line:rcuSpecReadLoad} is the only operation that can be an ordering
-point. For the \code{update} method, there exists more than one atomic
-operation, however they only serve as an ordering point when it successfully uses the CAS operation
-to update the \code{node} field. Thus, we specify in
-Line~\ref{line:rcuSpecUpdateOPBegin} that the CAS operation should be the
-ordering point for the update operation when \code{succ} is \code{true}. We
-associate the methods with the two ordering points in
-Line~\ref{line:rcuSpecReadInterfaceOPSet} and
-\ref{line:rcuSpecUpdateInterfaceOPSet}.
-
-Next, we specify the equivalent sequential data structure for this RCU implementation.
-Line~\ref{line:declVar} declares two integer fields \code{\_data} and
-\code{\_version} as the internal states of the equivalent sequential RCU, and
-Line~\ref{line:initVar} initializes both variables to \code{0}.
-
-We then specify the correct behaviors of the equivalent sequential
-history by defining the side effects and assertions for
-the \code{read} and \code{update} methods. Side effects specify how
-to perform the corresponding operation on the equivalent sequential
-data structure. For example,
-Line~\ref{line:rcuSpecUpdateInterfaceSideEffect} specifies the side
-effects of the \code{update} to the sequential states.
-Assertions specify properties that should be true of the concurrent data structure execution.
-For example, Line~\ref{line:rcuSpecReadInterfacePostCondition}
-specifies that the \code{read} method should satisfy the postcondition that the
-returned \code{data} and \code{version} fields should have consistent values
-as the internal state of the equivalent sequential data structure.
-
-Our implementation of the RCU data structure is designed to establish
-synchronization between the \code{update} method invocation and the later
-\code{read} or \code{update} method invocation. This is important, for
-example, if a client thread were to update an array index and use the RCU data
-structure to communicate the updated index to a second client thread. Without
-synchronization, the second client thread may not see the update to the array
-index. Besides, the synchronization between two \code{update} calls ensures that
-later \code{read} will see the most updated values.
-In order to specify the synchronization, we associate \code{read} and \code{update} methods with method call identifiers
-(Line~\ref{line:rcuSpecReadInterfaceID} and Line~\ref{line:rcuSpecUpdateInterfaceID}), which for this example is the value of the
-\code{this} pointer.
-Together these annotations ensure that every
-API method call on the same RCU object will have the same method call ID.
-Line~\ref{line:rcuSpecHB} then specifies
-the synchronization property for the RCU --- any \code{update} method invocation
-should synchronize with all later \code{read} and \code{update} method invocations that have the
-same method call identifier as that \code{update} method. This guarantees that
-\code{update} calls should synchronize with the \code{read} and \code{update}
-calls of the same RCU object.
-
-
-\begin{figure}[h!]
-\vspace{-.2cm}
-\begin{lstlisting}[xleftmargin=6.0ex]
-class RCU {
- /** @Structure_Define:
- @DeclareVar:/*@ \label{line:declVar} @*/ int _data, _version;
- @InitVar:/*@ \label{line:initVar} @*/ _data = 0; _version = 0;
- @Happens_Before: Update->Read Update->Update*//*@ \label{line:rcuSpecHB} @*/
- atomic<Node*> node;
- public:
- RCU() {
- Node *n = new Node;
- n->data = 0;
- n->version = 0;
- atomic_init(&node, n);
- }
- /** @Interface: Read/*@ \label{line:rcuSpecReadInterfaceLabel} @*/
- @Ordering_Point_Set: Read_Point/*@ \label{line:rcuSpecReadInterfaceOPSet} @*/
- @ID: this/*@ \label{line:rcuSpecReadInterfaceID} @*/
- @PostCondition:/*@ \label{line:rcuSpecReadInterfacePostCondition} @*/
- _data == *data && _version == *version *//*@ \label{line:rcuSpecReadInterfaceEnd} @*/
- void read(int *data, int *version) {
- Node *res = node.load(mo_acquire);/*@ \label{line:rcuSpecReadLoad} @*/
- /** @Ordering_Point_Label_Check: true/*@ \label{line:rcuSpecReadOPBegin} @*/
- @Label: Read_Point */
- *data = res->data;
- *version = res->version;
- }
- /** @Interface: Update
- @Ordering_Point_Set: Update_Point/*@ \label{line:rcuSpecUpdateInterfaceOPSet} @*/
- @ID: this/*@ \label{line:rcuSpecUpdateInterfaceID} @*/
- @SideEffect: _data = data; _version++; *//*@ \label{line:rcuSpecUpdateInterfaceSideEffect} @*/
- void update(int data) {
- bool succ = false;
- Node *newNode = new Node;/*@ \label{line:rcuSpecUpdateAlloc} @*/
- Node *prev = node.load(mo_acquire);/*@ \label{line:rcuSpecUpdateLoad} @*/
- do {
- newNode->data = data;
- newNode->version = prev->version + 1;
- succ = node.compare_exchange_strong(prev,/*@\label{line:rcuSpecUpdateCAS} @*/
- newNode, mo_acq_rel, mo_acquire);
- /** @Ordering_Point_Label_Check: succ/*@ \label{line:rcuSpecUpdateOPBegin} @*/
- @Label: Update_Point */
- } while (!succ);
- }
-};
-
-\end{lstlisting}
-\vspace{-.2cm}
-\caption{\label{fig:rcuSpecExample}Annotated RCU specification example}
-\vspace{-.3cm}
-\end{figure}
-
-\subsection{Defining the Equivalent Sequential History}
-
-While defining the equivalent sequential history for concurrent executions is well studied in the context of the
-SC memory model, optimizations that developers typically use in the
-context of weaker memory models create the following new challenges when
-we generate the equivalent sequential history using ordering points.
-
-\begin{itemize}
-\item {\bf Absence of a Meaningful Trace or Total Order:}
-For the SC memory model, an execution can be represented by a simple
-interleaving of all the memory operations, where each load operation reads from
-the last store operation to the same location in the trace. However, under a
-relaxed memory model like C/C++11, the interleaving does not uniquely define an
-execution because a given load operation can potentially read from many
-different store operations in the interleaving. Therefore, we have to rely on
-the intrinsic relations between ordering points such as \textit{reads from} and
-\textit{modification order} to order method calls.
-
-\item {\bf Lack of Program Order Preserving Sequential History:}
-Moreover, as discussed in Section~\ref{sec:exampleMotivation}, in
-general it is not possible to arrange an execution in any totally
-ordered sequential history that preserves program order.
-
-A key insight is that many concurrent data structures' API methods
-have a commit point, which is a single memory operation that makes the
-update visible to other threads and that also serves as an ordering
-point. When two data structure operations have a dependence, it is
-often the case that their respective commit points are both
-conflicting accesses to the same memory location. In this case, the
-modification order provided by C/C++ is sufficient to order these
-operations since modification order is guaranteed to be consistent
-with the happens before relation (and therefore also the sequenced
-before relation).
-
-For cases where the method calls are independent, such as
-a \code{put(X, 1)} followed by a
-\code{get(Y)} in a hashtable where \code{X} and \code{Y} are different keys,
-the lack of an ordering is not a problem since those methods commute.
-\end{itemize}
-
-\mypara{\bf Ordering Point Annotations:} In many cases, it is not
-possible to determine whether a given atomic operation is an ordering
-point until later in the execution. For example,
-some internal methods may be called by multiple API methods. In this
-case, the same atomic operation can be identified as a potential
-ordering point for multiple API methods, and each API method later has
-a checking annotation to verify whether it was a real ordering
-point. Therefore, the \TOOL specification separates the definition of ordering
-points as follows:
-\begin{enumerate}
-\vspace{-.1cm}
-\item {\code{Potential\_Ordering\_Point} annotation:} The labeling of ordering
-points that identifies the location of a potential ordering point.
-\vspace{-.2cm}
-\item {\code{Ordering\_Point\_Check} annotation:} The checking of ordering
-points that checks at a later point whether a potential ordering point was
-really an ordering point.
-\end{enumerate}
-\vspace{-.1cm}
-
-These two constructs together identify ordering points. For
-example, assume that $A$ is an atomic operation that is marked as a
-potential ordering point with the label \code{LabelA} under the
-condition \code{ConditionA}. The developer would write a
-\code{Potential\_Ordering\_Point} annotation with the label
-\code{LabelA} and then use the label \code{LabelA} in an
-\code{Ordering\_Point\_Check} annotation at a later point.
-
-The \code{Ordering\_Point\_Label\_Check} annotation combines
-the \code{Potential\_Ordering\_Point} and the
-\code{Ordering\_Point\_Check} annotations, and makes
-specifications simpler for the use case that the ordering point is known immediately.
-For example, in Line~\ref{line:rcuSpecReadOPBegin} of
-Figure~\ref{fig:rcuSpecExample}, we use the \code{Ordering\_Point\_Label\_Check} annotation to
-identify the ordering point for \code{read} because we know the load operation
-in Line~\ref{line:rcuSpecReadLoad} is an ordering point at the time it is
-executed.
-
-Some data structure operations may require multiple ordering points.
-For example, consider a transaction implementation that first attempts
-to lock all of the involved objects (dropping the locks and retrying
-if it fails to acquire a lock), performs the updates, and then releases
-the locks. To order such transactions in a relaxed memory model, we must consider all of the
-locks it acquires and not just the last lock. Thus, we allow a
-method invocation to have more than one ordering point, and the
-additional ordering points serve to order the operation with respect to
-multiple different memory locations. For the transaction example, it
-may be necessary to retry the acquisition of locks. To support this
-scenario, the \code{Ordering\_Point\_Clear} annotation removes all
-previous ordering points when it satisfies a specific condition.
-
-Moreover, when an API method calls another API method, they can share ordering points. In
-that case, \TOOL requires that at that ordering point, the concurrent data
-structure should satisfy the precondition and postcondition of both the inner
-and outer API methods.
-
-\subsection{Checking the IO Behavior of Methods}
-
-With the specified ordering points, \TOOL is able to generate the equivalent
-sequential history. Developers then need to define the equivalent sequential
-data structure. For example, in Line~\ref{line:declVar} and
-~\ref{line:initVar} of the annotated RCU example, we use the
-\code{Structure\_define} annotation to define the equivalent sequential RCU
-by specifying the internal states as two integers, \code{\_verion} and \code{\_data}. In the
-\code{Structure\_define} annotation, developers can also specify definitions for customized
-structs and methods for convenience. We design these annotations in such a way
-that developers can
-write specifications in C/C++ code such that they do not have to learn a new
-specification language.
-
-After defining the internal states and methods of the
-equivalent data structure, developers use the \code{SideEffect} annotation to
-define the corresponding sequential API methods, which should contain the action
-to be performed on the equivalent sequential data structure. For example, in
-Line~\ref{line:rcuSpecUpdateInterfaceSideEffect} of the annotated RCU example,
-we use \code{SideEffect} to specify that when we execute the \code{update}
-method on the equivalent sequential RCU, we should update the
-internal states of \code{\_version} and \code{\_data} accordingly. When
-the \code{SideEffect} annotation is omitted for a specific API method, it means
-that no side effects will happen on the sequential data structure when that
-method is called. Take the annotated RCU as an example, the \code{read} has no
-side effects on the equivalent sequential RCU.
-
-With the well-defined equivalent sequential data structure, developers then relate
-the generated equivalent sequential history to the equivalent sequential data
-structure. In \TOOL, we allow developers to accomplish this by using the
-\code{PreCondition} and \code{PostCondition} annotations to specify the
-conditions to be checked before and after the API method appears to happen.
-For example, Line~\ref{line:rcuSpecReadInterfaceEnd} in the
-annotated RCU example means that when \code{read} appears to happen, it should
-return the same value as the current interal variables of the equivalent
-sequential RCU.
-Note that these two annotations contain legitimate C/C++
-expressions that only access the method call parameters, return value and the
-internal states of the equivalent sequential data structure.
-
-\subsection{Checking Synchronization}
-
-Under a relaxed memory model, compilers and processors can reorder
-memory operations and thus the execution can exhibit counter-intuitive
-behaviors. The C/C++11 memory model provides the developer with memory ordering that establish synchronization, e.g., \code{acquire}, \code{release}, \code{seq\_cst}. Synchronization
-serves to control which reorderings are allowed --- however,
-restricting reorderings comes at a runtime cost so developers must
-balance complexity against runtime overhead. Checking that data
-structures establish proper synchronization is important to ensure
-that the data structures can be effectively composed with client code.
-
-We generalize the notion of happens before to methods as follows.
-Method call $c_1$ happens-before method call $c_2$ if the invocation
-event of $c_1$ happens before the response event of $c_2$. Note that
-by this definition two method calls can both happen before each other
---- an example of this is the \code{barrier} synchronization
-construct. For example, for a correctly synchronized queue, we want
-an enqueue to happen before the corresponding dequeue, which avoids
-the synchronization problems discussed earlier in
-Section~\ref{sec:introNewChallenges}.
-
-In order to flexibly express the synchronization between methods, we associate
-API methods with method call identifiers (or IDs) and happens-before conditional guard
-expressions. The method
-call ID is a C/C++ expression that computes a unique ID for the call, and if it
-is omitted, a default value is used. For example, in our RCU example in
-Figure~\ref{fig:rcuSpecExample}, method \code{update} and \code{read} both
-have the \code{this} pointer of the corresponding RCU object.
-The \code{HB\_Condition} component
-associates one happens-before conditional guard expression with a unique label.
-For one method, multiple conditional guard expressions are allowed to be
-defined, and the conditional guard expression can only access the method
-instance's argument values and return value.
-
-After specifying the
-method call IDs and the \code{HB\_Condition} labels, developers
-can specify the synchronization as ``\code{method1(HB\_condition1)} \code{->}
-\code{method2(HB\_condition2)}''. When the \code{HB\_condition} is omitted, it
-defaults to \code{true}. The semantics of this expression is that all
-instances of calls to \code{method1} that satisfy the conditional guard
-expression \code{HB\_condition1} should happen-before all later instances (as determined by ordering points) of
-calls to \code{method2} that satisfy the conditional guard expression
-\code{HB\_condition2} such that both instances shared the same ID.
-The ID and happens-before conditional guard expression are important because they
-allow developers to impose synchronization only between specific method
-invocations under specific conditions. For example, in
-Figure~\ref{fig:rcuSpecExample}, Line~\ref{line:rcuSpecHB} specifies two
-synchronization rules, which together mean that the
-\code{update} should only establish synchronization with later \code{read} and
-\code{update} from
-the same RCU object under all circumstances.
projects / cdsspec-compiler.git / blobdiff