text:
\section{Introduction}
In today's interconnected world, there is an ever-growing need to
write correct, scalable distributed programs that can serve users at
any location with low latency. Many such applications rely on {\it
 distributed state}, which in turn is often {\it replicated} at
multiple locations. Replication addresses many common concerns in
distributed systems. It can lower latency by keeping a copy of data
close to each client, it can improve availability by increasing the
odds that some replica is on a reachable machine, and it can enhance
the scalability of request handling by allowing the overall load of
requests to be partitioned across replicas.

However, programmers are trained to write sequential programs, and often struggle to write correct distributed programs that make concurrent updates to replicated state. As programs execute, different replicas may perform updates to their replicated state at different
times or in different orders, causing replicated state to diverge and
often resulting in erroneous application behavior. While traditional
applications use heavyweight approaches (e.g. Paxos \cite{paxos}, Raft \cite{raft}, and Zookeeper \cite{zookeeper}) to retain familiar sequential semantics by ensuring that all replicas run operations in the same order, such
approaches are prohibitively expensive for many applications---particularly at global scale~\cite{cassandra,tardis,keepingCalm}. Our goal is to get the best of both worlds: allow developers to \emph{write familiar sequential code} and use \emph{program synthesis to lift} that code to an efficient distributed implementation.

The key limitation in scaling distributed systems is \textbf{coordination}, where a
quorum of replicas must communicate before any individual replica can
process some operation. Coordination among a quorum ensures that all
replicas agree upon the order of execution, allowing each replica to delay the application of
early-arriving operations, which, if applied eagerly, would lead to
divergence.
However, coordination negates the benefits of
replication, as operations issued to single replicas may now
involve high-latency communication with other nodes. Thus, \emph{avoiding} coordination has become a popular
approach in the design of modern distributed systems \cite{dynamo,hydro}.

One of the most promising tools for designing coordination-free
programs is the use of \textbf{conflict-free replicated data types (CRDTs)}
\cite{CRDTs}.  Rather than relying on explicit coordination to decide the order in which operations execute, CRDTs instead
choose to limit their operations to only those which {\em commute}; if
all replicas of a CRDT see the same set of operations, then that CRDT
will always {\em converge} to the same state, eliminating the threat of
permanent replica divergence.  As a result, the system will {\em eventually} reach a {\em
  consistent} state at each replica.  For applications that can accommodate
this {\em eventual consistency} \cite{eventual-consistency}, CRDTs
enable truly coordination-free state replication. CRDT
interpretations of traditional sequential datatypes, including
shopping carts, maps, sets, and logs, have found wide adoption in both
academia \cite{logoot,jsonCrdt} and industry \cite{leagueOfLegends,riak,akka}.

Such CRDTs are hard to specify, as the corresponding traditional data
structures' operations are often {\it not} commutative.  For example, one
may wish to replicate a set data structure that supports both
additions and removals, despite the fact that addition and removal
operations on the same element are order-sensitive.  The desire to
share such data types has given rise to a class of CRDTs that {\it
  almost} match the behavior of a sequential data type, but with a twist.
For example, remove operations will
``appear'' to evaluate before concurrent add operations in the add-wins set, regardless of the order
in which those operations arrive at each replica. These semantic differences make such CRDTs hard to verify \cite{crdtVerif}. Moreover, these CRDTs require complex logic to compactly represent both state and operations while ensuring that replicas ultimately converge.

In this paper, we simplify the process of CRDT creation by leveraging
\textbf{verified lifting}~\cite{verifiedlifting}. Using program synthesis techniques, we automatically
\emph{lift} annotated implementations of sequential data types in languages like C/C++ to full implementations of behaviorally equivalent CRDTs. These sequential data types look like standard data structures in traditional
software, are not restricted to certain types of logic,
and do not need to satisfy any convergence properties.
Users annotate the sequential specification derived from these data types with
a simple sorting function, which defines the order in which conflicting operations should \emph{appear} to occur. For
example, in a set data structure, such a sorting function may choose to order removal
operations before all concurrent addition operations, specifying the
semantics of an add-wins set.

We then {\em automatically verify} these
generated CRDTs against a combination of the sequential semantics and a
user-specified conflict resolution policy.  Crucially, such policies
are easy to specify, requiring only a handful of lines in all our
examples. We design multiple SMT
encodings of our correctness conditions that allow us to quickly prune the CRDT search space or perform unbounded verification that fully proves correctness. By automating the process of verifying a candidate design, we can generate complete
implementations of the CRDT's state, operations, and queries without any user intervention.

CRDT designs can be split into two categories: op-based CRDTs and state-based CRDTs.
In this paper, we synthesize \textbf{state-based CRDTs (CvRDTs)}, as these can be deployed in more environments and can always be translated to op-based CRDTs if necessary \cite{shapiro2011comprehensive}.
State-based CRDTs are defined by a datatype representing their state, and an associative, commutative, and idempotent (ACI) \emph{merge function}, which determines how replicas are combined to reach convergence.
This
combination forms a
join-semilattice, with the merge function serving as the join.
Early papers describe complex designs, but it has been subsequently observed that these CRDTs (and more) can be assembled via composition of simple join-semilattices on sets, integers, or Booleans~\cite{bloomL}. We leverage this approach in the context of synthesis.
By limiting the space of state types we search to only compositions of
join-semilattices, we are able to achieve convergence---normally the
most difficult property of CRDTs to verify---{\em entirely by construction}.

With this intuition, we introduce new algorithms
for searching the space of possible CRDT implementations, including
the state representation of the CRDT, operations defined on
it, and the queries by which its state may be observed.
This includes grammars for runtime logic that we search with a Syntax-Guided Synthesis engine \cite{sygus} and a parallelized enumerative search over compositions of semilattices for the state type of the CRDT. Our end-to-end synthesis algorithm is able to automatically generate a variety of practical, provably correct CRDT designs for a wide range of specifications.

To summarize, we make the following contributions:

\begin{itemize}
\item We develop a definition of CRDT correctness in terms of their
  operations and queries, and demonstrate how users can specify the
  behavior of CRDTs by combining a sequential data type with ordering
  constraints that dictate how conflicting non-commutative operations
  should be applied in a consistent manner
  (Section~\ref{specification}).

\item We introduce an SMT encoding of our correctness conditions that
  enables automated verification of CRDTs against sequential data
  types with ordering constraints, along with a bounded variant of
  the encoding that enables efficient pruning of the program search
  space (Section \ref{verification}).

\item We design a synthesis algorithm that efficiently searches
  semilattice compositions for the internal state of the CRDT, creates
  grammars for runtime components that guarantee convergence, and
  applies syntax-guided synthesis to generate both the core logic and
  invariants that prove correctness over unbounded executions (Section
  \ref{synth}).

\item We describe a practical implementation of our synthesis
  algorithm, including the details of how we automatically generate
  verification conditions from sequential data type implementations in C/C++ and optimize
  performance by synthesizing several candidate CRDTs in parallel
  (Section~\ref{implementation}).

\item We demonstrate how our algorithm can automatically lift
  sequential data types into practical CRDTs, and generate alternative
  designs with behavior equivalent to human-designed CRDTs in existing literature by searching through the space of state structures (Section \ref{eval})
\end{itemize}

\section{Motivating Example} \label{example}
The distributed shopping carts problem was made popular by Amazon Dynamo~\cite{dynamo} as an essential business problem with a clever coordination-free solution. In the original formulation of this problem, we track a mapping of items to non-negative counts representing how many of that item are in the cart. Users can interact with the shopping cart by requesting insertions and removals of items. The cart can also be queried to determine the count of each item during a checkout procedure. Our goal is to replicate a single shopping cart across many distributed nodes to improve fault tolerance, while ensuring eventual consistency so that the accumulated states on any node can be used during checkout to identify the complete cart.

Let us focus on a simplified version of this problem, where each item can only be in the cart at most once---effectively simplifying the cart to a set of items. A developer without a distributed systems background could attempt to implement this as a replicated data type by having the insertions, removals, and queries all operate on a standard hash-set. However, if we deploy this in a distributed setting, we will immediately start to see consistency issues.

\begin{figure}[h]
    \centering
    \includegraphics[width=\textwidth]{combined-graphs.png}
    \caption{Situations where a sequential type (left) has consistency issues that are resolved by a CRDT (right).}
    \label{fig:broken_crdt_examples}
\end{figure}

Consider the leftmost scenario in Figure~\ref{fig:broken_crdt_examples}, where a shopping cart is replicated across two nodes. When the user sends in operations to add and remove the same item, these requests are distributed between the nodes. In this case, the node that receives the insert operation will add the item to its local set, but the node that receives the remove will treat it as a no-op because its local set is currently empty. We may wish to merge the state at these nodes via set union, but this would fail to preserve the locally-ineffective remove operation; it is unclear if this matches user expectations.

If we periodically share state via gossip \cite{gossip}, new situations emerge in which convergence may be disrupted. In the execution graph with gossip on the left of Figure~\ref{fig:broken_crdt_examples}, we see an execution where one node processes an insert, and the other processes an insert and then remove of the same element. Even if we merge via set union, we still end up with non-deterministic results depending on when gossip takes place. If the state of the right node is gossiped to the left after the insert but before the remove, the left node will merge the new value into its local state. Even after the remove is processed, merging the two states together will still result in the element 2 being present. But if the gossip were not to take place, the merged state would only have the element 1.

Situations like these have severe correctness implications, and it can be challenging to reason about the many ways a distributed system can break sequential assumptions built into your data type. Furthermore, it is challenging for developers to fix such correctness issues, because doing so involves reasoning about all possible orderings and interleavings of operations, and their possible outcomes. Our work aims to tackle this issue by automatically synthesizing a CRDT, which satisfies the property of \emph{convergence} and can be safely replicated in a distributed cluster without requiring coordination. Let's explore how a user would synthesize a shopping cart CRDT with our system.

Our synthesis algorithm takes two inputs: a sequential data type that defines the semantics of operations and queries the CRDT will support, and an ordering constraint that specifies how to resolve conflicts between non-commutative operations. We already have the first, since the user has implemented a sequential, single-node shopping cart. For the second, the non-commutative operations in the sequential type are inserts and removes, so the developer may decide that they want the CRDT to resolve conflicting operations by having the removes ``win.'' This can be encoded as a simple pairwise ordering constraint ($opOrder$) that is passed into the synthesis algorithm.

Once our algorithm is given this specification, it searches potential state types and runtime logic that are both behaviorally correct and convergent. Along the way, our synthesis algorithm prunes out candidates by using bounded verification to quickly check correctness against short sequences of operations. Eventually, the synthesis engine will produce a provably correct CRDT. For our running example, we might get the CRDT in Figure~\ref{fig:synthesis_example} with an internal state of two sets $(s1, s2)$.

\begin{figure}[h]
    \centering
    \hspace{0.02\textwidth}
    \begin{minipage}{.5\textwidth}
      \begin{minted}[fontsize=\small]{c}
set* init_state() { return set_create(); }

set* next_state(set* state, int add, int v) {
  if (add == 1) return set_insert(state, v);
  else return set_remove(state, v);
}

int query(set* state, int v) {
  return set_contains(state, v);
}
      \end{minted}

      \vspace{0.1cm}

      $opOrder(o_1, o_2)$: $o_{1,add} = 1 \lor o_{2,add} \neq 1$
    \end{minipage}
    \begin{minipage}{.42\textwidth}
      \begin{algorithm}[H]
        \CRDT{ShoppingCart}{
        \InitialState{$(\{\}, \{\})$}
        \Operation{$((s_1, s_2), add, value)$}{
          \eIf{$add = 1$}{
            \Return{$((s_1 \cup \{value\}), s_2)$}
          }{
            \Return{$(s_1, (s_2 \cup \{value\}))$}
          }
        }
        \Query{$((s_1, s_2), v)$}{
          \Return{$v \in (s_1 \setminus s_2)$}
        }
        }
      \end{algorithm}
    \end{minipage}
    \caption{An example of a sequential data type we can lift from and the CRDT we synthesize.}
    \label{fig:synthesis_example}
\end{figure}

Readers who are familiar with literature on CRDTs may recognize the implementation above as a Two-Phase Set \cite{shapiro2011comprehensive}, one of the classic CRDTs that mimics the behavior of a set while guaranteeing convergence in distributed execution. This synthesized implementation is provably correct for the given sequential specification with the operation reordering, so we can deploy it in our distributed application without having to worry about manually proving complex CRDT properties. We can see on the right of Figure~\ref{fig:broken_crdt_examples} that our CRDT now consistently handles the execution graphs that had conflicts with the naive implementation. Without any baked-in knowledge of existing CRDTs, our synthesis system is able to automatically generate such implementations that were previously only designed by distributed systems researchers, and can generate alternate designs by searching the wider space of CRDT structures.

\section{Specifying CRDTs with Sequential Data Types} \label{specification}
In verified lifting, a key piece of the puzzle is specifying correctness of the synthesized program in terms of the reference code. The correctness conditions are then encoded in a machine-checkable language such as SMT logic, which allows the synthesis algorithm to rapidly check candidate programs with a solver. In past work, which focused on transpiling legacy functions into high-level DSLs, correctness has a relatively simple definition: the synthesized logic must produce an identical output to the original code for any valid input. When lifting CRDTs, however, this approach is not applicable since the sequential data type and CRDT operate as ongoing processes that execute operations over time and respond to an unbounded number of queries. In this section, we develop a formal model for sequential data types and CRDTs and introduce the correctness conditions for a CRDT to match a sequential specification.

We model sequential data types as a combination of two functions: a state transition ($st(s, o)$) that takes in the current state and an operation (a tuple of client-provided parameters) and returns an updated state, and a query function ($query(s, q)$) that takes the current state and a query (similarly, a tuple of client-provided parameters) and returns some data of any type. Sequential types also define an initial state ($initialState$) that is updated as operations are processed. This model can handle a wide range of sequential data types, since patterns like multiple operations/queries can be combined into a single $st$/$query$ function and we do not restrict the logic inside the those functions.

On the CRDT side, we have a similar definition with one additional function to handle gossip from distributed nodes. Syntactically, we distinguish the values and functions corresponding to a CRDT candidate from the sequential data type by attaching an apostrophe to the CRDT names. Just like before, we have an initial state ($initialState'$), state transition ($st'(s', o)$), and query ($query'(s', q)$) which model how the CRDT processes requests over time. In addition, we introduce a merge function ($merge'(s_1', s_2')$), which is used to merge a node's local state with gossip received from other nodes so that the replicated data converges.

CRDTs have two key components to their correctness: they must respond appropriately to operations and queries, and they must satisfy the convergence properties to ensure safe distributed execution. We guarantee the latter by construction with grammar restrictions on the state (Section~\ref{synth_structure}) and runtime logic (Section~\ref{synth_runtime}). In this section, we focus on specifying the former by comparing the behavior of the CRDT to a reference sequential data type.

\subsection{Specifying CRDTs with Operation Sequences}
Because the sequential data type and the CRDT may use different internal state representations, we cannot directly compare instances of them by comparing their states. As a result, our definition of correctness must reason about the \emph{user-observable behavior} of the data type over \emph{unbounded sequences of interactions}. Both the sequential type and the CRDT have two components a user can interact with: the state transition and the query. Since queries are the only way for users to observe data, we want to ensure that after processing any sequence of user interactions, the sequential type and the CRDT respond identically to any query. Because queries do not modify the state, we can simplify this condition: a sequential type and CRDT are equivalent if both return the same result to an arbitrary query after processing an arbitrary sequence of operations.

But we have to go a step further to justify this correctness definition, since CRDTs can be executed in a distributed system. When we replicate the data type, operations will non-deterministically arrive at nodes in different orders. In addition, the use of gossip protocols in the cluster results in additional state updates when a node merges its local state with a state received from another node. As a result, instead of having a totally-ordered sequence of operations taking the initial state to the final one, we instead have a partial order---a directed acyclic graph---where states on different nodes can be concurrently updated and merged with each other.

Thankfully, the operations on a CRDT are commutative: the CRDT state depends only on the {\em set} of observed operations, and is independent of order.  Therefore, as long as the provided CRDT is convergent, we can reduce verification of a distributed CRDT execution to the sequential case via an arbitrary flattening of the execution graph.

\subsection{Resolving Commutativity with Operation Orderings}
So far, our correctness conditions require strict equivalence of the sequential data type and the synthesized CRDT. However, the additional requirement of operator commutativity on the CRDT means that many sequential types with non-commutative operations, including common ones like sets and maps, cannot directly correspond to an equivalent CRDT but instead are mapped to many popular CRDT variants that make different semantic compromises.

In our system, users can define these semantic adjustments through \textbf{operation orderings}, which loosen the correctness requirements to only verify sequences of operations following a specific ordering constraint. Formally, a user can define a partial order $opOrder(o_1, o_2)$, which returns true when a call to $o_2$ is allowed to occur after a call to $o_1$. As an example of the effect of this ordering, recall the shopping cart we lifted in the motivating example. In our sequential data type, inserts and removals do not commute, so no CRDT exists that strictly matches its semantics. However, we can resolve the conflict by introducing an ordering between the operations. If we specify that removes take place before inserts, we get a specification of a Grow-Only Set, which treats removes as no-ops. On the other hand, if we specify that removes take place after inserts, we get a specification of a Two-Phase Set, where elements can be inserted, then removed, but not inserted again.

Instead of having to consider all potential interleavings of operations in a distributed system, operation orderings make it possible for users to specify the distributed behavior in terms of a \emph{sequential execution model}. This makes it possible for non-experts to use our synthesis algorithm, since they can reason about the operation ordering with the existing sequential data type. In our implementation, we also provide a tool that can discover non-commutative operations in the sequential code provided by the user, which further simplifies the process of defining an ordering since the tool guides users with concrete examples of operations that need to be ordered.

This general approach of ordering operations to resolve commutativity allows us to synthesize a wide variety of CRDTs by applying different orderings to simple sequential data types. Intuitively, ordering the non-commutative operations of the sequential type transforms the semantics to be effectively commutative, since any ordering of non-commutative operations will always be reordered into the same sequence by the $opOrder$ constraint. Since the CRDTs we are verifying are already guaranteed to have commutative operations, it then suffices to verify correctness with sequences of operations that follow this order.

\subsection{Operation Orderings with Time}
A popular pattern when designing replicated data types is to timestamp all operations at the nodes they are initially received at, which makes it possible to introduce sequential semantics without losing the convergence property. For example, the last-writer-win set is a classic CRDT that uses timestamps on operations to allow repeated insertions and removals of the same element, with remove or add-wins semantics that resolve conflicts between concurrent operations.

When a user provides a sequential data type and ordering specification, we allow them to enable a flag to introduce timestamps to each operation. This flag augments every operation with an integer timestamp $o_t$, which is computed by the local node at runtime using a source that can be mapped to an integer value. We use Lamport timestamps \cite{lamportTimestamps} as this source, which offers a partial causal order. We then augment the $opOrder$ to order operations first by their timestamp, and then apply the user-defined ordering on operations with the same timestamp: $$opOrder(o_1, o_2) \triangleq (o_{1,t} < o_{2,t}) \lor ((o_{1,t} = o_{2,t}) \land opOrder_{orig}(o_1, o_2))$$

When we introduce time, we also must introduce constraints on the operations we consider in our correctness conditions to avoid degenerate cases with illegal timestamps. We do this through an additional user-defined function $opPrecondition(o)$, which checks that an operation is valid. When timestamps are enabled, we define the precondition as $opPrecondition(o) = o_t > 0$ to ensure the operations we check have valid timestamps. Users can also add constraints to this precondition based on domain knowledge, such as if an operation parameter will always be positive.

\section{Automated CRDT Verification} \label{verification}
With our formal definition for CRDT correctness in hand, we must encode these conditions so that candidate CRDT designs can be automatically verified. We tackle this by encoding correctness in SMT logic, which allows us to use solvers like Z3 \cite{z3} and CVC5 \cite{cvc5} to automatically prove correctness or find counterexamples. However, these solvers cannot directly reason about unbounded sequences of operations, so we must break down the correctness conditions into an inductive proof that reasons about individual state transitions.

\subsection{State Equivalence} \label{sec:verification_equivalence}
First, we focus on checking CRDT correctness without considering the ordering constraint. To build this inductive proof, we need a way to reason about the relationship between the states of the sequential data type and candidate CRDT after processing the same, arbitrary sequence of operations. To do this, we choose to relate the states of the CRDT and sequential data type implementations in the style of a bisimulation.

\newcommand{\ensuremath{\textit{equivalent}}}{\ensuremath{\textit{equivalent}}}
\newcommand{\ensuremath{\textit{initialState}}}{\ensuremath{\textit{initialState}}}
\newcommand{\ensuremath{\textit{opPrecondition}}}{\ensuremath{\textit{opPrecondition}}}
\newcommand{\ensuremath{\textit{opOrder}}}{\ensuremath{\textit{opOrder}}}
\newcommand{\ensuremath{\textit{query}}}{\ensuremath{\textit{query}}}
\newcommand{\ensuremath{\textit{orderWithState}}}{\ensuremath{\textit{orderWithState}}}

\begin{figure}[h]
  \begin{align*}
    (1)&~ \textit{\ensuremath{\textit{equivalent}}}(\ensuremath{\textit{initialState}}, \ensuremath{\textit{initialState}}')\\
    (2)&~ \forall{s,s',o}: (\ensuremath{\textit{equivalent}}(s, s') \land \ensuremath{\textit{opPrecondition}}(o)) \implies \ensuremath{\textit{equivalent}}(st(s, o), st'(s', o))\\
    (3)&~ \forall{s,s',q}: \ensuremath{\textit{equivalent}}(s, s') \implies \ensuremath{\textit{query}}(s, q) = \ensuremath{\textit{query}}'(s', q)
    \end{align*}
    \caption{The verification rules that constrain CRDT synthesis to preserve the source semantics}
    \label{fig:verif_rules}
\end{figure}

We approach this invariant by introducing the \textbf{state equivalence} function, which relates the states of the sequential reference and synthesized CRDT. Formally, if the reference and synthesized data types are in equivalent states, then after both process an arbitrary sequence of operations they will return the same result to any query. Intuitively, the equivalence function describes which states of the sequential data type correspond to states of the CRDT that capture the same queryable knowledge. Furthermore, the equivalence function captures invariants about the CRDT that filter unreachable states from the verification conditions.

We begin our conditions in Figure \ref{fig:verif_rules} with rule (1), that the initial states of the sequential data type and CRDT must be equivalent. Next, we build the inductive proof that carries equivalence all the way to the final query. We start by encoding the query constraint in rule (3), where we query the reference and synthesized implementations in equivalent states. For this condition, the query results are of the same type so we can directly check for equality. Intuitively, this rule requires equivalence to be a guarantee that queries on the two states return the same result. However, since equivalence deals with not only the current state but also queries on the future states, the equivalence condition may need to be stronger. The condition that forces this strengthening is the inductive step of our proof in rule (2), which checks that if the two data types are in equivalent states, then after executing the same operation they should still be in equivalent states.

As with past lifting work, the equivalence invariant is synthesized alongside the other runtime logic. But with equivalence defined in terms of just the reference and synthesized states, synthesis can quickly become infeasible when the internal states involve large, unbounded structures such as sets and maps (Section~\ref{synth_structure}), which would require the synthesizer to produce higher-order logic like reductions to compare the states. To reduce this burden on the synthesis algorithm, we introduce an additional query parameter and adjust the definition of {\ensuremath{\textit{equivalent}}} to check that the states are observationally equivalent \emph{for the given query}.

\begin{figure}[h]
    \begin{align*}
      (1)&~\mathbf{\forall{q}}: \ensuremath{\textit{equivalent}}(\ensuremath{\textit{initialState}}, \ensuremath{\textit{initialState}}',\mathbf{q})\\
      (2)&~\forall{s,s',o,\mathbf{q}}: (\ensuremath{\textit{equivalent}}(s, s', \mathbf{q}) \land \ensuremath{\textit{opPrecondition}}(o)) \implies \ensuremath{\textit{equivalent}}(st(s, o), st'(s', o), \mathbf{q})\\
      (3)&~\forall{s,s',q}: \ensuremath{\textit{equivalent}}(s, s', \mathbf{q}) \implies \ensuremath{\textit{query}}(s, q) = \ensuremath{\textit{query}}'(s', q)
    \end{align*}
    \caption{The verification conditions with the additional query parameter for equivalence}
    \label{fig:rules_with_q}
\end{figure}

By giving the equivalence function a specific query, the synthesized logic can now focus on comparing the parts of each state that are relevant to that query. For example, when synthesizing a CRDT that uses maps, this can result in significant simplifications like only checking one key. This change also makes it possible to seed the {\ensuremath{\textit{equivalent}}} function with a condition that the CRDT returns the same response to the given query as the sequential data type, which further reduces the burden on the synthesizer. We update the verification conditions by adding a new quantifier for the query to rules (1) and (2). In rule (3), we simply pass the existing query variable to the {\ensuremath{\textit{equivalent}}} function. We define these updated conditions in Figure~\ref{fig:rules_with_q}.

So far, our verification conditions ignore the presence of the user-defined operation ordering (\ensuremath{\textit{opOrder}}), which specifies how the CRDT should handle conflicting non-commutative operations in the sequential reference. In our system, we implement two encodings of the constraints imposed by this ordering: one that is only suitable for bounded verification but enables efficient exploration of the program space, and one that supports unbounded verification but requires synthesizing additional invariants. In our end-to-end algorithm (Section~\ref{sec:synth_e2e}), we use the bounded encoding first to quickly prune out candidate state structures. The unbounded encoding is used as a followup to fully verify any candidates that are emitted by the first phase.

\subsection{Solution Pruning with Bounded History}
First, let us consider the bounded situation, where we verify the candidate CRDT against short sequences of operations on which we can directly evaluate the ordering constraint. There is one key modification to the existing verification rules that we need to make: the state transition should only be checked when the operation being processed is in-order according the the user-provided function. To encode this, we augment the synthesized state with a temporary member ($s'_h$) that stores a bounded history of operations that have been processed. Note that this additional member cannot be used by any of the synthesized logic, since its only role is to aid verification.

\begin{figure}[h]

    \begin{align*}
    \text{list in-order/valid}: lio(s'_h) \triangleq& \forall{i}: (i < |s'_h|) \implies (opPrecondition(s'_h[i])~\land\\
    &((i < |s'_h| - 1) \implies opOrder(s'_h[i], s'_h[i + 1])))\\
    \text{list coherent}: lc(s') \triangleq& s' = fold(s'_h, initialState', st')
    \end{align*}
  \begin{align*}
    (1)~& \forall{q}: \ensuremath{\textit{equivalent}}(\ensuremath{\textit{initialState}}, \ensuremath{\textit{initialState}}', q) \land \mathbf{\ensuremath{\textit{initialState}}'_h = []}\\
    (2)~& \forall{s,s',o,q}: (\ensuremath{\textit{equivalent}}(s, s',q) \land \ensuremath{\textit{opPrecondition}}(o) \land\\
    &\mathbf{lio(s'_h) \land lc(s') \land \ensuremath{\textit{opOrder}}(s'_h[|s'_h|-1], o)})\\
    &\implies \ensuremath{\textit{equivalent}}(st(s, c), st'(s', o),q)\\
    (3)~& \forall{s,s',q}: \ensuremath{\textit{equivalent}}(s, s', q) \implies \ensuremath{\textit{query}}(s, q) = \ensuremath{\textit{query}}'(s', q)
    \end{align*}

    \caption{The verification rules updated to use history lists for ordering relaxations}
    \label{fig:verif_rules_history_list}
\end{figure}

To maintain this history, we augment the state transition to insert the operation parameters into the history list. In addition, we update the initial state to include an empty history list. Then, we update the state transition verification rule to add a precondition that the history list is in-order and coherent with the state of the CRDT. First, we check that every pair of operations in the history are in-order, since the history list is a quantified variable in the SMT encoding and may have out of order values. Then, we verify that the synthesized state equals the result of folding over the history with the synthesized state transition. Since the history list is bounded, this collapses into a bounded number of state transitions and can be efficiently verified by an SMT solver. Finally, we add a condition that the operation being applied in rule (2) is in-order with the existing history, which can be checked by comparing it against the last operation (since the ordering constraint is transitive).

Note that we do not need to introduce the ordering and coherence preconditions to the query verification conditions in rule (3) even though that rule operates on arbitrary input states. Our inductive proof requires that for every reachable synthesized state, the equivalence function is true for some state of the sequential data type. As a result, we do not need to constrain \emph{how} we reach the synthesized state being evaluated, just that any equivalent instance of the sequential reference will return the same response to the query.

Altogether, these rule modifications are summarized in Figure \ref{fig:verif_rules_history_list}. With bounding, this encoding enables efficient synthesis of the state transition and query functions with the ordering relaxations. However, the use of lists in the verification conditions make this approach infeasible for unbounded verification, since an SMT solver may not be able to execute the reductions in the coherency check when the input list is of unknown length.

\subsection{Unbounded History Verification with Invariant Synthesis}
To introduce the ordering constraint to the unbounded verification conditions, we take the approach of strengthening the inductive hypothesis by synthesizing additional invariants. The key insight in this approach is that CRDTs states are accumulated by merging updates produced by each operation, so we can enforce orderings that use simple comparisons (such as equality or greater/less than) in terms of the accumulated state instead of the individual operations in the history of the CRDT. For example, in the shopping cart example where inserts are ordered before removes, we know that an insert is in-order when the set of removed elements is empty.

Formally, we introduce another synthesized Boolean function $\ensuremath{\textit{orderWithState}}(s', o)$, which returns true if the operation $o$ satisfies the ordering constraint against the history of operations \emph{implied} by the state of the CRDT. This function must be true when executing any operation in a correctly ordered sequence. This in turn ensures that the CRDT correctly handles all executions that satisfy the ordering constraint. We can encode the requirement that $\ensuremath{\textit{orderWithState}}(s', o)$ must be true by augmenting the base case and inductive step verification conditions.

\begin{figure}[h]
  \begin{align*}
    (1)~& \forall{o,q}: \ensuremath{\textit{equivalent}}(\ensuremath{\textit{initialState}}, \ensuremath{\textit{initialState}}', q) \land\\
    &(\ensuremath{\textit{opPrecondition}}(o) \implies \mathbf{\ensuremath{\textit{orderWithState}}(\ensuremath{\textit{initialState}}', o)})\\
    (2)~&\forall{s,s',o_1,o_2, q}: (\ensuremath{\textit{equivalent}}(s, s', q) \land \ensuremath{\textit{opPrecondition}}(o_1) \land \mathbf{\ensuremath{\textit{orderWithState}}(s',o_1)})\\
    &\implies (equivalent(st(s,o_1), st'(s',o_1), q) \land ((opOrder(o_1, o_2) \land opPrecondition(o_2)) \implies\\
    &\mathbf{orderWithState(st'(s',o_1), o_2)}))\\
    (3)~&\forall{s,s',q}: equivalent(s, s', q) \implies query(s, q) = query'(s', q)
  \end{align*}

    \caption{The verification rules updated to use a synthesized invariant for ordering relaxations}
    \label{fig:verif_rules_invariant}
\end{figure}

To start, we update the base case to require that any operation executed in the initial state must be in-order. Then, we update the inductive step to enforce the correctness of $orderWithState$ on \emph{all} operations in an ordered sequence, by extending rule (2) to reason about two adjacent operations. We introduce a precondition that checks if the first operation being executed is in-order with the state, and enforce the transitive property that $o_2$ be in-order with the state after $o_1$ is processed if it is pairwise in-order after $o_1$. When these conditions are satisfied, we have a proof that our CRDT matches the sequential data type under the operation ordering for any unbounded execution.

\section{CRDT Synthesis Algorithm} \label{synth}
Now that we have a formal specification of correctness that can be verified by an SMT solver, we are ready to define the synthesis algorithm for CRDT implementations. There are four core components to synthesize: the type of the internal state, the initial state, the state transition function, and the query function. We must also synthesize the $equivalent$ and $orderWithState$ invariants from the previous section to enable verification. As discussed before, the synthesized CRDT may use a completely different state structure than the source, which adds a new layer of complexity since the state type affects which operations can be used in the synthesized functions.

In Section~\ref{specification}, we explained that our verification conditions only check the user-observable behavior of the CRDT, but do not verify that the CRDT implementation meets the convergence properties. Instead of checking these properties through verification conditions \cite{cav19crdtverification}, we craft our CRDTs in a way that satisfies these properties \emph{by construction}. Inspired by past work on designing coordination-free distributed systems \cite{bloomL}, we synthesize CRDTs that use \textbf{semilattice compositions} for their internal state, which makes it straightforward to enforce monotonicity and commutativity since these are properties of the semilattice join.

\subsection{State Synthesis} \label{synth_structure}
To explore candidate state structures for the CRDT, we use the classic synthesis approach of defining a grammar and iteratively processing deeper structures. Because we focus on compositions of semilattices, our grammar consists of simple rules for primitives, sets, maps, and tuples.

For primitive types, we include semilattice definitions based on Booleans and integers, which are sufficient to lift a wide variety of sequential data types. For Booleans, we have the \texttt{OrBool} lattice, which is a Boolean that has $\bot = false$ and is merged with $\lor$. For integers, we provide the \texttt{MaxInt} semilattice, which merges integers by taking the maximum. Beyond the primitives, we include a semilattice definition for \texttt{Set<T>}, which can have a non-lattice type \texttt{T} for elements; the only constraint on \texttt{T} is that it supports equality.

Our lattice definitions for composite data structures are more complex. First, we offer the \texttt{LexicalProduct<A, B>} semilattice, where A and B are themselves semilattices. In this semilattice, the first element has priority over the second when determining the ordering of two instances. This type is especially useful for CRDTs that use timestamps to have recent operations override older ones, but need to perform a merge over the underlying values when the effects of concurrent operations are combined. We define the lattice join for \texttt{LexicalProduct} as:

$$(a_1, b_1) \sqcup (a_2, b_2) = \begin{cases}
  (a_1, b_1) & a_1 > a_2 \\
  (a_2, b_2) & a_2 > a_1 \\
  (a_1 \sqcup a_2, b_1 \sqcup b_2) & \text{otherwise}
\end{cases}$$

It should be clear that this definition respects the lattice axioms of associativity, commutativity, and idempotence. Of course, these tuples can be nested to form tuples of arbitrary arity. We also support the \texttt{FreeTuple<A,B>} lattice, which simply joins elements pairwise (i.e. $(a_1, b_1) \sqcup (a_2, b_2) = (a_1 \sqcup a_2, b_1 \sqcup b_2)$) and can similarly be nested to form tuples of arbitrary arity.

In some cases we may not know the desired arity of a \texttt{FreeTuple} in advance, or we may not need all the ``fields'' of such a tuple in a given execution. To address this, we offer a \texttt{Map<K, V>} semilattice, where \texttt{K} can be any type that supports equality, and \texttt{V} is a semilattice. Our maps support common operations such as insertions with the same semantics as regular maps, except when inserting keys that are already present in the map. Instead of overwriting the value, we use the lattice join for the value type to combine the existing value with the one being inserted. This carries over to our definition of the lattice join for maps themselves, where we insert the entries of both maps, with keys that are present in both maps having their values merged according to their join:

$$m_1 \sqcup m_2 = \{k_i: \begin{cases}
  m_1[i] & (k_i \in m_1) \land (k_i \not\in m_2) \\
  m_2[i] & (k_i \not\in m_1) \land (k_i \in m_2) \\
  m_1[i] \sqcup m_2[i] & (k_i \in m_1) \land (k_i \in m_2)
\end{cases})\}$$

Again, it should be clear that this respects the standard lattice axioms. Given these semilattice types, we can construct the grammar in Figure~\ref{fig:lattice_grammar} that defines the space of compositions to explore. Our grammar covers a large space of semantics, since the available types encode core capabilities such as free and lexicographically-ordered semilattice products (via maps and tupling) and general semilattice representations (sets)\footnote{The finite powerset lattice---i.e. the lattice of sets from a finite domain with Union and Intersect---is natural and widely used. It is in a strong sense a ``universal'' lattice structure: every order relation on a countable domain is isomorphic to a suborder of the powerset of the natural numbers (see, e.g., \cite{hamkins}).
While the powerset lattice is expressive, it is often more natural to encode state in a more structured composite lattice, as evinced by both the CRDT literature~\cite{bloomL,anna} and the results of our synthesis.}. In our end-to-end synthesis algorithm, we explore types in this grammar with iteratively increasing depth bounds and attempt to synthesize the runtime component of the CRDT for each one. Note that we only include \texttt{FreeTuple} in the top-level $latticeList$ for CRDTs that need multiple semilattices in their state; we can omit it in the deeper grammar to reduce the search space since \texttt{Map} is strictly more general.

\begin{figure}[h]
    \centering
    \begin{minipage}[t]{.7\textwidth}
    \begin{grammar}
    <latticeList> ::= <latticeType> | FreeTuple(<latticeType>, <latticeList>)

    <latticeType> ::= OrBool | NegBool | MaxInt
    \alt Set(<type>) | Map(<type>, <latticeType>)
    \alt LexicalProduct(<latticeType>, <latticeType>)

    <type> ::= Bool | Int
    \end{grammar}
    \end{minipage}

    \caption{The grammar defining compositions of semilattices we explore during synthesis.}
    \label{fig:lattice_grammar}
\end{figure}

\subsection{Runtime Synthesis} \label{synth_runtime}
With our state structure selected, we can now move on to synthesizing the runtime logic. Our algorithm for runtime synthesis proceeds in two phases: a first step that synthesizes the core logic with the bounded history verification conditions, and a second that synthesizes the additional invariants required for unbounded verification.

\subsubsection{Core Logic Synthesis}
We derive significant power from our choice to implement the internal state of the CRDT via a semilattice.  First, we observe that, as lattice join is compositional, we can define the merge function as the lattice join on the internal state; this in turn is derived directly from the state's constituent lattices.  Next, we observe that we can also implement {\em operations} in terms of this lattice join: we define
our state transition as $st'(s', o) = merge'(s', f'(o))$, where $f'$, which returns a lattice value of the same type as $s'$, is
the function that we actually synthesize.  This choice grants us monotonicity, commutativity, associativity, and idempotence entirely for free, derived from the lattice join itself.

Along with the state transition, we synthesize the query
function that is used to pull information out of the CRDT. There are
no convergence restrictions on the query since it does not mutate the state, leaving only the sequential reference as a source of
constraints on its synthesis. As a result, we do not need to craft the
query function in any special way, and can let the synthesis engine
drive the search of the query logic.

To support the inductive step of the verification conditions, we must synthesize the equivalence function. This function has two intuitive roles: (1) a \emph{cross-state relation} that identifies which states of the sequential data type and the CRDT are observationally equivalent, and (2) a \emph{CRDT state invariant} that is needed to strengthen the inductive hypothesis of the correctness proof. Following this intuition, we split the synthesis of the equivalence function into components for each role. As discussed when we introduced the query parameter to $equivalent$ in Section~\ref{sec:verification_equivalence}, we seed the equivalence function with a check that both states respond identically to the given query. This means that our equivalence function has the form $equivalent(s, s', q) \triangleq query(s, q) = query'(s', q) \land relation'(s, s') \land invariant'(s')$, where $relation'$ and $invariant'$ are synthesized.

The $relation'$ function is synthesized using the same grammar as other functions, but with a slightly lower depth bound since we already have the query check. With the bounded history encoding, the $invariant'$ component is unnecessary because we check that the state of the CRDT equals the result of applying the state transition function over the history of operations. We will revisit the invariant in Section~\ref{sec:synth_unbounded}, when we synthesize with unbounded history.

\begin{figure}[h]
    \centering
    \begin{minipage}[t]{.45\textwidth}
    $\forall{T, U}$
    \begin{grammar}
    <bool> ::= false | true
    \alt <bool> $\land$ <bool> | <bool> $\lor$ <bool>
    \alt $\lnot$ <bool>
    \alt <int> $>$ <int> | <int> $\geq$ <int>
    \alt <T> $=$ <T>
    \alt<T> $\in$ <Set(T)> | <Set(T)> $\subset$ <Set(T)>

    <int> ::= 0 | 1 | <int> $+$ <int> | <int> $-$ <int>
    \alt constants in the sequential source
    \end{grammar}
    \end{minipage}
    \begin{minipage}[t]{.45\textwidth}
    \hfill
    \begin{grammar}
    <Set(T)> ::= $\{\}$ | $\{$<T>$\}$
    \alt <Set(T)> $\cup$ $\{$<T>$\}$ | <Set(T)> $\cup$ <Set(T)>
    \alt <Set(T)> $\setminus$ <Set(T)>

    <Map(T, U)> ::= $\{\}$ | $\{$<T>: <U>$\}$
    \alt <Map(T, U)> $\cup$ <Map(T, U)>

    <U> ::= <Map(T, U)>[<T>, default=<U>]
    \alt <Tuple(U, T)>[0] | <Tuple(T, U)>[1]
    \alt \text{input of type }U
    \end{grammar}
    \end{minipage}

    \caption{The core grammar used to synthesize the state transition and query functions.}
    \label{fig:grammar_core}
\end{figure}

The synthesized components of the state transition, query, and equivalence functions all use a common core grammar. Similar to past program synthesis work, we generate the grammar in Figure~\ref{fig:grammar_core} based on the type constraints of supported operations and bound it by an iteratively increased depth. In addition, since Boolean inputs will likely be used to branch, we automatically introduce top level conditionals to the grammar. Recall that we are synthesizing a function $f'(o)$ that returns a lattice value to be passed into $merge'$. Therefore, even though some operations in this grammar are not idempotent or commutative, the overall state transition function $st'$ remains associative, commutative and idempotent by construction. The semantics of the operations in our language are largely standard, and we lower the operations directly to the corresponding logic in the SMT solver when possible.

Finally, we synthesize the initial state using a shallow grammar of constructors and relevant constants for each type. We include small integer literals, Boolean constants, and empty instances of sets and maps. In cases in which $\bot$ is defined, the initial state is often synthesized to just be the bottom value of the lattice, but occasionally we want the synthesizer to pick an alternate value to handle queries in the initial state. For example, when synthesizing a Boolean register where concurrent enables are ordered after disables, the natural lattice to represent the flag's state is a \texttt{LexicalPair<ClockInt, OrBool>} with $\bot = (0, false)$, but we need the initial state to be $(0, true)$ if the sequential data type starts in a enabled state. By synthesizing this value instead of fixing it to $\bot$, we can synthesize CRDT designs over semilattices which do not define bottom, or where the initial state starts higher in the semilattice order.

\subsubsection{Synthesizing Non-Idempotent Operations}
So far, the state transitions we can synthesize are always idempotent, which is not a requirement of CRDTs in general and prevents us from synthesizing designs such as counters. To resolve this limitation, we use a common trick in replicated distributed systems and selectively ensure that certain state can only have a single writer via the state transition but multiple readers for queries. We introduce \textbf{node IDs}, which are unique integer identifiers for each node in the cluster that can be used as map keys to separate portions of the state that are tied to each node. With this separation of writable state, we can synthesize non-idempotent operations that update portions of the state that only the current node can write.

Users can introduce node IDs to the synthesis pipeline by enabling a flag when the sequential data type has non-idempotent operations. The synthesized component of the state transition, which previously could only read the operation arguments to ensure idempotence and commutativity, is then expanded to have access to the CRDT state as well as the current node ID.
To synthesize CRDT logic that uses node IDs, we add a production rule so that the state transition can read from portions of the state that are owned by the current node, which are the values of maps keyed by a node ID. Similarly, we add a rule that allows the state transition to mutate portions of the state that the current node owns. Finally, we introduce rules to the query grammar for performing reductions over the values of maps keyed by node IDs, which makes it possible to combine the state of each node into a global response to queries. We detail these additional grammar elements in Figure~\ref{fig:grammar_with_nid}.

\begin{figure}[h]
    \centering
    \begin{minipage}[t]{.78\textwidth}
    for the state transition:

    $\forall{V}$
    \begin{grammar}
    <V> ::= <Map(NodeID,V)>[currentNodeID, default=<V>]

    <Map(NodeID,V)> ::= <Map(NodeID,V)> $\sqcup$ $\{$currentNodeID: <V>$\}$
    \end{grammar}

    \hfill

    for queries:
    \begin{grammar}
    <Int> ::= reduce(values(<Map(NodeID,Int)>), $\lambda{a}.\lambda{b}.a + b$, $0$)

    <Bool> ::= reduce(values(<Map(NodeID,Bool)>), $\lambda{a}.\lambda{b}.a \lor b$, $false$)
    \alt reduce(values(<Map(NodeID,Bool)>), $\lambda{a}.\lambda{b}.a \land b$, $true$)
    \end{grammar}
    \end{minipage}

    \caption{The additional production rules required to support non-idempotent operations.}
    \label{fig:grammar_with_nid}
\end{figure}

Although these changes to the construction of the state transition may allow it to be non-idempotent (and potentially non-commutative), the synthesized CRDT remains convergent because the only requirement for state-based CRDTs is that the merge function agrees with the state transition. Because our state transition still performs a lattice join with the previous state at the top level, and the non-idempotence/commutative is restricted to disjoint portions of the state owned by each node in the cluster, the merge function remains correct since a node can never receive \emph{new} information from other nodes about the portions of state it owns.

\subsubsection{Pruning Grammars with Specialized Types}
While shallow instantiations of these grammars are sufficient to synthesize simple CRDTs, such as grow-only sets, they quickly grow to infeasible sizes when the state structure involves a larger number of nested data structures. Much of the grammar expansion comes from a conflation of types that can have distinct semantic meanings, resulting in production rules like arithmetic and comparison operations being unnecessarily introduced.

To resolve this, we introduce \emph{specialized} integer types, which represent distinct interpretations of integer values. In our system, we have \texttt{OpaqueInt}, which represents an abstract value that does not support arithmetic, \texttt{ClockInt}, which represents a positive timestamp that only supports comparison operations, and \texttt{EnumInt}, which represents values that only support equality. Users can then annotate the functions in their sequential data types to mark which types in the state and operation/query parameters conform to these specialized alternatives. By using distinct types for integer inputs, we can avoid searching expressions that, for example, try to compare timestamps with opaque values. We introduce new grammar rules for these types in Figure~\ref{fig:grammar_with_specialized_ints}. These types are also added to the state grammar, but for brevity we omit the changes here.

\begin{figure}[h]
    \centering
    \begin{minipage}[t]{.8\textwidth}
    $\forall{T, U}$
    \begin{grammar}
    <bool> ::= <opaque> $>$ <opaque> | <opaque> $\geq$ <opaque> | <opaque> $=$ <opaque>
    \alt <clock> $>$ <clock> | <clock> $\geq$ <clock> | <clock> $=$ <clock> | <enum> $=$ <enum>

    <clock> ::= 0

    <enum> ::= 0 | 1 | constants in the sequential source

    <U> ::= reduce(values(<Map(T,U)>), $\lambda{a}.\lambda{b}.a \sqcup b$, $\bot$)
    \end{grammar}
    \end{minipage}

    \caption{The production rules for specialized integer types and semilattice reductions.}
    \label{fig:grammar_with_specialized_ints}
\end{figure}

With the grammars defined for all three functions, we can apply a syntax-guided synthesis algorithm to explore the space of CRDT implementations and use the bounded history verification conditions to automatically verify candidates using an SMT solver. The bounds used in this phase start at very small values but are incrementally increased based on feedback from later phases of the synthesis algorithm, which we discuss in further detail in Section~\ref{sec:synth_e2e}.

\subsubsection{Invariant Synthesis for Unbounded Verification} \label{sec:synth_unbounded}
After the first synthesis phase produces a CRDT design that passes bounded-history verification, we must synthesize additional invariants to check the CRDT against the unbounded verification conditions. We must re-synthesize the equivalence function with the CRDT state invariant included, since the unbounded conditions depend on the invariant to exclude unreachable CRDT states. In addition, we synthesize the $orderWithState$ function so that the unbounded conditions can reason about operation orderings.

The CRDT state invariant only has access to the CRDT state, which helps reduce the size of the grammar generated. We seed the invariant with an explicit condition that checks if the state is valid according to the relevant semilattice definitions. Each semilattice in our state grammar comes with logic for checking validity, such as that the integer values for clocks are at least zero. By automatically including these checks, we further reduce the burden on the synthesizer to discover properties needed for the inductive proof. The rest of the invariant is synthesized using the same type-based grammar as the other functions. Note that we do not need to synthesize the relation component of equivalence, since that was already synthesized in the bounded-history phase.

Synthesizing $orderWithState$ is a bit more complex. Since the role of this function is to determine whether an operation is in-order while only having access to the CRDT state, this function often needs to combine information from large portions of the state rather than just manipulating data associated with specific keys. For example, when synthesizing a CRDT that uses clocks to order operations, $orderWithState$ will need to check that the timestamp of the given operation is greater than all existing timestamps in the state. But it is challenging for syntax-guided synthesis engines to reason about arbitrary reductions, so we must reduce the complexity of the grammar.

We tackle this by noting that reductions (such as collecting the highest timestamp) use the semilattice join of the type being accumulated. This has some intuitive backing as well, since comparing with the semilattice order against multiple values is equivalent to a single comparison against the semilattice join over those values. Based on this observation, we add a rule in Figure~\ref{fig:grammar_with_specialized_ints} to compute reductions using the lattice join for all relevant lattice values in the state. Note that we support reductions over map values, but not sets because their elements may not be semilattices.

With these additional production rules, we can synthesize an appropriate $orderWithState$ for the candidate CRDT. With the invariant grammars configured and the existing $st'$ and $query'$ functions from the previous phase, we return to the synthesis engine with the unbounded verification conditions. At this point, we are verifying all scenarios the CRDT is expected to correctly handle, so if we successfully synthesize the invariants we have a provably correct CRDT design!

\subsection{End-to-End Synthesis Algorithm} \label{sec:synth_e2e}
Now that we have the search space for state structures and runtime logic defined, we can synthesize the entire CRDT from scratch by simultaneously exploring both spaces. In our end-to-end algorithm, we apply multiple logic synthesis phases and verification modes to create provably correct CRDTs while also pruning the program space early in the synthesis algorithm.

\begin{algorithm}[h]
    \Function{search($ref, opOrder$)}{
        \For{$depth \gets (2..\infty)$}{
            \For{$s \gets semilatticeCompositions(depth)$}{
                $historyBound \gets 2$

                $p2Depth \gets depth$

                \Loop{
                    $p1Synth \gets synthBoundedHistory(ref, s, opOrder, depth, historyBound)$

                    \lIf{$p1Synth = \text{unsat}$}{
                        \Break
                    }

                    \BlankLine

                    $p2Synth \gets synthUnbounded(ref, s, opOrder, p2Depth, p1Synth)$

                    \eIf{$p2Synth = \text{unsat}$}{
                        $historyBound \gets historyBound + 1$

                        $p2Depth \gets p2Depth + 1$
                    }{
                        \Return{$p2Synth$}
                    }
                }
            }
        }
        \BlankLine
        \BlankLine
    }

    \caption{The end-to-end algorithm for synthesizing a CRDT from scratch.}
    \label{alg:e2e_algo}
\end{algorithm}

At the top level of the algorithm, we iterate over candidate state structures generated from the grammar of semilattice compositions. For each of these, we then generate the appropriate runtime logic grammars and perform synthesis with the bounded-history verification conditions (with an initial bound of 2). If we fail to synthesize, we can eliminate the candidate state structure from consideration, since there is no synthesizable logic even when the verification is relaxed.

If we successfully synthesize, we can move on to synthesizing the additional invariants for unbounded history verification. We combine the synthesized code from the previous phase with new grammars for the extensions to equivalence and the $orderWithState$ function, and call out to the synthesis engine again. If we fail to synthesize at this point, it means that either the bounded-history phase returned a buggy implementation or the grammar for invariants was too small. To address this, we return to the bounded-history phase and increase the history bound as well as the grammar depth for invariants. If we successfully synthesize, we have a provably correct CRDT that we can return to the user. We summarize this algorithm in Algorithm~\ref{alg:e2e_algo}.

\section{Implementation} \label{implementation}
We implement our synthesis system using an extended version of the framework in Casper \cite{casper}, which allows us to automatically extract sequential data types written in C, C++, and other languages by first compiling them to LLVM and analyzing the IR to generate the equivalent SMT logic. Our implementation also includes wrappers around the Rosette synthesis engine \cite{rosette} and CVC5 theorem prover \cite{cvc5}, which we use to perform synthesis and unbounded verification.

\subsection{Supported Language Features}
To synthesize a CRDT, our algorithm must first extract the semantics of the sequential data type provided by the user. To ensure that the logic implemented by the user can be accurately translated into the SMT logic used for verification, we define a space of programs that can be safely handled. Our system can handle basic LLVM operations, branches, integer/Boolean primitives, and list/set/map data structures.

Our analysis can accurately handle primitive types such as integers and Booleans, along with the corresponding arithmetic and logical operations on them. In addition, we provide a set of APIs for lists, sets, and maps that users can build on in their sequential data type. Our analysis automatically recognizes uses of these specialized APIs and lowers them to the corresponding SMT theory. Our framework offers a modular approach to defining the semantics of these types, so it is straightforward to add support for richer data structures such as stacks.

In addition to analyzing the types and operations on them, our framework can extract branches found in the LLVM IR to conditionals in the generated SMT logic. Our system generates separate specifications of each basic block found in a function, and links them together to define the function as a whole. This approach allows us to handle nested conditionals and early returns without needing additional logic for these cases. In addition to branches, our analysis also handles user-defined functions by inlining them into the top-level function that is lifted.

\subsection{Bounded Data Structure Verification}
When synthesizing with Rosette, we face a limitation that the size of the symbolic state must be a constant, which means that we cannot define verification conditions that operate over unbounded data structures such as lists or sets. To address this limitation, we bound the size of these data structures to a fixed size while performing synthesis. After Rosette returns us a successfully synthesized CRDT, we then pass the result to CVC5, which can perform verification with unbounded data structures when a theory is defined for their behavior.

CVC5 natively supports a theory of sets, and we provide our own set of axioms that define tuples. When maps---which have not yet been modeled in CVC5---are involved in the synthesized CRDT, we fall back to using Rosette for verification with a large bound for the data structures. We hope to improve this in future work by providing a set of complete axioms that enable the solver to reason about unbounded map instances. In the meantime, the bounds we use for the fallback are sufficiently large to consistently produce correct synthesized results.

\subsection{Parallel State Structure Exploration}
Both Rosette, which uses Z3 under the hood, and CVC5 are single-threaded. If we were to naively implement the end-to-end algorithm, we would underutilize the multi-core capabilities of modern systems. But because we control the search of CRDT state structures, and the logic synthesis for each structure candidate is independent of the others, we can drastically speed up the synthesis algorithm by parallelizing across state structures.

Our system allows users to configure the number of state structures to synthesize logic for in parallel. Based on this parameter, we then instantiate a thread pool and spawn the logic synthesis algorithm for candidate structures on free threads. When a thread returns a successfully synthesized candidate, we shut down all other jobs and return the result. If a thread reports that no synthesized logic exists for the state structure, we launch synthesis for the next candidate structure. By exploring more state structures and avoiding situations where synthesis is blocked on a state candidate that is particularly difficult to synthesize logic for, this technique drastically improves the end-to-end synthesis performance.

\section{Evaluation} \label{eval}
In our evaluation, we explore the capability of our system to \emph{correctly} and \emph{efficiently} synthesize CRDTs for a variety of sequential data type and operation ordering specifications. We focus on answering the following research questions:

\begin{itemize}
    \item \textbf{RQ1}: Can the system produce practical CRDTs based on specifications sourced from literature on coordination-avoidance?
    \item \textbf{RQ2}: What is the effect of pruning structures with bounded-history verification on the overall synthesis performance?
    \item \textbf{RQ3}: Is the grammar of lattice composition sufficiently rich to produce CRDT designs that differ from the canonical implementations in the literature?
\end{itemize}

\subsection{\textbf{RQ1}: Synthesizing Practical CRDTs}
We begin by evaluating the ability of our synthesis algorithm to produce correct CRDTs from scratch for a variety of user-provided specifications. We sourced several sequential data types and operation orderings, summarized in Table~\ref{tab:crdt_specs}, from existing literature on human-designed CRDTs \cite{shapiro2011comprehensive} and coordination-avoidance \cite{ecros}. For each of the benchmarks, we created a minimal implementation of the sequential type in C based on the specifications provided by the source and encoded the operation ordering using the IR provided by the synthesis system. All benchmarks were conducted on a AMD Ryzen 9 3900X processor with 12C/24T and 48 GB of memory, with our implementation configured to use up to 12 threads. We use LLVM 11 to compile and analyze the sequential types, as well as the latest versions of Rosette (4.1) and CVC5 (1.0.0).

\begin{table}[h]
    \centering
    \begin{tabular}{p{3.7cm}|c|c|c|c}
        Benchmark & Source & Specification Size & Timestamps & Non-Idempotent \\
        \hline
        Grow-Only Counter & Shapiro & 21 LoC &  & \checkmark \\
        General Counter & Shapiro & 20 LoC &  & \checkmark \\
        Enable-Wins Flag & De Porre & 21 LoC & \checkmark &  \\
        Disable-Wins Flag & De Porre & 21 LoC & \checkmark &  \\
        Last-Writer-Wins Register & Shapiro & 16 LoC & \checkmark &  \\
        Grow-Only Set & Shapiro & 24 LoC &  &  \\
        Two-Phase Set & Shapiro & 24 LoC &  &  \\
        Add-Wins Set & De Porre & 24 LoC & \checkmark &  \\
        Remove-Wins Set & De Porre & 24 LoC & \checkmark &
    \end{tabular}
    \caption{The set of CRDT specifications used to evaluate our synthesis algorithm.}
    \label{tab:crdt_specs}
\end{table}

Our overall approach is designed to require minimal user intervention to produce a practical CRDT. As a proxy for this goal, we measured the amount of code required for a user to specify both the sequential data type and the operation ordering that specifies the synthesized CRDT. For all our benchmarks, both of these components can be declared within 25 lines of C (for the data type) and Python (for the operation ordering). In addition, most of the code is for the sequential data type, which a developer using our system will likely already have. The operation orderings, which are specific to our synthesis system, could all be defined in 4 LoC or less of integer comparisons.

When run with our collection of benchmarks, our synthesis algorithm is able to successfully generate designs that conform to all of the specifications, and it identifies the inductive invariants necessary to prove correctness of each CRDT over unbounded executions. We list the time required to synthesize each CRDT and the state structure of the synthesized result in Table~\ref{tab:synth_times}. Simpler CRDTs, such as the Grow-Only/Two-Phase Set and LWW-Register, can be synthesized by our system in a matter of seconds. More complex CRDTs, especially those that use timestamps to order operations such as the Add/Remove-Wins Set, can take on the order of 10s of minutes to synthesize. These performance measurements indicate that the composition of multiple synthesis phases allows for many types of CRDTs to be synthesized in a reasonable amount of time.

\begin{table}[h]
    \centering
    \begin{tabular}{p{2.55cm}|p{2.15cm}|p{2.15cm}|p{5.6cm}}
        Benchmark & Synthesis Time (default) & Synthesis Time (no pruning) & Synthesized State Type \\
        \hline
        Grow-Only Counter & 54s & 37s & \footnotesize{\texttt{Map<NodeID, MaxInt<Int{>}>}} \\
        \hline
        General Counter & 11m 54s & 16m 3s & \footnotesize{\texttt{FreeTuple<Map<NodeID, MaxInt<Int{>}>,}}

        \footnotesize{\texttt{  Map<NodeID, MaxInt<Int{>}{>}>}} \\
        \hline
        Enable-Wins Flag & 59s & 3m 1s & \footnotesize{\texttt{LexicalProduct<MaxInt<ClockInt>, OrBool>}} \\
        \hline
        Disable-Wins Flag & 1m 7s & 2m 40s & \footnotesize{\texttt{LexicalProduct<MaxInt<ClockInt>, OrBool>}} \\
        \hline
        Last-Writer-Wins Register & 35s & 44s & \footnotesize{\texttt{LexicalProduct<MaxInt<ClockInt>,}}

        \footnotesize{\texttt{  MaxInt<Opaque{>}>}}\\
        \hline
        Grow-Only Set & 14s & 16s & \footnotesize{\texttt{Set<Opaque>}} \\
        \hline
        Two-Phase Set & 47s & 1m 7s & \footnotesize{\texttt{Map<Opaque, OrBool>}} \\
        \hline
        Add-Wins Set & 22m 58s & 1hr 57m 4s & \footnotesize{\texttt{FreeTuple<Map<Opaque, MaxInt<ClockInt{>}>,}}

        \footnotesize{\texttt{  Map<Opaque, MaxInt<ClockInt{>}{>}>}} \\
        \hline
        Remove-Wins Set & 21m 5s & 1hr 50m 19s & \footnotesize{\texttt{FreeTuple<Map<Opaque, MaxInt<ClockInt{>}>,}}

        \footnotesize{\texttt{  Map<Opaque, MaxInt<ClockInt{>}{>}>}}
    \end{tabular}
    \caption{The performance of synthesizing CRDTs for the benchmark specifications with our algorithm.}
    \label{tab:synth_times}
\end{table}

Our synthesis results also show the algorithm discovering a variety of CRDT design techniques without any baked-in knowledge of CRDTs, such as using timestamps to guard data and storing the effects of conflicting operations in separate parts of the state. For example, our system synthesizes the CRDT on the left in Figure~\ref{fig:set_and_counter_crdts} for the Add-Wins Set, which supports repeated insertions and removals by using timestamps to have Adds only shadow Removes when they are concurrent. Similarly, on the right side of Fig~\ref{fig:set_and_counter_crdts}, our system is able to discover how to use node IDs to handle non-idempotent operations in a counter CRDT, using multiple reductions in the query to take the difference of the accumulated increments and decrements.

\begin{figure}[h]
    \centering
    \begin{minipage}{.47\textwidth}
      \begin{algorithm}[H]
        \CRDT{AddWinsSet}{
        \InitialState{$(\{\}, \{\})$}
        \BlankLine
        \Operation{$((s_1, s_2), add, value, time)$}{
          \eIf{$add = 1$}{
            \Return{$((s_1 \cup \{value: time\}), s_2)$}
          }{
            \Return{$(s_1, (s_2 \cup \{value: time\}))$}
          }
        }
        \BlankLine
        \Query{$((s_1, s_2), v)$}{
          $t_1 = s_1[v, default=0]$

          $t_2 = s_2[v, default=0]$

          \Return{$t_1 \geq t_2 \land t_1 > 0$}
        }
        }
      \end{algorithm}
    \end{minipage}
    \begin{minipage}{.52\textwidth}
      \begin{algorithm}[H]
        \CRDT{GeneralCounter}{
        \InitialState{$(\{\}, \{\})$}
        \BlankLine
        \Operation{$((s_1, s_2), inc, nodeID)$}{
          $cur_1 = s_1[nodeID, default=0]$

          $cur_2 = s_2[nodeID, default=0]$

          \eIf{$inc = 1$}{
            \Return{$((s_1 \cup \{nodeID: cur_1 + 1\}), s_2)$}
          }{
            \Return{$(s_1, s_2 \cup \{nodeID: cur_2 + 1\})$}
          }
        }
        \BlankLine
        \Query{$((s_1, s_2))$}{
          $r_1 = reduce(values(s_1), \lambda{a}.\lambda{b}.a + b, 0)$

          $r_2 = reduce(values(s_2), \lambda{a}.\lambda{b}.a + b, 0)$

          \Return{$r_1 - r_2$}
        }
        }
      \end{algorithm}
    \end{minipage}
    \caption{The Add-Wins Set and General Counter CRDTs our synthesis algorithm is able to produce.}
    \label{fig:set_and_counter_crdts}
\end{figure}

Although our work does not focus on the runtime performance, all of our CRDTs have comparable theoretical performance to human designs in existing literature. In the case of the Two-Phase Set benchmark, our synthesis algorithm comes up with a more efficient state encoding (which we discuss in Section~\ref{sec:alt_crdt}) that simplifies the state to a single integer to Boolean map rather than the typical two integer sets. Overall, our synthesis algorithm is able to produce practical, provably correct CRDTs for the variety of specifications in our benchmarks.

\subsection{\textbf{RQ2}: Search Space Pruning}
A key contribution in our runtime synthesis algorithm is the use of two SMT encodings of the correctness conditions: one that can quickly verify CRDT candidates with checks for bounded executions, and one that can prove unbounded correctness but requires the synthesizer to identify additional invariants. In this section, we explore the performance of this two-phase approach.

First, we can compare the time that our end-to-end algorithm takes to find CRDTs for each of the benchmarks with and without the bounded-history phase as a pruning optimization. In Table~\ref{tab:synth_times}, we list the synthesis times without the bounded-history phase under the "no pruning" column. Other than the Grow-Only Counter, which synthesizes under a minute in both modes since the CRDT design is relatively simple, all the benchmarks synthesize faster with the bounded-history phase. The biggest performance improvements come for the CRDTs with the most complex state structures: the General Counter and Add/Remove-Wins Set. In the case of the Sets, we see up to a 5x speedup by using bounded-history to prune data structures.

\begin{wrapfigure}{r}{0.5\textwidth}
    \pgfplotstableread[col sep=comma,]{add-wins-bounded-history.csv}\dataBounded
    \pgfplotstableread[col sep=comma,]{add-wins-unbounded.csv}\dataUnbounded

    \centering
    \pgfplotsset{
        every non boxed y axis/.style={}
    }
    \hspace*{-0.2\textwidth}
    \begin{tikzpicture}
    \begin{groupplot}[
        group style={
            group size=2 by 1,
            yticklabels at=edge bottom,
            horizontal sep=0pt
        },
        x filter/.code={\pgfmathparse{#1/60}\pgfmathresult},
        y filter/.code={\pgfmathparse{#1*100}\pgfmathresult},
        height=5cm,
        ymin=0, ymax=105
    ]

    \nextgroupplot[xmin=0,xmax=20,
                   xtick={0,5,10,15},
                   axis y line=left,
                   width=0.3\textwidth,
                   xlabel={Synthesis Time (minutes)},
                   x label style={at={(axis description cs:1,-0.3)},anchor=south},
                   ylabel={Candidates Evaluated},
                   yticklabel={\pgfmathprintnumber\tick\,\%}]
    \addplot [blue] table [x={time}, y={percent}]{\dataBounded};
    \addplot [red] table [x={time}, y={percent}]{\dataUnbounded};

    \nextgroupplot[xmin=50,xmax=70,
                   xtick={55,60,65,70},
                   axis y line=right,
                   axis x discontinuity=crunch,
                   width=0.3\textwidth,
                   yticklabels={,,},
                   legend pos={south east}]
    \addplot [blue] table [x={time}, y={percent}]{\dataBounded};
    \addlegendentry{\footnotesize{bounded history}}
    \addplot [red] table [x={time}, y={percent}]{\dataUnbounded};
    \addlegendentry{\footnotesize{direct unbounded}}
    \end{groupplot}
    \end{tikzpicture}

    \caption{The distribution of time taken to evaluate candidates for the Add-Wins Set benchmark.}
    \label{fig:bounded_vs_unbounded_plot}
\end{wrapfigure}

For a more nuanced exploration of \emph{why} we see these speedups, we collect the time it takes each synthesis algorithm to either correctly synthesize or prune out each candidate data structure for the Add-Wins Set benchmark. We compare the two algorithms in Figure~\ref{fig:bounded_vs_unbounded_plot}, where we plot a distribution of the percent of candidates (out of 86 total) that can be evaluated within a given amount of time. With bounded history, all candidate structures can be processed in under 15 minutes, allowing the end-to-end algorithm to quickly reach the state candidate that yields a correct CRDT. Without pruning, many state candidates take up to 20 minutes to be evaluated and there is a long tail of candidates that take up to an hour. When the CRDT must have a complex state to support the specified semantics, these stragglers have a significant toll on synthesis performance since they block exploration of the program space.

\subsection{\textbf{RQ3}: Alternative CRDT Synthesis} \label{sec:alt_crdt}
Finally, we evaluate the richness of the space of CRDTs our synthesis algorithm explores. In particular, we are interested in the ability of our synthesis algorithm to produce \emph{multiple} CRDT implementations for a \emph{single} specification. Since our combination of a sequential type and operation ordering uniquely defines the user-observable behavior of a CRDT, any alternate designs will be functionally equivalent but may have different memory utilization and performance characteristics.

\begin{wrapfigure}{r}{.42\textwidth}
    \centering
    \begin{minipage}{.42\textwidth}
      \begin{algorithm}[H]
        \CRDT{TwoPhaseSet}{
        \InitialState{$\{\}$}
        \BlankLine
        \Operation{$(s, add, value)$}{
          \eIf{$add = 1$}{
            \Return{$s_1 \cup \{value: false\}$}
          }{
            \Return{$s_1 \cup \{value: true\}$}
          }
        }
        \BlankLine
        \Query{$(s, v)$}{
          \Return{$\lnot{s[v, default=true]}$}
        }
        }
      \end{algorithm}
    \end{minipage}
    \caption{The novel map-based CRDT that is synthesized for the two-phase set benchmark.}
    \label{fig:map_2p_set}
\end{wrapfigure}

In our exploration of alternate CRDT designs, we focus on the Two-Phase Set, which has moderately complex semantics since its execution has multiple phases: allow inserts, then removes, but not inserts again. When we perform synthesis, the first CRDT that is generated is surprisingly \textbf{not} the 2P-Set from existing CRDT literature, but instead (to our knowledge) a novel design that uses a map to capture the phase of each element. If we continue searching, the algorithm also emits the classic 2P-Set, but this arrives later since its state structure is larger.

We list the new design in Figure~\ref{fig:map_2p_set}. There are several clever tricks that the synthesizer comes up with to match the specification while using a simpler state. First, the synthesizer realizes that the behavior of a two-phase set "saturating" after removing an element matches how an \texttt{OrBool} saturates when it becomes true. Next, it discovers that by using a mapping from keys to these values, it can maintain a separate saturating value for each key in the set.

But this still leaves a challenging situation for the initial state. Because we use the saturated $true$ value to represent the element being removed, that means we have to set the value for a key to $false$ when it is inserted the first time. But since $\bot = false$ for an \texttt{OrBool}, that would leave us with no additional state. This is where the final trick is discovered by the synthesizer: to query the map with a default value of $true$. This effectively creates a third state for when the key is not even in the map. By automatically discovering this combination of CRDT design tricks, our synthesis algorithm is able to produce this novel encoding of a two-phase set.

Our synthesis algorithm also produces alternate designs for many other benchmarks, such as using pairs of clocks instead of a \texttt{LexicalProduct} for the enable/disable-wins flag benchmarks. The presence of such alternatives paves the way for future work where we synthesize not only a \emph{correct} CRDT, but a \emph{performant} one according to a cost model that can compare CRDT candidates. Furthermore, the pool of alternative designs may be useful for incrementally re-synthesizing CRDTs as the sequential data type is updated, something we hope to explore in the future.

\input{relwork_notes}

\section{Conclusion}
The future of computing is distributed, so it is important to reduce the complexity of developing correct, efficient distributed programs. We believe that verified lifting can be a useful tool towards this goal, by automating much of the process of converting familiar sequential code into scalable distributed code.
In this paper, we presented a first step in this direction with a system that automatically synthesizes CRDT designs from existing sequential data type implementations, requiring only simple annotations that are are easy for developers to reason about.

We formalized the definition of \emph{correctness} for CRDTs in terms of a sequential data type by introducing \emph{operation orderings}, which allow users to define how the CRDT should handle conflicting non-commutative operations. To automate the verification process, we developed SMT encodings of this correctness definition that can be used to check CRDT candidates with a solver. Finally, we explored how compositions of semilattices can be naturally used as the state of a CRDT, and defined grammars for runtime logic and the invariants that enable unbounded verification of correctness. Our end-to-end algorithm efficiently synthesizes CRDTs for a variety of scenarios and produces novel alternatives to human-designed CRDTs. With our system, we hope to further unlock the power of distributed systems by making it possible for any developer to automatically replicate their existing data types by synthesizing provably equivalent CRDTs.

\section{Abstract}
We are able to synthesize CRDTs from sequential code using verified lifting!

\section{Introduction}
We are able to synthesize CRDTs from sequential code using verified lifting!

(2 pages)

\subsection{Motivating Example}
(figure of distributed execution of shopping cart)

Shopping carts are an important real-world example that can be solved using a two-phase set CRDT.

(4-5 pages)

\section{CRDT Verification}
\subsection{Object Execution Model}
We prove that verifying linear sequences is sufficient for correctness.

(7 pages)

\subsection{State Equivalence}
Introduce the idea of an equivalence function and that we can encode correctness conditions for this that are verifiable by SMT. Core inductive proof of verifying arbitrary sequences of operators.

(9 pages)

\section{Semantics Relaxation}
(figure showing transformation of sequences)

Introduce user-defined ordering and show we can synthesize different CRDTs based on this. Argue that this is sound because CRDTs are commutative.

(10 pages)

\subsection{Verification with Bounded History}
Motivate that we want a cheap way of verifying that doesn't involve additional invariants. "What is an easy way we can integrate this into the existing proof framework without introducing more functions".

(11 pages)

\subsection{History Invariant Synthesis}
(figure showing states of 2P-Set to show when supportedCommand is true/false)

Show that the verification with bounded synthesis is sound.

(12 pages)

\subsection{Orderings with Time}
Talk about the timestamp scenarios that aren't fully commutative and require partial orders. How we use Lamport timestamps to solve these.

(14 pages)

\subsection{Interactive Ordering Creation?}
It is common in CRDTs for application developers to choose how to break ties in a way that makes sense for their specific application. We developed an interactive interface for developers to input this tie-breaking information to enable us to synthesize CRDTs from non-commutative code.

\section{CRDT Synthesis}
\subsection{Data Structure Exploration}
(pseudocode for enumeration algorithm)

How we pick lattices.

(16 pages)

\subsection{Runtime Synthesis}
(figure of IR for synthesis)

How we generate the grammar. How we make the grammar constrained to make operations commutative.

(18 pages)

\subsection{End to End Synthesis Algorithm}
How we use bounded verification to prune options and get reasonable runtimes.

(19 pages)

\section{Evaluation}
Explanation that the set of CRDTs we are able to synthesize is a sufficient set of examples. (same as ECRO paper)
Walk through two phase set and LWW set synthesis examples. Show execution of synthesizing them and time it takes to synthesize.

(21-22 pages)

\section{Related Work}
ECROs, Static Analysis Approaches, Indigo.

(24 pages ?)

Future work: collaborative editors, string and tree based structures.
\section{Conclusion}
We were able to synthesize CRDTs from sequential code using verified lifting!

(24-25 pages)

\section{References}
\end{document}
\section{Related Work}
\subsection{Creating Replicated Objects from Sequential Specifications}

There are a few lines of work that focus narrowly on the same problem
we take aim at here: taking specifications of sequential datatypes and
automatically creating equivalent replicated types. Where these projects differ
from ours is primarily in our use of program synthesis: to our knowledge we
are the first to utilize a search-based synthesis approach to
generate state representations and runtime logic.
Our other differences focus on how we chose to resolve conflicting
operations, and our approach of searching semilattice compositions for the CRDT state.

Gallifrey \cite{gallifrey}, Indigo \cite{indigo}, and ECROs {\cite{ecros}} focus on not just specifying replicated
data types, but also in ensuring that applications which use them do
not see inconsistent state---much as our work verifies correctness
with respect to queries. Beyond the use of program
synthesis in our work, the main point of divergence is in their use of
preconditions and postconditions as a verification tool
to exactly match the behavior of synchronous objects.  Other work also uses this pre/post-condition approach \cite{secros} or shares the goal of matching sequential behavior~\cite{static-local-coordination-avoidance}.
Our goal is not to exactly match sequential behavior; we let
programmers tweak the semantics of synchronous
objects with simple ordering constraints on conflicting operations.  This allows us to lift all
specified operations into CRDTs, rather than limiting ourselves to operations which already commute (as in Gallifrey) or resorting to explicit synchronization or deferred
re-execution for conflicting events (as in Indigo and ECROs).

The MRDT line of work \cite{mrdts, certified-mrdts} starts with a similar premise to
ours---synthesizing replicated datatypes from annotated sequential
specifications---but takes a radically different approach.
Our largest differences center around their runtime
system, which is based on a Git-inspired log of versioned
data structures, and in their mode of annotation, which centers around
abstraction and concretization functions. In contrast, our sorting-based annotations are simpler, and our generated CRDTs require only a basic gossip protocol at run-time. Additionally, their
synthesized merge functions use a rule-based approach to construction,
whereas our work takes the search-based approach most commonly associated
with synthesis literature.

\subsection{Program Synthesis and Verified Lifting}
The synthesis approach taken in this work is directly inspired by
verified lifting \cite{verifiedlifting}, the approach at the heart of work such as Domino \cite{domino}, Casper \cite{casper}, and Dexter \cite{dexter}. With verified lifting, the correctness conditions for synthesizing code in a particular DSL are derived from \emph{existing implementations} in standard languages such as C/C++. Our approach expands on this tradition
primarily by our choice to synthesize entire data
types, instead of just function implementations. This involves more complex
verification conditions that check \emph{behavioral equivalence} between the input
code and the synthesized CRDT, rather than just checking equality of function
outputs.
Furthermore, our introduction of ordering constraints goes beyond
verifying strict equivalence to allow user-supplied adjustments
that enable even sequential data types with conflicting operations to be
lifted to CRDTs.

Few previous systems have attempted to directly apply search-based
program synthesis to the space of replication.  Two
that stand out are Hamsaz~\cite{hamsaz} and Hampa~\cite{hampa}.  Hamsaz uses
programmer-provided invariants to synthesize custom consistency
protocols for the replication of shared data structures.  While its
analysis component is reminiscent of other work, such as Quelea,
and the Indigo line \cite{quelea, indigo, ecros, indigo-ipa}, its novel synthesis
component is of particular interest to this work. Like our work,
Hamsaz uses an SMT encoding of the programmer-specified
semantics to search through potential replication strategies. Hampa \cite{hampa}, a
similar work from the same research group, adds recency to the mix. However, both of these solutions are focused on identifying efficient coordination protocols, rather than \emph{eliminating} coordination altogether. The CRDTs synthesized by our algorithm can be replicated without needing any coordination within the cluster.

\subsection{Making Replicated Objects Easier to Work With}

Several papers attempt to make the process of programming against weak
consistency tractable. Some do so by exposing
weakly-consistent replicated objects with approachable semantics;
indeed, the original CRDT work fits in this vein \cite{shapiro2011comprehensive}.  Other
such approaches include the CloudTypes work from Microsoft \cite{cloud-types} or work on
allowing an application to safely mix consistency levels via MixT \cite{mixt},
Disciplined Inconsistency \cite{disciplined-inconsistency}, CScript \cite{cscript}, or Red-Blue consistency \cite{redblue}.  Some work automatically chooses consistency levels for the programmer, driving the choice of mixed consistency via program invariants rather than explicit consistency annotations \cite{redblue-automating, quelea, kaki-2018, observable-atomic-consisency-2018, observable-atomic-consisency-2020}.  All work on mixing consistency shares the belief that programmers require stronger consistency for some operations; in contrast, we let users introduce semantic adjustments that eliminate the need for strong consistency.

Other work focuses on ensuring that application executions are
convergent despite the inherent non-determinism of concurrency and
weakly-consistent replication.  These include a long line of work from
Berkeley \cite{bloom,bloomL,alvaro2010dedalus,blazes,conway2014edelweiss}, and the Gallifrey, LASP,
and LVars languages \cite{gallifrey,lasp,lvars}.  While we believe
that whole-language approaches are valuable in this space,
the CRDT literature typically does not analyze
programs beyond the boundaries of the CRDT implementation.
A more sophisticated treatment of CRDT convergence which factors in application semantics is outside the scope of this work.

\subsection{Verifying Replicated Data Types}

Many previous systems have also provided verification systems for
manually-implemented CRDTs, checking both convergence properties and
correctness with respect to a specification.  Several of these require manual proof effort \cite{replicated-datatype-verification-liquid-haskell, crdtVerif, specifying-crdts}, which make them infeasible for program synthesis approaches that require rapid verification of a large number of candidates.

Of particular note is recent work which explores automated verification of convergence properties via an SMT encoding \cite{cav19crdtverification}, which is especially relevant because we also use SMT to automatically verify CRDT candidates. However, our work differs from this research in \emph{what} is being verified. Because our CRDTs are \emph{convergent by construction}, we do not need to perform any convergence verification. Instead, our verification conditions focus on the \emph{user-observable behavior} of the CRDT, including checking the correctness of queries---something that convergence verification approaches do not include (as queries do not affect convergence).
Others focus on the general question of correct use of weak consistency, and are not specific to CRDTs \cite{cause-im-strong-enough, ralinearizability}.


Saturday timings as always, Registration from 9am followed by practice sessions.
First round of matches 10:30, second 13:30 and 3rd round at 16:30.
Please remember that any player who has not yet provided a completed and SIGNED player registration form will not be allowed to play until that has been done.


We are sorry but listing # 1008349178 is no longer available.
Please check back our Delaware MLS database is updated daily or try Searching all Delaware Properties Here.
ARE YOU A SELLER of Delaware real estate?
We are the Delaware Real Estate Agents YOU want to work with!