5 Technically, this is at least the weakest-precondition of the update for safety. It strengthens any a priori precondition that the developer may have set.

σi -Inv (1)

$$\forall \text{ op}, \sigma, \sigma\_{new}, \left( \begin{array}{c} \sigma \models \mathsf{Pre}\_{\mathsf{op}} \wedge \\ \sigma \models \mathsf{Inv} \wedge \\ \mathsf{[op]}(\sigma) = \sigma\_{new} \end{array} \right) \Rightarrow \qquad \qquad \sigma\_{new} \models \mathsf{Inv} \tag{2}$$

$$\forall \ \sigma, \sigma', \sigma\_{new}, \left( \begin{array}{c} (\sigma, \sigma') \models \mathsf{Pre\_{narga}} \land \\ \sigma \models \mathsf{Inv} \land \\ \sigma' \models \mathsf{Inv} \land \\ \mathsf{[merge]} (\sigma, \sigma') = \sigma\_{new} \end{array} \right) \Rightarrow \qquad \sigma\_{new} \models \ \mathsf{Inv} \tag{3}$$

(σi, σi) -Invconc (4)

$$\forall \text{ } \textsf{op}, \sigma, \sigma', \sigma\_{new}, \left( \begin{array}{c} \sigma \models \textsf{Pre}\_{\textsf{op}} \land\\ (\sigma, \sigma') \models \textsf{Inv}\_{conc} \land\\ \textsf{[op}](\sigma) = \sigma\_{new} \end{array} \right) \Rightarrow \qquad \left( \sigma\_{new}, \sigma' \right) \models \textsf{Inv}\_{conc} \tag{5}$$

$$(\forall \ \sigma, \sigma', \sigma\_{new}, \begin{pmatrix} (\sigma, \sigma') \models \mathsf{Pre\_{narga}} \land \\ (\sigma, \sigma') \models \mathsf{Inv\_{conc}} \land \\ \mathsf{[merge]}(\sigma, \sigma') = \sigma\_{new} \end{pmatrix} \Rightarrow \qquad (\sigma\_{new}, \sigma') \models \mathsf{Inv\_{conc}} \tag{6}$$

**–** Clearly, the initial state of the object must satisfy the global invariant, this is checked by conditions (1) and (4).

The rest of the rules perform a kind of inductive reasoning. Assuming that we start in a state that satisfies the global invariant, we need to check that any state update preserves the validity of said invariant. Importantly, this reasoning is not circular, since the initial state is known by the rule above to be safe.6

**–** Condition (2) checks that each of the operations, when executed starting in a state satisfying its precondition and the invariant, is safe. Notice that we require that the precondition of the operation be satisfied in the starting state. This is the core of the inductive argument alluded to above, all operations – which as we mentioned in Section 3 execute atomically w.r.t. concurrency – preserve the invariant Inv.

Other than the execution of operations, the other source of local state changes is the execution of the merge function in a replica. It is not true in general that for any two given states of an object, the merge should compute a safe state. In particular, it could be the case that the merge function needs a precondition that is stronger than the conjunction of the invariants in the two states to be merged. The following rules deal with these cases.

**–** We require the merge function to be annotated with a precondition strong enough to guarantee that merge will result in a safe state. Generally, this

6 Indeed, the proof of soundness of program logics such as Rely/Guarantee are typically inductive arguments of this nature.

precondition can be obtained by calculating the weakest precondition [9] of merge w.r.t. the desired invariant. Since merge is the only operation that requires two states as input, the precondition of merge has two states. We can then verify that merging two states is safe. This is the purpose of rule (3).

As per the program model of Section 3, any two replicas can exchange their states at any given point of time and trigger the execution of a merge operation. Thus, it must be the case that the precondition of the merge function is enabled at all times between any two replica local states. Since merge is the only point where a local replica can observe the result of concurrent operations in other replicas, we call this a *concurrency invariant* (Invconc). In other words: the *concurrency invariant is part of the global invariant* of the object. This is the main insight that allows us to reduce the proof of the distributed object to checking that both the invariant Inv and the concurrency invariant Invconv are global invariants. In particular, the latter implies the former, but for exposition purposes we shall preserve the invariant Inv in the rules.

As anticipated at the beginning of this section, the reasoning about the concurrency is performed in a completely local manner, by carefully choosing the verification conditions, and it avoids the stability blow-up commonly found in concurrent program logics. The program model, and the verification conditions allow us to effectively reduce the problem of verifying safety of an asynchronous concurrent distributed system, to the modular verification of the global invariant (Inv ∧ Invconc) as pre and post conditions of all operations and merge.

**Proposition 1 (Soundness).** *The proof rules in equations (1)-(6) guarantee that the implementation is safe.*

To conduct an inductive proof of this lemma we need to strengthen the argument to include the set of observed states as given by the semantics of Figure 3.

**Lemma 5 (Strengthening of Soundness).** *Assuming that the equations (1)- (6) hold for an implementation of a replicated object with initial state* Ωi*. For any state* (Ω, S) *reachable from* (Ωi, {σi})*, that is* (Ωi, {σi}) ∗ −→ (Ω, S)*, we have that:*

#### **Corollary 1.** *The soundness proposition (1) is a direct consequence of Lemma 5.*

We remark at this point that there are numerous program logic approaches to proving invariants of shared-memory concurrent programs, with Rely/Guarantee [15] and concurrent separation logic [6] underlying many of them. While these approaches could be adapted to our use case (propagating-state distributed systems), this adaptation is not evident. As an indication of this complexity: one would have to predicate about the different states of the different replicas, restate the invariant to talk about these different versions of the state, encode the non-deterministic behaviour of merge, etc. Instead, we argue that our specialised rules are much simpler, allowing for a purely sequential and modular verification that we can mechanise and automate. This reduction in complexity is the main theoretical contribution of this paper.

#### **4.2 Applying the proof rule**

Let us apply the proof methodology to the auction object. Its invariant is the following conjunction:

Computing the weakest precondition of each update operation, for this invariant is obvious. For instance, as discussed earlier, close auction(w) gets precondition is highest(Bids, w), because of Invariant Item 2 above.

Despite local updates to each replica respecting the invariant Inv, Figure 1 showed that it is susceptible of being violated by merging. This is the case if Bob's \$100 bid in Brussels wins, even though Charles concurrently placed a \$105 bid in Calgary; this occurred because status became CLOSED in Brussels while still ACTIVE in Calgary. The weakest precondition of merge for safety expresses that, if status in either state is CLOSED, the winner should be the bid with the highest amount in both the states. This merge precondition, now called the concurrency invariant, strengthens the global invariant to be safe in concurrent executions.

Let us now consider how this strengthening impacts the local update operations. Since starting the auction doesn't modify any bids, the operation trivially preserves it. Placing a bid might violate Invconc if the auction is concurrently closed in some other replica; conversely, closing the auction could also violate Invconc, if a higher bid is concurrently placed in a remote replica. Thus, the auction object is safe when executed sequentially, but it is unsafe when updates are concurrent. This indicates the specification has a bug, which we now proceed to fix.

#### **4.3 Concurrency Control for Invariant Preservation**

As we discussed earlier, the preconditions of operations and merge are strengthened in order to be sequentially safe. An object must also preserve the concurrency invariant in order to ensure concurrent safety. Violating this indicates the presence of a concurrency bug in the specification. In that case, the operations that fail to preserve the concurrency invariant might need to synchronise. The developer adds the required concurrency control mechanisms as part of the state in our model. The modified state is now composed of the state and the concurrency control mechanism.

Recall that in the auction example, placing bids and closing the auction did not preserve the precondition of merge. This requires strengthening the specification by adding a concurrency control mechanism to restrict these operations. We can enforce them to be strictly sequential, thereby avoiding any concurrency at all. But this will affect the availability of the object.

A concurrency control can be better designed with the workload characteristics in mind. For this particular use case, we know that placing bids are much more frequent operations than closing an auction. Hence we try to formulate a concurrency control like a readers-writer lock. In order to realise this we distribute tokens to each replica. As long as a replica has the token, it can allow placing bids. Closing the auction requires recalling the tokens from all replicas. This ensures that there are no concurrent bids placed and thus a winner can be declared, respecting the invariant. The addition of this concurrency control also updates the Invconc. Clearly, all operations must respect this modification for the specification to be considered safe.

Note that the token model described here restricts availability in order to ensure safety. Adding efficient synchronization is not a problem to be solved only with application specification in hand, it rather requires the knowledge of the application dynamics such as the workload characteristics and is part of our future work.

Figure 6 shows the evolution of the modified auction object with concurrency control. The keys shown are the tokens distributed to each replica. When a replica wants to close the auction, it can request tokens from other replicas. When a replica releases its token, it is indicated by a cross mark on the key. This concurrency control mechanism makes sure that the object is safe during concurrent executions as well. The specification including the concurrency control is given in the extended version[23].

To summarize, all updates (operations and merge) have to respect the global invariant (Inv∧Invconc). If an update violates Inv, the developer must strengthen its precondition. If an update violates Invconc, the developer must add concurrency control mechanisms.

# **5 Case Studies**

This section presents three representative examples of different consistency requirements of several distributed applications. The consensus object is an ex-

Fig. 6: Evolution of state in an auction object with concurrency control

ample of a coordination-free design, illustrating a safe object with just eventual consistency. The next example of a distributed lock shows a design that maintains a total order, illustrating strong consistency. And the final example of courseware shows a mix of concurrent operations and operations with restrained concurrency. This example, similar to our auction example, illustrates applications that might require coordination for some operations to ensure safety.

For each case study, we give an overview of the operational semantics informally. We then discuss how the design preserves the safety conditions discussed in Section 4. We also provide pseudocode for better comprehension.

#### **5.1 Consensus application**

Consensus is required in distributed systems when all replicas have to agree upon a single value. We consider the specification of a consensus object with a fixed number of replicas. We assume that replica failures are solved locally by redundancy or other means, and all replicas participate.

The state consists of a boolean flag indicating the result of consensus, and a boolean array indicating the votes from replicas. Each replica agrees on a proposal by setting its dedicated entry in the boolean array. A replica cannot withdraw its agreement. A replica sets the consensus flag when it sees all entries of the boolean array set.

The consistency between the values of agree flag and the boolean array is ensured by the invariant. The merge function is the disjunction of the individual components. In this case study, we can see that the merge ensures safety without any additional precondition. This means that the object is trivially safe under concurrent executions.

```
Initial state:
  ¬B ∧ ¬flag
Invariant:
  flag =⇒ B
{Premerge : True}
# no precondition
merge(B, flag , B0 , flag0 ):
    B := B ∨ B0
    flag := flag ∨ flag0
                                Comparison function:
                                  flag ∨ (¬flag0 ∧ ( B ∨ ¬B0 ))
                               {Premark : True}
                               # no precondition
                                mark():
                                  B.me := true
                               {Preagree : B}
                                agree():
                                  flag := true
```
Fig. 7: Pseudocode for consensus

```
Initial state:
    ∃ r, V.r ∧ t=0
  {Pretransfer : V.me}
  transfer(ro ):
    t = t+1
    V.me := false
    V.r0 := true
                                 Comparison function:
                                   t>t0
                                   ∨ (t = t0 ∧ V=V0 )
                                 {Premerge :
                                   (t = t0 =⇒ V=V0 )
                                   ∧ (V.me =⇒ t ≥ t0 )}
                                 merge((t,V),(t0 ,V0 )):
                                   t = max(t,t0 )
                                   v = (t0 <t)?V:V0
Invariant:
  ∃ r, V.r ∧ ∀ r, r0 , (V.r ∧ V.r0 ) =⇒ r=r0
```
Fig. 8: Specification of a distributed lock

The pseudo code of the consensus example is shown in Figure 7. The design for consensus can be relaxed, requiring only the majority of replicas to mark their boxes. The extension for that is trivial.

#### **5.2 A replicated concurrency control**

We now discuss an object, a distributed lock, that ensures mutual exclusion. We use an array of boolean values, one entry per replica, to model a lock. If a replica owns the lock, the corresponding array entry is set to true. The lock is transferred to any other replica by using the transfer function. The full specification is shown in Figure 8.

We need to ensure that the lock is owned by exactly one replica at any given point in time, which is the invariant here. For simplicity, we are not considering failures. In order to preserve safety, we need to enforce a precondition on the transfer operation such that the operation can only transfer the ownership of its origin replica. For state inflation, a timestamp associated with the lock is incremented during each transfer.

A merge of two states of this distributed lock will preserve the state with the highest timestamp. In order for the merge function to be the least upper bound, we must specify that if the timestamps of the two states are equal, their corresponding boolean arrays are also equal. Also if the origin replica owns the lock, it has the highest timestamp. The conjunction of these two restrictions which form the precondition of merge, Premerge, is the concurrency invariant, Invconc.

Consider the case of three replicas r1, r2 and r3 sharing a distributed lock. Assume that initially replica r1 owns the lock. Replicas r2 and r3 concurrently place a request for the lock. The current owner r1, has to make a decision on the priority of the requests based on the business logic. r1 calculates a higher priority for r3 and transfers the lock to r3. Since r1 no longer has the lock, it cannot issue any further transfer operations. We see here clearly that the transfer operation is safe. In the new state, r3 is the only replica that can perform a transfer operation. We can also note that this prevents any concurrent transfer operations. This can guarantee mutual exclusion and hence ensures safety in a concurrent execution environment.

An interesting property we can observe from this example is total order. Due to the preconditions imposed in order to be safe, we see that the states progress through a total order, ordered by the timestamp. The transfer function increases the timestamp and merge function preserves the highest timestamp.

#### **5.3 Courseware**

We now look at an application that allows students to register and enroll in a course. For space reasons, we elide the pseudocode which can be found in the extended version[23]. The state consists of a set of students, a set of courses and enrollments of students for different courses. Students can register and deregister, courses can be created and deleted, and a student can enroll for a course. The invariant requires enrolled students and courses to be registered and created respectively.

The set of students and courses consists of two sets - one to track registrations or creations and another to track deregistrations or deletions. Registration or creation monotonically adds the student or course to the registered sets respectively and deregistration or deletion monotonically adds them to the unregistered sets. The semantics currently doesn't support re-registration, but that can be fixed by using a slightly modified data structure that counts the number of times the student has been registered/unregistered and decides on the status of registration. Enrollment adds the student-course pair to the set. Currently, we do not consider canceling an enrollment, but it is a trivial extension. Merging two states takes the union of the sets.

Let us consider the safety of each operation. The operations to register a student and create a course are safe without any restrictions. Therefore they do not need any precondition. The remaining three operations might violate the

invariant in some cases. This leads to strengthening their preconditions. The precondition of the operation for deregistering a student and deleting a course requires no existing enrollments for them. For enrollment, both the student and the course should be registered/created and not unregistered/deleted.

Merge also requires strengthening of its precondition. It requires the set of enrolled students and courses to be registered and not unregistered in all the remote states as well. This is the concurrent invariant (Invconc) for this object.

Running this specification through our tool which we describe in Section 6 reveals concurrency issues for deregistering a student, deleting a course and enrollment. This means that we need to add concurrency control to the state.

For this use case, we know that enrolling will be more frequent than deregistering a student or deleting a course. So, we model a concurrency control mechanism as in the case of the auction object discussed earlier. We assign a token to each replica for each student and course, called a student token and course token respectively. A replica will have a set of student tokens indicating the registered students and course tokens indicating the created courses. In order to deregister a student or delete a course, all replicas must have released their tokens for that particular student/course. Enroll operations can progress as long as the student token and course token are available at the local replica for the student and course for that particular enrollment.

This concurrency control mechanism now forms part of the state. The preconditions of operations and merge are recomputed and the concurrency invariant is updated. The edited specification passes all checks and is deemed safe.

# **6 Automation**

In this section, we present a tool to automate the verification of invariants as discussed in the previous sections. Our tool, called *Soteria* is based on the Boogie [5] verification framework. The input to Soteria is a specification of the object written as Boogie procedures, augmented with a number of domain-specific annotations needed to check the properties described in Section 4.

Let us now consider how a distributed object is specified in Soteria.:

programmer to provide the precondition Preop. In general, operations are encoded as Boogie procedures. Alternatively, we could just require only a post-condition describing how the state transitions from the precondition to the post-condition. Notice that since in our program model operations are atomic, this is an unambiguous encoding of the operations.

A few things are important in this code. The specification declares operations that can modify the contents of the global variables as declared in the modifies clause. Preconditions are annotated with the requires clauses, and the postcondition is specified by the ensures clauses. The semantics of multiple requires and ensures clauses is conjunction.

**– Merge function:** We require the special merge operation to be distinguished from other operations. To that end, we use the annotation @merge. While, as mentioned before, the precondition of merge can be obtained by calculating the weakest precondition to ensure safety. The current version of Soteria does not perform this step automatically, it relies on the developer to provide the preconditions. Notice that, as we argued in Section 4.1, Soteria will consider this as the concurrency invariant (Invconc).

While in Section 3 we mentioned that the merge procedure takes two states as arguments, in the specification input to Soteria, the procedure merge takes only one state as the argument. This is because this procedure assumes that the merge is being applied in a replica, and therefore, the local state of the replica is captured by the global variables.

**– Invariant:** Clearly, we require the programmer to provide the invariant to be verified by the tool. This invariant is simply provided as a Boogie assertion over the state of the object. Once more, we require the invariant to be annotated with the special keyword @invariant.

While these are the components required by Soteria to check the safety, often Boogie requires additional information to verify the procedures. Some of these components are:

#### **6.1 Verification passes**

The verification of a specification is performed in multiple stages. Let us consider these in order:

# 1. **Syntax checks**

The first simple checks validate that the specification provided respects Boogie syntax when ignoring Soteria annotations. It also calls Boogie to validate that the types are correct and that the pre/post conditions provided are sound.

Then it checks that the specification provides all the elements necessary for a complete specification. Specifically, it checks the function signatures marked by @gteq and @invariant and the procedure marked by @merge.

# 2. **Convergence check**

This stage checks the convergence of the specification. Specifically, it checks whether the specification respects Strong Eventual Consistency. The *Strong Eventual Consistency* (SEC) property states that any two replicas that received the same set of updates are in the same state. To guarantee this, objects are designed to have certain sufficient properties in the encoding of the state [3, 4, 25], which can be summarised as follows:

We present the conditions formally in the extended version[23].

An alternative is to make use of the CALM theorem [12]. This allows nonmonotonic operations, but requires them to coordinate. However, our aim is to provide maximum possible availability with SEC. 7

To ensure these conditions of Strong Eventual Consistency, the tool performs the following checks:

**–** That each operation is an inflation.  The verification condition discharged is shown below:

$$\begin{array}{l} \mathsf{a}\texttt{a}\texttt{a}\texttt{un}\,\mathsf{o} \quad (\sigma,\sigma') \in \mathsf{Pre}\_{\texttt{narg}}\\ \mathsf{c}\texttt{a}\texttt{11}\quad\sigma\_{new} := \texttt{narg}(\sigma,\sigma')\\ \mathsf{a}\texttt{a}\texttt{a}\texttt{o}\texttt{r}\texttt{t} \quad \sigma\_{new} \geq \sigma \wedge \sigma\_{new} \geq \sigma'\\ \mathsf{a}\texttt{a}\texttt{a}\texttt{o}\texttt{r}\texttt{t} \quad \forall \sigma\*,\sigma\* \geq \sigma \wedge \sigma\* \geq \sigma' \implies \sigma\* \geq \sigma\_{new} \end{array}$$

	- **–** *Sequential safety:* Soteria checks whether each individual operation is safe. This corresponds to the conditions (2) and (3) in Figure 5. The verification condition discharged by the tool to ensure sequential safety of operations is:

7 Convergence of our running example is discussed in the extended version[23].

```
assume σ ∈ Preop ∧ Inv
call σnew := op(σ)
assert σnew ∈ Inv
```
The special case of the merge function is verified with the following verification condition:

```
assume (σ, σ-

              ) ∈ Premerge ∧ σ ∈ Inv ∧ σ-
                                         ∈ Inv
call σnew := merge(σ, σ-

                           )
assert σnew ∈ Inv
```
Notice that in this condition we assume that there are two copies of the state, the state of the replica applying the merge, and the state with superscript representing a state arriving from another replica. In case of failure of the sequential safety check, the designer needs to strengthen the precondition of the operation (or merge) which was unsafe.

**–** *Concurrent safety:* Here we check whether each operation upholds the precondition of merge. This corresponds to the conditions (5) and (6) in Figure 5. Notice that while this check relates to the concurrent behaviour of the distributed object, the check itself is completely sequential; it does not require reasoning about operations performed by other processes. As shown in Section 4, this ensures safety during concurrent operation.

The verification conditions are:

```
assume σ ∈ Preop ∧ Inv ∧ (σ, σ-

                                ) ∈ Invconc
call σnew := op(σ)
assert (σnew, σ-

                  ) ∈ Invconc
```
to validate each operation op, and

assume (σ, σ- ) ∈ Invconc ∧ σ ∈ Inv ∧ σ- ∈ Inv call σnew := merge(σ, σ- ) assert (σnew, σ) ∈ Invconc

to validate a call to merge. If the concurrent safety check fails, the design of the distributed object needs a replicated concurrency control mechanism embedded as part of the state.

When all checks are validated, the tool reports that the specification is safe. Whenever a check fails, Soteria provides a counterexample 8 along with the failure message tailored to the type of check. This can help the developer identify issues with the specification and fix it.

Once the invariants and specification of an application is given, Soteria is fully automatic, thanks to Z3, an SMT solver that is fully automated. The specification of the application includes the state, all the operations including the pre and post conditions (including merge). In case the invariant cannot be proven, Soteria provides counter-examples. The programmer can leverage these to update the specification with appropriate concurrency control, rerun Soteria, and so on until the application is correct. As far as the proof system is concerned, no programmer involvement is required. Currently, the effort of adding the required synchronization conditions is manual, but as the next step, we are working on

8 Soteria uses the counter model provided by Boogie.

automating the efficient generation of synchronization control considering the workload characteristics. The tool and the full specifications in the form of the tool input are available at Soteria [22]. 9

# **7 Related Work**

Several works have concentrated on the formalisation and specification of eventually consistent systems [7, 8, 27] to mention but a few.

A number of works concentrate on the specification and correct implementation of replicated data types [10, 14]. Unlike these works, we are not concerned with the correctness of the data type implementation with respect to a specification, but rather on proving properties that hold of a distributed object.

Gotsman et al.[11] present a proof methodology for proving invariants of distributed objects. In fact, that work has been extended with a tool called CISE [24] which, similar to Soteria, performs the check using an SMT solver as a backend. Another more user-friendly tool was developed by Marcelino et al.[19] based on the principle of CISE. It is named Correct Eventual Consistency(CEC) Tool. The tool is based on Boogie verification framework and also proposes sets of tokens that the developer might use. An improved token generation by using the counterexamples generated by Boogie is discussed by Nair and Shapiro[20].

Unlike our work, CISE and CEC (and more generally the work of Gotsman et al.[11]) consider the implementation of operation-based objects. As a consequence, they assume that the underlying network model ensures causal consistency, and the proof methodology therein presented requires reasoning about concurrent behaviours (reflected as stability verification conditions on assertions). We position Soteria as a *complementary* tool to CISE, since CISE is not well-adapted to reason about systems that propagate state, and Soteria is not well-adapted to reason about objects that propagate operations. We consider, as part of our future work, the use of both CISE and Soteria in tandem to prove properties depending on the implementation of the objects at hand.

Houshmand et al.[13] extends CISE by lowering the causal consistency requirements and generating concurrency control protocols. It still requires reasoning about concurrent behaviours.

As anticipated in Section 4, Bailis et al. [2] introduced the concept of Iconfluence based on a similar system model. I-confluence states that for an invariant to hold in a lattice-based state-propagating distributed application, the set of *reachable* valid (i.e. invariant preserving) states must be closed under operations and merge. This condition is similar to the ones presented in Figure 5. However, there is a fundamental difference: while Bailis et al. [2] recognises that one needs to consider only *reachable* states when checking that the merge operation satisfies the invariant, they do not provide means to identify these reachable states. This is indeed a hard problem. In Soteria, we instead *over-approximate the set of reachable states* by ignoring whether the states are indeed reachable,

9 Experimental results with verification time is provided in the extended version[23].

but requiring that their merge satisfies the invariant. This is captured in the concurrency invariant, Invconc, which is synthesised from the user provided invariant. How to obtain this invariant is understandably not addressed in Bailis et al.[2] since no proof technique is provided. Notice that this is a sound approximation since it guarantees the invariant is satisfied, and we also verify that every operation preserves this condition as shown in Corollary 1. In this sense we say that the pre-condition of merge for a given invariant I, is also an invariant of the system. It is this abstraction step that makes the analysis performed by Soteria to be syntax-driven, automated, and machine-checked. The fact that Soteria is an analysis of a program is in contrast with I-confluence [2] where no means to link a given program text to the semantical model, let alone rules to show that the syntax implies invariant preservation, are provided. In other words, Iconfluence [2] does not provide a program logic, but rather a meta-theoretical proof about lattice-based state-propagating systems.

Our previous work [21], provides an informal proof methodology for ensuring safety of Convergent Replicated Data Types(CvRDTs), which are a group of specialised data structures used to ensure convergence in distributed programming. This work builds upon it, and formalises the proof rules and prove them sound. We relax the requirement of CvRDTs by allowing the usage of any data types, that together respect the lattice conditions mentioned in Section 3. We also show several case studies which demonstrate the use of the rule.

A final interesting remark is that we can show how our methodology can aid in the verification of distributed objects mediated by concurrency control. Some works [16, 17, 26, 27] have considered this problem from the standpoint of synthesis, or from the point of view of which mechanisms can be used to check a certain property of the system.

# **8 Conclusion**

We have presented a sound proof rule to verify invariants of state-based distributed objects, i.e., the objects that propagate state. We present the proof obligations guaranteeing that the implementation is safe in concurrent execution by reducing the problem to checking that each operation of the object satisfies a precondition of the merge function of the state.

We presented Soteria, a tool sitting on top of the Boogie verification framework. This tool can be used to identify the concurrency bugs in the design of a distributed object. Soteria also checks convergence by checking the lattice conditions on the state, described by [3]. We have shown multiple compelling case-studies showing how Soteria can be leveraged to ensure the correctness of distributed objects that propagate state. It would be an interesting next step to look into automatic concurrency control synthesis. The synthesised concurrency control can be analysed and adapted dynamically to minimise the cost of synchronisation.

**Acknowledgements.** This research is supported in part by the RainbowFS project (*Agence Nationale de la Recherche*, France, number ANR-16-CE25-0013-01) and by European H2020 project 732 505 LightKone (2017–2020).

# **Bibliography**

workshops, Assoc. for Computing MachinerySpecial Interest Group on Op. Sys. (SIGOPS), Assoc. for Computing Machinery, London, UK (Apr 2016), http://dx.doi.org/10.1145/2911151.2911160

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Solving Program Sketches with Large Integer Values

Rong Pan1, Qinheping Hu2, Rishabh Singh3, and Loris D'Antoni2

1 The University of Texas at Austin, Austin, USA 2 University of Wisconsin-Madison, Madison, USA

3Google, Mountain View, USA

Abstract. Program sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the assertions. The most popular sketching tool, Sketch, can efficiently solve complex program sketches, but uses an integer encoding that often performs poorly if the sketched program manipulates large integer values. In this paper, we propose a new solving technique that allows Sketch to handle large integer values while retaining its integer encoding. Our technique uses a result from number theory, the Chinese Remainder Theorem, to rewrite program sketches to only track the remainders of certain variable values with respect to several prime numbers. We prove that our transformation is sound and the encoding of the resulting programs are exponentially more succinct than existing Sketch encodings. We evaluate our technique on a variety of benchmarks manipulating large integer values. Our technique provides speedups against both existing Sketch solvers and can solve benchmarks that existing Sketch solvers cannot handle.

# 1 Introduction

Program synthesis, the art of automatically generating programs that meet a user's intent, promises to increase the productivity of programmers by automating tedious, error-prone, and time-consuming tasks. Syntax-guided Synthesis (SyGuS) [2], where the search space of possible programs is defined using a grammar or a domain-specific language, has emerged as a common program synthesis paradigm for many synthesis domains. One of the earliest and successful syntaxguided program synthesis frameworks is program sketching [19], where (i) the search space of the synthesis problem is described using a partial program in which certain integer constants are left unspecified (represented as holes), and (ii) the specification is provided as a set of assertions describing the intended behavior of the program. The goal of the synthesizer is to automatically replace the holes in the program with integer values so that the resulting complete program satisfies all the assertions. Thanks to its simplicity, program sketching has found wide adoption in applications such as data-structure design [20], personalized education [18], program repair [7], and many others.

The most popular sketching tool, Sketch [21], can efficiently solve complex program sketches with hundreds of lines of code. However, Sketch often performs poorly if the sketched program manipulates large integer values. Sketch's synthesis is based on an algorithm called counterexample-guided inductive synthesis (Cegis) [21]. The Cegis algorithm iteratively considers a finite set I of inputs for the program and performs SAT queries to identify values for the holes so that the resulting program satisfies all the assertions for the inputs in I. Further SAT queries are then used to verify whether the generated solution is correct on all the possible inputs of the program. Sketch represents integers using a unary encoding (a variable for each integer value) so that arithmetic computations such as addition, multiplication etc. can be represented efficiently in the SAT formulas as lookup operations. This unary encoding, however, results in huge formulas for solving sketches with larger integer values as we also observe in our evaluation. Recently, an SMT-like technique that extends the SAT solver with native integer variables and integer constraints was proposed to alleviate this issue in Sketch. It guesses values for the integer variables and propagates them through the integer constraints, and learns from conflict clauses. However, this technique does not scale well when the sketches contain complex arithmetic operations—e.g., non-linear integer arithmetic.

In this paper, we propose a program transformation technique that allows Sketch to solve program sketches involving large integer values while retaining the unary encoding used by the traditional Sketch solver. Our technique rewrites a Sketch program into an equivalent one that performs computations over smaller values. The technique is based on the well-known Chinese Remainder Theorem, which states that, given distinct prime numbers p1,...,pn such that N = p1 · ... · pn, for every two distinct numbers 0 ≤ k1, k2 < N, there exists a pi such that k1 mod pi = k2 mod pi. Intuitively, this theorem states that tracking the modular values of a number smaller than N for each pi is enough to uniquely recover the actual value of the number itself. We use this idea to replace a variable x in the program with n variables xp1 ,...,xpn , so that for every i, xpi = x mod pi. Using closure properties of modular arithmetic we show that, as long as the program uses the operators +, −, ∗, ==, tracking the modular values of variables and performing the corresponding operations on such values is enough to ensure correctness. For example, to reflect the variable assignment x = y+z, we perform the assignment xpi = (ypi +zpi ) mod pi, for every pi. Similarly, the Boolean operation x == y will only hold if xpi = ypi , for every pi. To identify what variables and values in the program can be rewritten, we develop a data-flow analysis that computes what variables may flow into operations that are not sound in modular arithmetic—e.g., <, >, ≤, and /.

We provide a comprehensive theoretical analysis of the complexity of the proposed transformation. First, we derive how many prime numbers are needed to track values in a certain integer range. Second, we analyze the number of bits required to encode values in the original and rewritten program and show that, for the unary encoding used by Sketch, our technique offers an exponential saving in the number of required bits.

We evaluate our technique on 181 benchmarks from various applications of program sketching. Our results show that our technique results in significant speedups over existing Sketch solvers and is able to solve 48 benchmarks on which Sketch times out.

Contributions. In summary, our contributions are:

An extended version containing all proofs and further details has been uploaded to arXiv as supplementary material.

# 2 Motivating Example

In this section, we use a simple example to illustrate our technique and its effectiveness. Consider the Sketch program polyArray presented in Figure 1b. The goal of this synthesis problem is to synthesize a two-variable quadratic polynomial (lines 7–8) whose evaluation p on given inputs x and y is equal to a given expected-output array z (line 9). Solving the problem amounts to finding non-negative integer values for the holes (??) and sign values, i.e., -1 or 1, for the holes (??s) such that the assertion becomes true.1 In this case, a possible solution is the polynomial:

p[i] = -17\*y[i]^2-8\*x[i]\*y[i]-17\*x[i]^2-3\*x[i];

When attempting to solve this problem, the Sketch synthesizer times out at 300 seconds. To solve this problem, Sketch creates SAT queries where the variables are the holes. Due to the large numbers involved in the computation of this program, the unary encoding of Sketch ends up with SAT formulas with approximately 45 million clauses.

1 In Sketch, holes can only assume positive values. This is why we need the sign holes, which are implemented using regular holes as follows: if(??) then 1 else -1.

```
1 // n=4, x=[24,-1,0,-19], y=[-7,11,-3,13]
 2 // z=[-9353,-1983,-153,-6977]
 3 polyArray(int n, int[n] x, int[n] y, int[n] z){
 4 int[n] p;
 5 int i=0;
 6 while (i<n){
 7 p[i]=?? s
              1 *??1 *y[i]2 +??s
                           2 *??2 *x[i]2 +??s
                                        3 *??3 *x[i]*y[i]
 8 +??s
               4 *??4 *y[i ]+?? s
                           5 *??5 *x[i ]+?? s
                                        6 *??6 ;
 9 assert p[i] == z[i];
10 i++; }
11 }
                (a) Original sketch program.
1 // n=4, x=[24,-1,0,-19], y=[-7,11,-3,13]
2 // z=[-9353,-1983,-153,-6977]
3 pAPrime(int n, int[n] x, int[n] y, int[n] z){
4 int[n] x2,x3,x5 ,x7 ,x11 ,x13 ,x17;
5 while (i<n){ // Initialize modular variables
6 x2[i]=x[i]%2;
7 x3[i]=x[i]%3;
8 ... i++; }
9 int i=0;
10 int[n] p2,p3,p5 ,p7 ,p11 ,p13 ,p17;
11 while (i<n){
12 p2[i]=(?? s
               1 *(??1 %2)*(y2[i]2 %2)%2
13 +??s
               2 *(??2 %2)*(x2[i]2 %2)%2
14 +??s
               3 *(??3 %2)*(x2[i]%2)*(y2[i]%2)%2
15 +??s
               4 *(??4 %2)*(y2[i]%2)%2
16 +??s
               5 *(??5 %2)*(x2[i]%2)%2
17 +??s
               6 *(??6 %2)%2)%2;
18 ...
19 assert p2[i] = z2[i];
20 assert p3[i] = z3[i];
21 ...
22 i++; }
23 }
```
(b) Rewritten sketch program.

Fig. 1: Sketch program (a) and rewritten version with values tracked for different moduli (b).

Sketch Program with Modular Arithmetic The technique we propose in this paper has the goal of reducing the complexity of the synthesis problem by transforming the program into an equivalent one that manipulates smaller integer values and that yields easier SAT queries. Given the Sketch program in Figure 1b, our technique produces the modified Sketch program pAPrime in Figure 1a. The new Sketch program has the same control flow graph as the original one, but instead of computing the actual values of the expressions x[·] and y[·], it tracks their remainders for the set of prime numbers {2, 3, 5, 7, 11, 13, 17} using new variables—e.g., x2[i] tracks the remainder of x[i] modulo 2.

The program pAPrime initializes the modular variables with the corresponding modular values (lines 5–8). When rewriting a computation over modular variables, the same computation is performed modularly (lines 12–17). For example, the term ??s 1 ∗ ??1\*y[i]2 when tracked modulo 2 is rewritten as

$$(\text{??}\,\text{?}\,\_1^a \star (\text{?}\,\_1\text{?}\,\_2) \star (\text{(}\,\_2\text{I}\,\text{?}\,\_1\text{?}\,\_2\text{?}\,\_2) \,\text{?}\,\_2^a)$$

In the rewritten program, the variables i and n are not tracked modularly, since such a transformation would incorrectly access array indices. Finally, the assertions for different moduli share the same holes as the solution to the Sketch has to be correct for all modular values. In the rest of the paper, we develop a data flow analysis that detects when variables can be tracked modularly.

Sketch can solve the rewritten program in less than 2 seconds and produce hole values that are correct solutions for the original program. This speedup is due to the small integer values manipulated by the modular computations. In fact, the intermediate SAT formulas generated by Sketch for the program pAPrime have approximately 120 thousand clauses instead of the 45 million clauses for polyArray. Due to the complex arithmetic in the formulas, even if Sketch uses the SMT-like native integer encoding, it still requires more than 300 seconds to solve this problem.

While this technique is quite powerful, it does have some limitations. In particular, the solution to the rewritten Sketch is guaranteed to be a correct solution only for inputs that cause intermediate values of the program to be in a range [d1, d2] such that d2 − d1 ≤ 2 × 3 × 5 × 7 × 11 × 13 × 17 = 510, 510. We will prove this result in Section 4.

# 3 Preliminaries

In this section, we describe the IMP language that we will consider throughout the paper and briefly recall the counter-example guided inductive synthesis algorithm employed by the Sketch solver.

For simplicity, we consider a simple imperative language IMP with integer holes for defining the hypothesis space of programs. The syntax and semantics of IMP are shown in Appendix ??. Without loss of generality, we assume the programs consists of a single program f(v1, ··· , vn, ??1,...??m) with n integer variables and m integer holes. The body of the program f consists of a sequence of statements, where a statement s can either be a variable assignment, a while loop statement, an if conditional statement, or an assert statement. The holes ?? denote integer constant values that are unknown and the goal of the synthesis process is to compute these values such that a set of desired program assertions are satisfied for every possible input values to f. 2

2 Our implementation also supports for-loops, recursion, arrays, and complex types.

Example 1. An example IMP sketch denoting a partial program is shown below.

$$\mathtt{tr}\mathtt{if}\mathtt{p1e}\{\mathtt{n},\mathtt{h},\mathtt{?}\mathtt{?}\}\{\mathtt{\h}=\mathtt{?}\mathtt{?},\mathtt{a}\mathtt{s}\mathtt{s}\mathtt{er}\mathtt{st}\mathtt{.}\mathtt{h}\mathtt{\*}\mathtt{n}=\mathtt{n}+\mathtt{n}+\mathtt{n};\quad\mathtt{\h}\}$$

The goal of the synthesizer is to compute the value of the hole ?? such that the assertion is true for all possible input values of n and h. For this example, ?? = 3 is a valid solution.

The Sketch solver uses the counter-example guided inductive synthesis algorithm (Cegis) to find hole values such that the desired assertions hold for all input values. Formally, the Sketch synthesizer solves the following constraint:

$$\exists \mathcal{T} \equiv (\mathcal{T}\mathbf{?}\_1, \dots, \mathbf{?}\mathbf{?}\_m) \in \mathbb{Z}^m. \,\forall in \in \mathcal{T}. \,\left[f\{in, \mathbf{?}\mathbf{?}\}\right]^{\mathbf{IIP}} \neq \perp$$

where Z denotes the domain of all integer values, ?? denotes the list of unknown hole values (??1, ··· , ??m) ∈ Zm, I denotes the domain of all input argument values to the function f, and f(in, ??)IMP = ⊥ denotes that the program satisfies all assertions. The synthesis problem is in general undecidable for a language with complex operations such as the IMP language because of the infinite size of possible hole and input values. To make the synthesis process more tractable, Sketch imposes a bound on the sizes of both the input domain (Ib) and the domain of hole values (Zb) to obtain the following constraint:

$$\exists \mathcal{T} \mathcal{T} \equiv (\mathcal{T}\mathcal{T}\_1, \dots, \mathcal{T}\mathcal{T}\_m) \in \mathbb{Z}\_b^m. \,\forall in \in \mathbb{Z}\_b. \,\left[f \,\{in, \text{??}\}\right]^{\text{IMP}} \neq \perp.$$

The bounded domains make the synthesis problem decidable, but the secondorder quantified formula results in a search space of hole values that is still huge for any reasonable bounds. To solve such bounded equations efficiently, Sketch uses the Cegis algorithm to incrementally add inputs from the domain until obtaining hole values ?? that satisfy the assertion predicates for all the input values in the bounded domain. The algorithm solves the second-order formula by iteratively solving a series of first-order queries. It first encodes the existential query (synthesis query) over a randomly selected input value in0 to find the hole values *H* that satisfy the predicate for in0 using a SAT solver in the backend.

$$\exists \mathcal{T} \mathcal{T} \equiv (\mathcal{T}\mathcal{T}\_1, \dots, \mathcal{T}\mathcal{T}\_m) \in \mathbb{Z}\_b^m. \ [f \,\!\!/ \, in\_0, \mathcal{T}\mathcal{T}\!\!\!/]^{\text{IMP}} \neq \perp.$$

It then encodes another existential query (verification) to now find a counterexample in1 for which the predicate is not satisfied for the previously found hole values.

$$\exists in\in\mathcal{I}\_b.\ \neg[f\,\langle in,H\rangle]^{\mathsf{IMP}}\neq\bot$$

If no counter-example input can be found, the hole values are returned as the desired solution. Otherwise, the algorithm computes a new hole value that satisfies the assertion for all the counter-example inputs found so far. This process continues iteratively until either a desired hole value is found (i.e. no counter-example input exists), no satisfiable hole value is found (i.e. the synthesis problem is infeasible), or the SAT solver times out.

Integer Encoding The Sketch solver can efficiently solve the synthesis constraint in many domains, but it does not scale well for sketches manipulating large numbers. Sketch uses a unary encoding to represent integers, where the encoded formula consists of a variable for each integer value. The unary encoding allows for simplifying the representation of complex non-linear arithmetic operations. For example, a multiplication operation can be represented as simply a lookup table using this encoding. In practice, the unary encoding results in magnitudes of faster solving times compared to the logarithmic encoding for many synthesis problems. However, this also results in huge SAT formulas in presence of large integers. Recently, a new SMT-like technique based on extending the SAT solver with native integer variables and constraints was proposed to alleviate this issue in Sketch. Similar to the Boolean variables, this extended solver guesses for integer values and propagates them in the constraints while also learning from conflict clauses. Note that Sketch uses these SAT extensions and encodings instead of an SMT solver as SMT doesn't scale well for the nonlinear constraints typically found in the synthesis problems. Our new technique for handling computations over large numbers still maintains the efficient unary encoding of integers and computations over them.

# 4 Modular Arithmetic Semantics

In this section, we present the language IMP-MOD in which variables can be tracked using modular arithmetic. We start by recalling the Chinese Remainder Theorem, then define both a modular and integer semantics for the IMP-MOD language, and show that the two semantics are equivalent.

# 4.1 The Chinese Remainder Theorem

The Chinese Remainder Theorem is a powerful number theory result that shows the following: given a set of distinct primes P = {p1,...,pk}, any number n in an interval of size p1 · ... · pk can be uniquely identified from the remainders [n mod p1, ··· , n mod pk]. In Section 4.2, we will use this idea to define the semantics of the IMP-MOD language. The main benefit of this idea is that the remainders could be much smaller than actual program values.

Example 2. For P = [3, 5, 7] and an integer 101, its remainders [2, 1, 3] are much smaller than 101. However, any number of the form 101 + 105 × n also has remainders [2, 1, 3] with respect to the same prime set.

In general, one cannot uniquely determine an arbitrary integer value from its remainders for some set P—i.e., the mapping from a number to its remainders is an abstraction in the sense of abstract interpretation [6]. However, if we are interested in a limited range of integer values [L, U), one can choose a set of primes P = {p1,...,pk} such that, for values L ≤ x<U, the map [r1, ··· , rk] → x, where x ≡ ri mod pi, is an injection.

Modular Expr aP := c P | vP | aP 1 opP *a* aP 2 | toPrime(a) Modular Op opP *a* := + |−|∗ Arith Expr a := ?? | c | v | a1 op*a* a2 Arith Op op*a* := + |−|∗| / Bool Expr b := not b | a1 op*c* a2 | b1 and b2 | b1 or b2 | aP 1==aP 2 Comp Op op*c* := < | > |≤|≥ Stmt s := v = a | vP = aP | s1; s2 | while(b) {s} | if(b) s1 else s2 | assert b Program P := f(v1, ··· , v*n*, vP 1, ··· , vP *m*, ??1,..., ??*l*) {s}

Fig. 2: Syntax of the IMP-MOD language.

Theorem 1 (Chinese Remainder Theorem [4]). Let p1, ..., pk be positive integers that are pairwise co-prime—i.e., no two numbers share a divisor larger than 1. Denote N = k i=1 pi, and let d, r1, r2, ..., rk be any integers. Then there is one and only one integer d ≤ x<d + N such that x ≡ ri mod pi for every 1 ≤ i ≤ k.

We define the translation function mP(x) := [x mod pi, ··· , x mod pk] that maps an integer to its set of remainders with respect to P. When mP(x) is bijective on some set R, we denote with m−1,R P : [0, p1) ×···× [0, pk) → R its inverse function.

Example 3. Let x be a integer in the range [0, 105) (note that 105 = 3 × 5 × 7). If we know that the value of x is congruent to [2, 1, 3] modulo {3, 5, 7}, we can uniquely identify the value of x to be 101 by observing that 101 ≡ 2 mod 3, 101 ≡ 1 mod 5, and 101 ≡ 3 mod 7.

The following lemma shows that the function mP is closed under addition, subtraction and multiplication of integers.

Lemma 1. For every set of primes P, integers x and y, and op ∈ {+, −, ∗}, the following holds: mP(x op y) = mP(x) op mP(y).

# 4.2 The IMP-MOD Language

In this section, we define the IMP-MOD language (syntax in Figure 2), a variant of the IMP language for which the semantics can be defined using modular arithmetic.3 An IMP-MOD program is parametric on a set P = {p1,...,pk} of distinct

3 We consider the simple subset for a clear presentation of the semantics, but our framework works for the full IMP language (and for more complex language constructs) as we will see in the later sections.

toPrime(a) P *σ,σ*P := [ a P *σ,σ*P mod p1, ··· ] vP P *σ,σ*P := σP(v) cP P *σ,σ*P := [ c mod p1, ··· , c mod p*k* ] aP 1 opP *a* aP 2 P *σ,σ*P := [ (x1 1 opP *a* x2 1) mod p1, ··· ] where aP *i* P = [ x*i* 1, ··· , x*i k* ] aP 1== aP 2 P *σ,σ*P := x1 1==x2 1 ∧···∧ x1 *k* == x2 *k* where aP *i* P = [ x*i* 1, ··· , x*i k* ] c P *σ,σ*P := c v P *σ,σ*P := σ(v) a1 op*a* a2 P *σ,σ*P := a1 P *σ,σ*P op*a* a2 P *σ,σ*P v = a P *σ,σ*P := (σ[v ← a P *σ,σ*P ], σP) vP = aP P *σ,σ*P := (σ, σP[vP ← aP P *σ,σ*P ])

Fig. 3: Modular semantics.

prime numbers. The structure of an IMP-MOD program is similar to an IMP program, but IMP-MOD supports two types of variables and arithmetic expressions: the regular IMP ones (i.e., v, a, and b), which operate over an integer semantics, and the modular ones (i.e., vP, aP, and bP), which take as an additional parameter the set of primes P and operate over a modular semantics. The semantics of some of the key constructs of IMP-MOD is shown in Figure 3.

The key idea of the modular semantics is that the value of each program variable in vP and arithmetic expressions in aP is denoted by a tuple of values, one for each prime number pi ∈ P. For example, the value of the constant cP is represented by the tuple [c mod p1, ··· , c mod pk], where each individual value denotes the remainder of c when divided by the prime number pi ∈ P. Formally, the program f has two sets of variables V Z = {v1, ··· , vn} and V P = {vP 1 , ··· , vP m}, which contain all the integer and prime variables respectively, and a set of holes H = {??1,..., ??k}. The denotation function, uses two valuation functions: (i) σ : V Z ∪ H → Z, which maps variables and holes to integer values, (ii) σP : V P → [0, p1) ×···× [0, pk), which maps primed variables to modular values. The expression toPrime(a) converts the integer value of an integer expression a to a modular tuple. Arithmetic expressions in aP are computed using modular values with the result being obtained using modular arithmetic with respect to the corresponding primes in P. Note that the only comparison operator allowed over modular expressions is == and that the division operator cannot be applied to modular expressions. While the syntax does not directly allow for holes to be represented modularly—i.e., we do not have expressions of the form ??P—an expression of the form toPrime(??) effectively achieves the objective of representing a hole ?? modularly.

#### 4.3 Equivalence between the two Semantics

Next, we provide an alternative integer semantics, which applies the IMP integer semantics to modular expressions and show that, under some assumptions on the values manipulated by the program, the modular and integer semantics are equivalent. We will use this result to build our modified synthesis algorithm.

toPrime(a)*σ*1*,σ*2 := a*σ*1*,σ*2 vP*σ*1*,σ*2 := σ2(vP) cP*σ*1*,σ*2 := c aP 1 opP *a* aP 2*σ*1*,σ*2 := aP 1*σ*1*,σ*2 op*a* aP 2*σ*1*,σ*2 aP 1==aP 2*σ*1*,σ*2 := aP 1*σ*1*,σ*2==aP 2*σ*1*,σ*2 c*σ*1*,σ*2 := c v*σ*1*,σ*2 := σ1(v) a1 op*a* a2*σ*1*,σ*2 := a1*σ*1*,σ*2 op*a* a2*σ*1*,σ*2 v = a*σ*1*,σ*2 := (σ1[v ← a*σ*1*,σ*2 ], σ2) vP = aP*σ*1*,σ*2 := (σ1, σ2[vP ← aP*σ*1*,σ*2 ])

Fig. 4: Integer semantics.

Integer Semantics The integer semantics of IMP-MOD is shown in Figure 4 (denoted -·σ1,σ2 ). In this semantics, modular expressions are evaluated as integer expressions using the same semantics as for IMP—i.e., the values of modular variables and modular arithmetic expressions are denoted by integer values. Therefore, in the integer semantics, we use two valuation functions σ1 : V Z ∪ H → Z mapping variables and holes to integers and σ2 : V P → Z mapping modular variables to integers.

Relation between the Two Semantics We now show that the modular semantics is, in some sense, equivalent to the integer semantics. For the rest of this section, we fix a set of distinct primes P = {p1, ··· , pk}.

To prove the equivalence of the two program semantics, we will require the values of modular expressions to lie in some range that is covered by the prime numbers in P. The following definition captures this restriction.

Definition 1. Given a modular arithmetic expression aP (resp. Boolean expression b) and some integers L<U, we say aP with context (σ1, σ2) is uniformly in the range R := [L, U) —aP ∈σ1,σ2 R for short—if under the integer semantics, all evaluation of modular subexpressions of aP (resp. b) are in the range R:

Given a valuation function σ : V P → Z, we write mP ◦ σ to denote the modular valuation obtained by applying the mP function to σ—i.e., for every vP ∈ V P, (mP ◦ σ)(vP) = mP(σ(vP)). Similarly, for a modular valuation function σP : V P → [0, p1) ×··· [0, pk), we denote m−1,R P ◦ σP the integer valuation from V P to R such that, for every vP ∈ V P, (m−1,R P ◦ σP)(vP) = m−1,R P (σP(vP)). The following lemma shows that, when the values of modular arithmetic expressions lay in an interval of size N = p1 · ... · pk the modular and integer semantics of modular arithmetic expressions are equivalent.

Lemma 2. Given a set of primes P = {p1, ··· , pk}, an arithmetic expression aP, and two valuation functions σ1 : V Z ∪ H → Z and σ2 : V P → Z, we have

$$m\_{\mathbb{P}}([a^{\mathbb{P}}]\_{\sigma\_1,\sigma\_2}) = [a^{\mathbb{P}}]\_{\sigma\_1,m\_{\mathbb{P}}\diamond \sigma\_2}^{\mathbb{P}}$$

Moreover, if there exists an interval R of size N = p1 · ... · pk such that aP ∈σ1,σ2 R, then

$$m\_{\mathbb{P}}^{-1,R}([a^{\mathbb{P}}]\_{\sigma\_1,m\_{\mathbb{P}}\diamond \sigma\_2}^{\mathbb{P}}) = [a^{\mathbb{P}}]\_{\sigma\_1,\sigma\_2}.$$

Similarly, we show that the two semantics are also equivalent for Boolean expressions.

Lemma 3. Given a set of primes P = {p1, ··· , pk}, an interval R of size N = p1 ·...· pk, a Boolean expression b, and two valuation functions σ1 : V Z ∪H → Z and σ2 : V P → Z, if b ∈σ1,σ2 R, then bσ1,σ2 = bP σ1,mP◦σ2 .

We are now ready to show the equivalence between the modular semantics and the integer semantics for programs P ∈ IMP-MOD. The semantics of a program P = f(V Z, V P, H) {s} is a map from valuations to valuations, i.e., given a valuation σ1 : V Z → Z for integer variables, a valuation σ2 : V P → Z for modular variables and a valuation σH : H → Z for holes, we have -P(σ1, σ2, σH) = sσ1∪σH,σ2 and -PP(σ1, σ2, σH) = sP σ1∪σH,mP◦σ2 . Therefore, it is sufficient to show that the two semantics are equivalent for any statement s.

The two semantics are equivalent for a statement s if, under the same input valuations, the resulting valuations of the semantics can be translated to each other. Formally, given valuations σ1, σ2 and an interval R of size N, we say sσ1,σ2 ≡P sP σ1,mP◦σ2 iff σ 1 = σ 1 , mP ◦ σ 2 = σP 2 and σ 2 = m−1,R P ◦ σP 2 where sσ1,σ2 = (σ 1, σ 2) and sP σ1,mP◦σ2 = (σ 1 , σP 2 ).

We define uniform inclusion for statements.

Definition 2.

Theorem 2. Given a set of primes P = [p1, ··· , pk], a statement s and two valuation functions σ1 : V Z ∪H → Z and σ2 : V P → Z, if there exists an interval R of size N such that s ∈σ1,σ2 R, then sσ1,σ2 ≡P sP σ1,mP◦σ2 .

Algorithm 1: returns variables that should be tracked using modular/integer semantics.

```
/* f: sketched function, V P variables to be tracked modularly, V Z
    variables to be tracked with integer values */
1 function DataFlowAnalysis(f)
2 S ← {/, <, >, ≤, ≥}; V Z ← ∅
3 for op ∈ S do
       /* Compute all variables v that may flow into op */
4 V Z ← V Z ∪ Dataflow(op, f)
5 V P ← V \ V Z
6 return (V Z, V P)
```
# 5 From IMP to IMP-MOD Programs

In this section, we develop a data flow analysis for detecting variables in IMP programs for which it is sound to track values modularly. We then use this data flow analysis to rewrite an IMP program to an equivalent IMP-MOD program.

#### 5.1 Data Flow Analysis

The formalization of IMP-MOD in Section 4.2 made it clear that the modular semantics is only appropriate when integer values are manipulated using addition, multiplication, subtraction, and equality. Other operations like division and less-than comparison cannot be computed soundly in modular arithmetic.

Example 4. Consider an integer variable x with modular value x2 under modulus 2 and x3 under modulus 3, and an integer variable y with modular value y2, y3 under corresponding moduli. Then the assignment of x = y + y; implies x2 = (y2 + y2) mod 2; and x3 = (y3 + y3) mod 3. However, x = x/y; does not imply x2 = (x2/y2) mod 2; and x3 = (x3/y3) mod 3.

We now define a data flow analysis (shown in Algorithm 1) for computing which variables in a program must be tracked with the integer semantics (i.e., the set V Z) and which variables can be soundly tracked using the modular semantics (i.e., the set V P). For each operator op in {/, <, >, ≤, ≥}, the analysis computes the set of variables that may flow into the operands of an expression of the form e1 op e2. In practice, this is done via backward may analysis, noted as Dataflow procedure in Algorithm 1. The obtained set of variables must be tracked using the integer semantics. The remaining variables will never flow into a problematic operator and can therefore be tracked using the modular semantics.

Implementation Remark Since our implementation also supports arrays and recursion, the data flow analysis in Algorithm 1 is inter-procedural and the set S also contains the array indexing operator [ ]—i.e., given an expression arr[a], if a variable v may flow into a, then a must be tracked using the integer semantics.

R*a*(a) = ⎧ ⎪⎪⎪⎨ ⎪⎪⎪⎩ vP if a ≡ v and v ∈ V P cP if a ≡ c R*a*(a1) opP *a* R*a*(a2) if a ≡ a1 opP *a* a2 toPrime(a) otherwise R*b*(b) = ⎧ ⎪⎪⎪⎨ ⎪⎪⎪⎩ R*a*(a1) == R*a*(a2) if b ≡ a1 == a2 R*b*(b1) and R*b*(b2) if b ≡ b1 and b2 not R*b*(b1) if b ≡ not b2 b otherwise R*s*(s) = ⎧ ⎪⎪⎪⎪⎪⎪⎪⎪⎨ ⎪⎪⎪⎪⎪⎪⎪⎪⎩ R*s*(s1); R*s*(s2) if s ≡ s1; s2 v = a if s ≡ v = a and v ∈ V Z vP = R*a*(a) if s ≡ v = a and v ∈ V P if(R*b*(b)) R*s*(s0) else R*s*(s1) if s ≡ if(b) s0 else s1 while(R*b*(b)) {R*s*(s)} if s ≡ while b {s} assert R*b*(b) if s ≡ assert b

Fig. 5: Subset of rules for the translation from IMP to IMP-MOD programs. Rules are parametric in V Z, V P with P: Rf (f(V, ??){s}) = f(V Z, V P, ??){Rs(s)}.

Furthermore, while in our formalization we allow variables to be tracked using only one of the two semantics, in our implementation, we allow variables to be tracked differently (using actual values or modular values) at different program points by tracking, for each variable v, the program points for which the actual value of v is needed, which is done by using the same data-flow analysis. In this case, a variable might initially need to be tracked using actual values but can later be tracked using modular values.

Example 5. Consider the sketch program polyArray in Figure 1b. For this program, Algorithm 1 will return that the variables x and y can be tracked modularly. However, the variables i and n must be tracked using the integer semantics since they are used in a < operation and as array indices.

# 5.2 From IMP to IMP-MOD

Now that we have computed what sets of variables can be tracked modularly, we can transform the IMP program into an IMP-MOD program. The transformation Rf that rewrites f into an IMP-MOD program is shown in Figure 5. The key idea of the program transformation is to use the sets V Z and V P to only rewrite variables and sub-expressions of f for which the modular arithmetic can be performed soundly.

Once we get a solution for the IMP-MOD program as hole values, we can get a solution for the IMP program by mapping the hole to integer values given by the integer semantics.

Example 6. Consider a program where the dataflow analysis computes V Z = {i, n} and V P = {x}. The statement x = x + i + 1 is rewritten to xP = xP + toPrime(i)+1P.

The transformation Rf is sound.

Theorem 3. Given an IMP program f, and sets V Z and V P resulting from the data flow analysis on f, the program Rf (f) is in the IMP-MOD language. Moreover, fIMP = -Rf (f).

# 6 Solving IMP-MOD Sketches

In this section, we discuss how synthesis in the modular semantics relates to synthesis in the integer semantics and provide an incremental algorithm for solving IMP-MOD sketches.

# 6.1 Synthesis in IMP-MOD

Given a set of integers R we say that a variable valuation σ is in R (denoted σ ∈ R) if for every v, we have σ(v) ∈ R. Similarly to what we saw in Section 3, we assume that the sketch has to be solved for finite ranges of possible values for the hole (RH) and input values (Rin). Solving an IMP-MOD problem P = f(V,V P, H){s} for the integer semantics amounts to solving the following constraint:

$$
\exists \sigma^H \in R\_H. \forall \sigma\_1, \sigma\_2 \in R\_{in}. \left[ \left. s \right|\_{\sigma\_1 \cup \sigma^H, \sigma\_2} \neq \bot \dots \right]
$$

According to Theorem. 2, given a set of distinct primes P = {p1, ··· , pk} and variable valuations σH, σ1, and σ2, if there exists a range R of size N = p1 · ... ··· pk such that s ∈σ1∪σH,σ2 R, the modular semantics and the integer semantics are equivalent to each other. Using this observation, we can define the set of variable valuations for which the two semantics are guaranteed to be equivalent:

$$\mathcal{L}\_R^\mathbb{P} \coloneqq \left\{ (\sigma\_1, \sigma\_2) \mid \forall \sigma^H \in R\_H. \exists R. \ |R| = N \land s \in\_{\sigma\_1 \cup \sigma^H, \sigma\_2} R \right\} \dots$$

Since for every σH ∈ RH and σ1, σ2 ∈ IP R we have that sP σ1∪σH,mP◦σ2 = sσ1∪σH,σ2 , any solution to an IMP-MOD program in the modular semantics is also a solution to the following formula in the integer semantics:

$$\exists \sigma^H \in R\_H. \forall \sigma\_1, \sigma\_2 \in \mathcal{T}\_R^{\mathbb{P}}. \lbrack s \rbrack\_{\sigma\_1 \cup \sigma^H, \sigma\_2} \neq \bot.$$

When all valuations in σ1, σ2 ∈ Rin are also elements of IP R, any solution to an IMP-MOD program in the modular semantics is guaranteed to be a correct solution under the integer semantics.

To summarize, if the synthesizer returns UNSAT for the IMP-MOD program, the problem is unrealizable and does not admit a solution. When it returns a solution, the solution is correct if it only produces valuations in the range allowed by

```
Algorithm 2: Incremental synthesis for IMP-MOD.
```
/\* f: function, P: set of primes \*/ 1 function IncrementalSynthesis(f, P) 2 P- ← [p1] 3 fsyn ← Synthesis(f, P- ) 4 while ∃pcex ∈ P : ¬Verify(fsyn, pcex) do 5 P- ← P- ∪ pcex 6 fsyn ← Synthesis(f, P- ) 7 if fsyn == UNSAT then return ∅ ; 8 return fsyn

the choice of prime numbers. In practice, one can use a verifier to check the correctness of the synthesized solution and add more prime numbers to the modular synthesizer if needed. In fact, this is the main idea behind the counterexampleguided inductive synthesis algorithm used by Sketch (Section 3).

#### 6.2 Incremental Synthesis Algorithm

In this section, we propose an incremental synthesis algorithm that builds on the following observation. The set of variable valuations for which modular and integer semantics are equivalent increases monotonically in the size of P:

$$\mathbb{P}\_1 \subseteq \mathbb{P}\_2 \implies \mathcal{T}\_R^{\mathbb{P}\_1} \subseteq \mathcal{T}\_R^{\mathbb{P}\_2}.\tag{1}$$

Algorithm 2 uses Equation 1 to add prime numbers lazily during the synthesis process. The algorithm first constructs a set P = {p1} with the first prime number p1 ∈ P and synthesizes a solution that is correct for computations modulo the set P . It then checks if the synthesized solution fsyn satisfies the assertions with respect to all prime numbers in P. If yes, fsyn is returned as the solution. Otherwise, the algorithm finds a prime pcex ∈ P where Verify(fsyn, pcex) does not hold and it adds it to the set P continuing the iterative algorithm. Due to Equation 1, Algorithm 2 is sound and complete with respect to the synthesis algorithm that considers the full prime set P all at once.

In practice, the user could use domain knowledge to estimate a suitable set of primes or alternatively use our incremental algorithm to discover appropriate prime sets. The set of prime numbers {2, 3, 5, 7, 11, 13, 17} could usually instantiate a range R that is large enough for most synthesis tasks based on Sketch.

# 7 Complexity of Rewritten Programs

In this section, we analyze how many bits are necessary to encode numbers for both semantics using unary and binary bit-vector encodings of integers (Sec. 7.1 and 7.2), and show how many prime numbers are necessary in the modular semantics to cover values up to a certain bound (Sec. 7.3). The following results build upon several number theory results that the reader can consult at [9, 15].

#### 7.1 Bit-complexity of Binary Encoding

In this section, we analyze how many bits are necessary when representing an interval of size N in binary in our modular semantics. In the rest of the section, we consider the set of primes Pn = {p | p<n} = {p1,...,pk} containing the prime numbers that have value smaller than n. We will show in Section 8 that this choice of prime number also yields good performance in practice. Concretely, we are interested in knowing what is the magnitude of the number N = p1 ·...·pk and how many bits are used to represent the numbers in Pn.

We start by introducing the notion of primorial.

Definition 3 (Primorial). Given a number n, the primorial n# is defined as the product of all primes smaller than n—i.e., n# = - p∈Pn p.

The primorial captures the size N of the interval covered by the Chinese Remainder Theorem when using prime numbers up to n. The following number theory result gives us a close form for the primorial and shows that the number N has approximately n bits.

$$n\# = e^{(1+o(1))n} = 2^{(1+o(1))n} \tag{2}$$

We use another number theory notion to quantify the number of bits in Pn.

Definition 4 (Chebyshev function). Given a number n, the Chebyshev function ϑ(n) is the sum of the logarithms of all the prime numbers smaller than n—i.e., ϑ(n) = p∈Pn log p.

The following number theory result relates the primorial to the Chebyshev function.

$$\vartheta(n) = \log(n\#) = \log 2^{(1+o(1))n} = (1+o(1))n \tag{3}$$

Aside from rounding errors, the Chebyshev function captures the number of bits required to represent the numbers in Pn. To obtain a more precise bound on this number, we need a bound for the formula log p.

p∈Pn We start by recalling the following fundamental number theory result.

Theorem 4 (Prime number theorem). The set Pn has size approximately n/ log n.

Using Theorem 4, we get the following result.

$$\sum\_{p \in \mathbb{P}\_n} \lceil \log p \rceil \le n/\log n + \sum\_{p \in \mathbb{P}\_n} \log p \approx (1 + o(1))n \tag{4}$$

Representing a number en in a classic binary encoding requires log2(en) = (1 + o(1))n bits and, combining Equations 2 and 4, we get the following result.

Theorem 5. Representing a number 2n in binary requires (1+o(1))n bits under both modular and integer semantics.

Hence, representing a number in binary requires the same number of bits in the both semantics.

Example 7. Consider the set P18 = {2, 3, 5, 7, 11, 13, 17}, which can model an interval of N = 510, 510 integers (i.e., n = 18 in Theorem 5). Representing N in binary requires 19 bits while the binary representations of all the primes in P18 use 22 bits. Both numbers are close to 18 as predicted by the theorem.

# 7.2 Bit-complexity of Unary Encoding

As discussed in Sec. 3, the default Sketch solver encodes numbers using a unary encoding—i.e., Sketch requires 2n bits to encode the number 2n. Representing the same number in unary under the modular semantics requires only prime numbers smaller than n and therefore p∈Pn p bits. We can then use the following

closed form to approximate this quantity.

$$\sum\_{p \in \mathbb{P}\_n} p \sim \frac{n^2}{2\log n} \tag{5}$$

Equation 5 yields the following theorem.

Theorem 6. Representing a number 2n in unary requires 2n bits in the integer semantics and approximately n2 2 log n bits in the modular semantics.

These results show that, under a unary encoding, the modular semantics is exponentially more succinct than the integer semantics.

Example 8. Consider again the prime set P18 = {2, 3, 5, 7, 11, 13, 17}, which can model an interval of N = 510, 510 integers. Representing N in unary requires 510,510 bits. On the other hand, the sum of the bits in the unary encoding of the primes in P18 is 58.

#### 7.3 Number of Required Primes

We analyze how many primes are needed to represent a certain number in the modular semantics. We start by introducing the following alternative version of the primorial.

Definition 5 (Prime Primorial). For the n-th prime number pn, the prime primorial pn# is defined as the product of the first n primes—i.e., pn# = n k=1 pi.

The following known number theory result gives us an approximation for the prime primorial.

$$p\_n \# = e^{(1+o(1))n\log n} \tag{6}$$

Notice how the approximation of the primorial differs from that of the prime primorial. This is due to the fact that prime numbers are sparse—i.e., the n-th prime number is approximately n log n.

Using Equation 6 we obtain the following result.

Theorem 7. Representing numbers in an interval of size N = en log n in the modular semantics requires the first n prime numbers.

Since the relation k = n log n does not admit a closed form for n, we cannot derive exactly how many primes are needed to represent a number 2k with k bits. It is however clear from the theorem that the number of required primes grows slower than k.

# 8 Evaluation

We implemented a prototype of our technique as a simple compiler in Java. Our implementation provides a simplified Sketch frontend, which only allows the limited syntax we support. Given a Sketch file, our tool rewrites it into a different Sketch file that operates according to the modular semantics. We will use Unary to denote the result obtained by running the default version of Sketch with unary integer encoding on the original Sketch file, Binary to denote the result obtained by running the version of Sketch using an SMT-like native integer solver based on binary integer encoding, Unary-p to denote the result of running the default Sketch version on our modified Sketch file, and Unaryp-inc to denote the result of running the default version of Sketch on the file generated by the incremental version of our algorithm described in Section 6. As expected from our theory, the prime technique is not beneficial for the SMT-like native integer solver and always results in worse runtime. Therefore, we do not present data for this solver. All experiments were performed on a machine with 4.0GHz Intel Core i7 CPU with 16GB RAM with Sketch-1.7.5 and we use a timeout value of 300 seconds (we also report out-of-memory errors as timeouts).

Our evaluation answers the following research questions:

Q1 How does the performance of Unary-p compare to Unary and Binary?

Q2 How does the incremental algorithm compare to the non-incremental one?

Q3 Is Unary-p's performance sensitive to the set of selected prime numbers?

Q4 How many primes are needed by Unary-p to produce correct solutions?

Q5 Does Unary generate larger SAT queries than Unary-p?

#### 8.1 Benchmarks

We perform our evaluation on three families of programs.

Polynomials The first set of benchmarks contains 81 variants of the polynomial synthesis problem presented in Figure 1. The original version of this benchmark appears in the Sketch benchmark suite under the name polynomial.sk. For each benchmark, we generate a random polynomial f, random inputs {−→x }, and take the set {( −→x,f(x))} as specification. Each benchmark in this set has the following parameters: #Ex∈ {2, 4, 6} is the number of input-output examples as specification, cbits∈ {5, 6, 7} denote the number of bits hole values can use, exIn∈ {[−10, 10], [−30, 30], [−50, 50]} denotes the range of randomly generated input examples and coeff∈ {[−10, 10], [−30, 30], [−50, 50]} denotes the range of randomly generated coefficients in the polynomial f.

Invariants The second set of benchmarks contain 46 variants of two invariant generation problems obtained from a public set of programs that require polynomial invariants to be verified [8]. We selected the two programs in which at least one variable could be tracked modularly by our tool (the other programs involved complex array operations or inequality operators) and turned the verification problems into synthesis problems by asking Sketch to find a polynomial equality (using the program variables) that is an invariant for the loop in the program. To control the size of the magnitudes of the inputs, we only require the invariants to hold for a fixed set of input examples.

The first problem, mannadiv, iteratively computes the remainder and the quotient of two numbers given as input. The invariant required to verify mannadiv is a polynomial equality of degree 2 involving 5 variables. The Sketch template required to describe the space of all polynomial equalities has 32 holes and cannot be handled by any of the Sketch solvers we consider. We therefore simplify the invariant synthesis problems in two ways. In the first variant, we reduce the ranges of the hole values in the templates by considering cbits ∈ {2, 3}. In the second variant, we set cbits = {5, 6, 7}, but reduce the number of missing hole values to 4 (i.e., we provide part of the invariant). Each benchmark takes two random inputs and we consider the following input ranges {[1, 50], [1, 100]}. In total, we have 10 benchmarks for mannadiv.

The second problem, petter, iteratively computes the sum 1≤i≤n i 5 for a given input n. The invariant required to verify petter is a polynomial equality of degree 6 involving 3 variables. The Sketch template required to describe all such polynomial equalities has 56 holes and cannot be handled by any of the Sketch solvers we consider. We consider the following simplified variants of the problem: (i) petter\_0 computes 1≤i≤n 1 and requires a polynomial invariant of degree one, (ii) petter\_x computes 1≤i≤n x for a given input variable x and requires a polynomial invariant of degree two, ( iii) petter\_1 computes 1≤i≤n i and requires a polynomial invariant of degree two, and (iv) petter\_10 computes 1≤i≤n i + 1 and requires a polynomial invariant of degree two. Each benchmark takes two random inputs and we consider the following input ranges {[1, 10], [1, 100], [1, 1000]}. In total, we have 12 variants of petter, each run for values of cbits ∈ {5, 6, 7}—i.e., a total of 36 benchmarks.

Program Repair The third set of benchmarks contains 54 variants of Sketch problems from the domain of automatic feedback generation for introductory programming assignments [7]. Each benchmark corresponds to an incorrect program submitted by a student and the goal of the synthesizer is to find a small variation of the program that behaves correctly on a set of test cases. We select the 6/11 benchmarks from the tool Qlose [7] for which (i) our implementation can support all the features in the program, and (ii) our data flow analysis identifies at least one variable that can be tracked modularly. Of the remaining benchmarks, 3/11 do not contain variables that can be tracked modularly, and 2/11 call auxiliary functions that cannot be translated into Sketch. For each Table 1: Effectiveness of different solvers. SAT (resp. UNSAT) denotes the number of benchmarks for which solver could find a solution to the benchmarks (resp. prove no solution existed) while TO denotes the number of timeouts.

program, we consider the original problem and two variants where the integer inputs are multiplied by 10 and 100, respectively. Further, for each program variants, we impose an assertion specifying that the distance between the original program and the repaired program is within a certain bound. We select three different bounds for each program: the minimum cost c, c + 100, and c + 200.

# 8.2 Performance of Unary-p

Table 1 summarizes our comparison. First, we compare the performance of Unary-p and Unary. We use P = {2, 3, 5, 7, 11, 13, 17}, which is enough for Unary-p to always find correct solutions (we verify the correctness of a solution by instantiating the hole values in the original sketch programs). Unary can only solve 69/181 benchmarks while Unary-p can solve 169/181. Figure 7a shows a scatter plot (log scale) of the solving times for the two techniques: each point below the diagonal line denotes a benchmark on which Unary-p was faster than Unary. Points on the extreme right-hand side of the plot denote timeout for Unary. When both solvers terminate, Unary-p (avg. 1.7s) is 6.1X (geometric mean) faster than Unary (avg. 25.0s).

Next, we compare the performance of Unary-p and Binary (Figure 7b). On the 64 easier benchmarks that Binary can solve in less than 1 second, Binary (avg. 0.55s) outperforms Unary-p (avg. 2.32s), but Unary-p still has reasonable performance. On the 49 benchmarks that Binary can solve between 1 and 10 seconds, Unary-p (avg. 3.5s) is on average 1.9X faster than Binary (avg. 6.9s). Most interestingly, for the 14 harder benchmarks for which Binary takes more than 10 seconds, Unary-p (avg. 5.7s) is on average 15.9X faster than Binary (avg. 90.9s). Remarkably, Unary-p solved 43 of the benchmarks (in less than 8s each) for which Binary timed out4, and Unary-p only timed out for two benchmarks that Binary could solve in less than a second and one benchmark that Binary could solve in 260s. Finally, we would like to highlight that for 41/208 benchmarks, even Unary outperforms Binary. As expected from

4 During our experiment, we observed that Binary *incorrectly* reported UNSAT for 10 satisfiable benchmarks. We reported these benchmarks as timeouts and have contacted the authors of Sketch to address the issue.

the discussion throughout the paper, these are benchmarks typically involving complex operations but not involving overly large numbers.

We can now answer Q1. First, Unary-p consistently outperforms Unary across all benchmarks. Second, Unary-p outperforms Binary on hard-tosolve problems and can solve problems that Binary cannot solve e.g., Unary-p solved 28/46 invariant problems that Sketch could not solve. Unary-p and Binary have similar performance on easy problems.

Comparison to full SMT encoding For completeness, we also compare our approach to a tool that uses SMT solvers to model the entire synthesis problem. We choose the state-of-the-art SMT-based synthesizer Rosette [23] for our comparison. Rosette is a programming language that encodes verification and

synthesis constraints written in a domainspecific language into SMT formulas that can be solved using SMT solvers.

We only run Rosette on the set of Polynomials because Rosette does support the theories of integers, but does not have native support for loops, so there is no direct way to encode Invariants and Program Repair benchmarks. To our knowledge, Rosette provides a way to specify the number k it uses to model integers and reals as k-bit words, but the user has no control over how many bits it uses for unknown holes specifically. So

Fig. 6: Rosette vs Binary

we evaluate 27 instead of 81 variants of the polynomial synthesis problem on Rosette, i.e., we consider different numbers of cbits.

Figure 6 shows the running times (log scale) for Rosette and Binary with cbits=6. Rosette successfully solved 16/27 benchmarks and it terminates quickly (avg. 2.9s) when it can find a solution. However, Rosette times out on 11 benchmarks for which Binary terminates. The timeouts are due to the fact that Rosette employs full SMT encodings that combine multiple theories while Binary uses a SAT solver that is only modified to accommodate SMT-like integer constraints. Since we now know full SMT encodings are not as general and efficient as the encodings used in Sketch, we will only evaluate the effectiveness of our technique based on comparison with Binary.

Finally, we tried applying our prime-based technique to Rosette and, as expected, the technique is not beneficial due to the binary encoding of numbers in SMT, and causes all benchmarks to timeout. To summarize, (i) SMT solvers cannot efficiently handle the synthesis problems considered in this paper, and (ii) our technique is better suited for SAT solvers than SMT solvers.

#### 8.3 Performance of Incremental Solving

Our implementation of the incremental solver Unary-p-inc first attempts to find a solution with the prime set P = {2, 3, 5, 7}. If the solver returns a correct

Fig. 7: Performance of Unary, Binary, and Unary-p.

solution, Unary-p-inc terminates. Otherwise, Unary-p-inc incrementally adds the next prime to P until it finds a correct solution, it proves there is no solution, or it times out. Unary-pinc is 25.2% (geometric mean) slower than Unary-p (Figure 8 (log scale)). Unary-p-inc can solve three benchmarks for which both Unary-p and Binary timed out. To answer Q3, Unary-p-inc and Unary-p have similar performance.

Fig. 8: Unary-p-inc vs Unary-p

# 8.4 Varying the Prime Number Set P

In this experiment, we evaluate how different prime number sets affect Unary-p.

We consider the 5 increasing sets of primes: P5 = {2, 3, 5}, P7 = {2, 3, 5, 7}, P11 = {2, 3, 5, 7, 11}, P13 = {2, 3, 5, 7, 11, 13}, and P17 = {2, 3, 5, 7, 11, 13, 17}. Figure 9a (log scale) shows the running times for all the polynomial benchmarks with cbits=7 (showing all benchmarks would clutter the plot). The points where the lines change from dashed to solid denote the number of primes for which the algorithm starts yielding correct solutions. As expected, a smaller set of primes leads to faster solving times as the resulting constraints are smaller and fewer bits are needed for encoding intermediate values. The runtime on average grows with the increasing size of the primes. For example, across all benchmarks, using P17 takes 23% longer on average than using P11. To answer Q3, Unary-p is slower when using increasingly large sets of prime.

In terms of correctness, we find that smaller prime sets often yield incorrect solutions (P5 (37% correct), P7 (70%), P11 (86%), P13 (97 %), and P17 (100%) because there is not enough discriminative power with fewer primes and the

Fig. 9: Performance for different sets of prime numbers.

solutions may overfit to the smaller set of intermediate values. It is interesting to note that even prime sets of intermediate size often lead to correct solutions in practice, which explains some of the speedups observed in the incremental synthesis algorithm. To answer Q4, Unary-p is able to synthesize correct solutions even with intermediate sized sets of primes.

Changing Magnitude of Primes We also evaluate the performance of Unaryp when using primes of different magnitudes. We consider the sets of primes {11, 17, 19, 23}, {31, 41, 47}, and {251, 263}, which define similar integer ranges, but pose different trade-offs between the number of used primes and their sizes e.g., the set {251, 263} only uses two very large primes. Since the different sets cover similar integer ranges, they all produce correct solutions. Figure 9b (log scale) shows the running time of Unary-p for the same benchmarks as Figure 9a. Larger prime sets of smaller prime values require less time to solve than smaller prime sets of larger prime values. This result is expected since, in the unary encoding of numbers, representing larger numbers requires more bits.

#### 8.5 Size of SAT Formulas

In this experiment, we compare the sizes of the intermediate SAT formulas generated by Unary-p and Unary. Figure 10a shows a scatter plot (log scale) of the number of clauses of the largest intermediate SAT query generated by the CEGIS algorithm for the two techniques. We only plot the instances in which Unary was able to produce at least a SAT formula. Unary produces SAT formulas that are on average 19.3X larger than those produced by Unary-p. To answer Q5, as predicted by our theory, Unary-p produces significantly smaller SAT queries than Unary.

Performance vs Size of SAT Queries We also evaluate the correlation between synthesis time and size of SAT queries. Figure 10b plots the synthesis times of both solvers against the sizes of the SAT queries. It is clear that the synthesis

Fig. 10: SAT formulas sizes and performance.

time increases with larger SAT queries. The plot illustrates how the solving time strongly depends on the size of the generated formulas.

# 9 Related Work

Program Sketching Program sketching was designed to automatically synthesize efficient bit-vector manipulations from inefficient iterative implementations [21]. The Sketch tool has since been engineered to support complex language features and operations [19]. Thanks to its simplicity, sketching has found wide adoption in applications such as optimizing database queries [3], automated feedback generation [18], program repair [7], and many others. Our work further extends the capabilities of Sketch in a new direction by leveraging number theory results. In particular, our technique allows Sketch to handle sketches manipulating large integer numbers. To the best of our knowledge, our technique is the first one that can solve many of the benchmarks presented in this paper. Uses of Chinese Remainder Theorem The Chinese Remainder Theorem and its derivative corollaries have found wide application in several branches of Computer Science and, in particular, in Cryptography [11, 26].

The idea of using modular arithmetic to abstract integer values has been used in program analysis. Since modular fields are finite, they can be used as an abstract domain for verifying programs manipulating integers [5]—e.g., the abstract domain can track whether a number is even or odd. Our work extends this idea to the domain of program synthesis and requires us to solve several challenges. First, when used for verifying programs, the modular abstraction is used to overapproximate the set of possible values of the program and does not need to be precise. In particular, Clark et al. [5] allow program operations that are in the IMP language but not in the IMP-MOD language and lose precision when modeling such operations—e.g., when performing the assignment x = x/2 the value of x mod 2 can be either 0 or 1. Such imprecision is fine in program analysis since the abstraction is used to show that a program does not contain a bug i.e., even in the abstract domain, the problem behaves fine. In our setting, the problem is opposite as we use the abstraction to simplify the synthesis problem and provide a theory for when the modular and integer semantics are equivalent.

Pruning Spaces in Program Synthesis Many techniques have been proposed to prune large search space of possible programs [14]. Enumerative synthesis techniques [24, 12, 13, 17] enumerate programs in a search space and avoid enumerating syntactically and semantically equivalent terms. Some synthesizers such as Synquid [16] and Morpheus [10] use refinement types and first-order formulas over specifications of DSL constructs to refute inconsistent programs. Recently, Wang et al. [25] proposed a technique based on abstraction refinement for iteratively refining abstractions to construct synthesis problems of increasing complexity for incremental search over a large space of programs.

Instead of pruning programs in the syntactic space, our technique uses modular arithmetic to prune the semantic space—i.e., the complexity of verifying the correctness of the synthesized solution—while maintaining the syntactic space of programs. Our approach is related to that of Tiwari et al. [22], who present a technique for component-based synthesis using dual semantics—where syntactic symbols in a language are provided two different semantics to capture different requirements. Our technique is similar in the sense that we also provide an additional semantics based on modular arithmetic. However, we formalize our analysis based on number theory results and develop it in the context of generalpurpose Sketch programs that manipulate integer values, unlike Tiwari et al.'s work that is developed for straight-line programs composed of components.

Synthesis for Large Integer Values Abate et al. propose a modification of the Cegis algorithm for solving syntax-guided synthesis (SyGuS) problems with large constants [1]. SyGuS differs from program sketching in how the synthesis problem is posed and in the type of programs that can be modeled. In particular, in SyGuS one can only describe programs representing SMT formulas and the logical specification for the problem can only relate the input and output of the program—i.e., there cannot be intermediate assertions within the program. The problem setup and the solving algorithms proposed in this paper are orthogonal to those of Abate et al. First, we focus on program sketching, which is orthogonal to SyGuS as sketching allows for richer and more generic program spaces as well as richer specifications. While it is true that certain synthesis problems can be expressed both as sketches and as SyGuS problems, this is not the case for our benchmarks programs, which use loops, arrays and non-linear integer arithmetic, all of which are not supported by SyGuS. Second, our technique is motivated by how Sketch encodes and solves program sketches through SAT solving. While the traditional Sketch encoding can explode for large constants, the same encoding allows Sketch to solve program sketches involving complex arithmetic and complex programming constructs. The algorithm proposed by Abate et al. iteratively builds SMT (not SAT) formulas that are required to be in a decidable logical theory. Such an encoding only works for the restricted programming models used in SyGuS problems.

# References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

#### **Modular Relaxed Dependencies in Weak Memory Concurrency***-*

Marco Paviotti12, Simon Cooksey2, Anouk Paradis3, Daniel Wright2, Scott Owens2, and Mark Batty2

1 Imperial College London, United Kingdom<EMAIL_ADDRESS>2 University of Kent, Canterbury, United Kingdom {m.paviotti, sjc205, daw29, S.A.Owens<EMAIL_ADDRESS>3 ETH Zurich, Switzerland<EMAIL_ADDRESS>
**Abstract.** We present a denotational semantics for weak memory concurrency that avoids thin-air reads, provides data-race free programs with sequentially consistent semantics (DRF-SC), and supports a compositional refinement relation for validating optimisations. Our semantics identifies false program dependencies that might be removed by compiler optimisation, and leaves in place just the dependencies necessary to rule out thin-air reads. We show that our dependency calculation can be used to rule out thin-air reads in any axiomatic concurrency model, in particular C++. We present a tool that automatically evaluates litmus tests, show that we can augment C++ to fix the thin-air problem, and we prove that our augmentation is compatible with the previously used compilation mappings over key processor architectures. We argue that our dependency calculation offers a practical route to fixing the longstanding problem of thin-air reads in the C++ specification.

**Keywords:** Thin-air problem · Weak memory concurrency · Compiler Optimisations · Denotational Semantics · Compositionality

# **1 Introduction**

It has been a longstanding problem to define the semantics of programming languages with shared memory concurrency in a way that does not allow unwanted behaviours – especially observing *thin-air* values [8,7] – and that does not forbid compiler optimisations that are important in practice, as is the case with Java and Hotspot [30,29]. Recent attempts [16,11,25,15] have abandoned the style of *axiomatic models*, which is the de facto paradigm of industrial specification [8,2,6]. Axiomatic models comprise rules that allow or forbid individual program executions. While it is impossible to solve all of the problems in an

- This work was funded by EPSRC Grants EP/M017176/1, EP/R020566/1 and EP/S028129/1, the Lloyds Register Foundation, and the Royal Academy of Engineering.

axiomatic setting [7], abandoning it completely casts aside mature tools for automatic evaluation [3], automatic test generation [32], and model checking [23], as well as the hard-won refinements embodied in existing specifications like C++, where problems have been discovered and fixed [8,7,18]. Furthermore, the industrial appetite for fundamental change is limited. In this paper we offer a solution to the thin-air problem that integrates with existing axiomatic models.

The thin-air problem in C++ stems from a failure to account for dependencies [22]: *false dependencies* are those that optimisation might remove, and *real dependencies* must be left in place to forbid unwanted behaviour [7]. A single execution is not sufficient to discern real and false dependencies. A key insight from previous work [14,15] is that event structures [33,34] give us a simultaneous overview of all traces at once, allowing us to check whether a write is sure to happen in every branch of execution. Unfortunately, previous work does not integrate well with axiomatic models, nor lend itself to automatic evaluation.

To address this, we construct a denotational semantics in which the meaning of an entire program is constructed by combining the meanings of its subcomponents via a compositional function over the program text. This approach can be particularly amenable to automatic evaluation, reasoning and compiler certification [19,24], and fits with the prevailing axiomatic approach.

This paper uses this denotational approach to capturing program dependencies to explore the thin-air problem, resulting in a concrete proposal for fixing the thin-air problem in the ISO standard for C++.

*Contributions.* There are two parts to the paper. In the first, we develop a denotational model called "Modular Relaxed Dependencies model" (MRD) and build metatheory around it. The model uses a relatively simple account of synchronisation, but it demonstrates separation between the calculation of dependency and the enforcement of synchronisation. In the second, we evaluate the dependency calculation by combining it with the fully-featured axiomatic models RC11 [18] and IMM [26].

The denotational semantics has the following advantages:

We adopt the dependency calculation from the global semantics of point 4 as the basis of our C++ model, which we call MRD-C11. We establish the C++ DRF-SC property described in the standard [13] (§9.1) and we provide several desirable properties for a solution to the thin-air problem in C++:

#### **1.1 Modular Relaxed Dependency by example**

To simplify things for now, we will attach an Init program to the beginning of each example to initialise all global variables to zero. Doing this makes the semantics non-compositional, but it is a natural starting place and aligns well with previous work in the area. Later, after we have made all of our formal definitions, we will see why the Init program is not necessary.

For now, consider a simple programming language where all values are booleans, registers (ranging over r) are thread-local, and variables (ranging over x, y) are global. Informally, an event structure for a program consists of a directed graph of events. Events represent the global variable reads and writes that occur on all possible paths that the program can take. This can be built up over the program as follows: each write generates a single event, while each read generates two – one for each possible value that could be read. These read events are put in *conflict* with each other to indicate that they cannot both happen in a single execution, this is indicated with a zig-zag red arrow between the two events. Additionally, the event structure tracks true dependencies via an additional relation which we call *semantic dependencies* (dp). These are yellow arrows from read events to write events.

For example, consider the program

$$(\mathbf{r}\_1 := \mathbf{x}; \; \mathbf{y} := \mathbf{r}\_1) \tag{LB\_1}$$

that reads from a variable x and then writes the result to y. The interpretation of this program is an event structure depicted as follows:

Each event has a unique identifier (the number attached to the box). The straight black arrows represent program order, the curved yellow arrows indicate a causal dependency between the reads and writes, and the red zigzag represents a conflict between two events. If two events are in conflict, then their respective continuations are in conflict too.

If we interpret the program Init; LB1, as below, we get a program where the Init event sets the variables to zero.

In the above event structure, we highlight events {1, 2, 3} to identify an execution. The green dotted arrow indicates that event 2 reads its value from event 1, we call this relation *reads-from* (rf). This execution is *complete* as all of its reads read from a write and it is closed w.r.t conflict-free program order.

We interpret the following program similarly,

$$\{\mathbf{r}\_2 \colon \mathbf{\color{red}{y} : x \mathrel{\begin{array}{c} = \mathbf{r}\_2 \ \\ \cdot \end{array}}\} \tag{LB\_2}$$

leading to a symmetrical event structure where the write to x is dependent on the read from y.

The interpretation of Init; (LB1 - LB2) gives the event structure where (LB1) and (LB2) are simply placed alongside one another.

The interpretation of parallel composition is the union of the event structures from LB1 and LB2 without any additional conflict edges. When parallel composing the semantics of two programs, we add all rf-edges that satisfy a coherence axiom. Here we present an axiom that provides desirable behaviour in this example (Section 4 provides our model's complete axioms).

(dp ∪ rf) is acyclic

The program Init; (LB1 - LB2) allows executions of the following three shapes.

Note that in this example, we are not allowed to read the value 1 – reading a value that does not appear in the program is one sort of thin-air behaviour, as described by Batty et al. [7]. For example, the execution {1, 4, 5, 8, 9} does not satisfy the coherence axiom as 4 dp −→ 5 rf −→ 8 dp −→ 9 rf −→ 4 forms a cycle.

We now substitute (LB2) with the following code snippet

$$\mathbf{r}\_1 \colon= \mathbf{y}; \; \mathbf{x} \; := 1 \tag{L B\_3}$$

where the value written to the variable x is a constant. Its generated event structure is depicted as follows

In this program, for each branch, we can reach a write of value 1 to location x. Hence, this will happen no matter which branch is chosen: we say b and d are *independent writes* and we draw no dependency edges from their preceding reads.

Consider now the program (LB3) in parallel with LB1 introduced earlier in this section. As usual, we interpret the Init program in sequence with (LB1 - LB3) as follows:

The resulting event structure is very similar to that of (LB1 - LB2), but the executions permitted in this event structure are different. The dependency edges calculated when adding the read are preserved, and now executions {1, 2, 3, a, b} and {1, a, b, 4, 5} are allowed. However, this event structure also contains the execution in which d is independent.

In the execution {d rf −→ 4 dp −→ 5 rf −→ c} there is no rf or dp edge between d and c that can create a cycle, hence this is a valid complete execution in which we can observe x = 1, y = 1. Note that the Init is irrelevant in the consistency of this execution.

*Modularity.* It is worthwhile underlining the role that modularity plays here. In order to compute the behaviour of (LB1 - LB2) and (LB1 - LB3) we did not have to compute the behaviour of LB1 again. In fact, we computed the semantics of LB1, LB2 and LB3 in isolation and then we observed the behaviour in parallel composition.

*Thin-air values.* The program (LB1 - LB3) is a standard example in the weak memory literature called *load buffering*. In the program (LB1 - LB2), if event 5 or 9 were allowed in a complete execution, that would be an undesirable thin-air behaviour: there is no value 1 in the program text, nor does any operation in the program compute the value 1. The program (LB1 - LB3) is similar, but now contains a write of value 1 in the program text, so this is no longer a thin-air value. Note that the execution given for it is not sequentially consistent, but nonetheless a weak memory model needs to allow it so that a compiler can, for example, swap the order of the two commands in LB3, which are completely independent of each other from its perspective.

# **2 Event Structures**

Event structures will form the semantic domain of our denotational semantics in Section 5. Our presentation follows the essential ideas of Winskel [33] and is further influenced by the treatment of shared memory by Jeffrey and Riely [15].

#### **2.1 Background**

A partial order (E, ) is a set E equipped with a reflexive, transitive and antisymmetric relation . A well-founded partial order is a partial order that has no infinite decreasing chains of the form ··· ei−1 ei ei+1 ··· .

A *prime event structure* is a triple (E, , #). E is a set of events, is a well-founded partial order on E and # is a conflict relation on E. # is binary, symmetric and irreflexive such that, for all c, d, e ∈ E, if c#d e then c#e. We write Con(E) for the set of *conflict-free* subsets of E, *i.e.* those subsets C ⊆ E for which there is no c, d ∈ C such that c#d.

*Notation.* We use E to range over (prime/labelled/memory) event structures, and also the event set contained within, when there is no ambiguity. We also use E for event structures.

A *labelled event structure* (E, , #, λ), over a set of labels Σ, is a prime event structure together with a function λ : E → Σ which assigns a label to an event. We make events explicit using the notation {e : σ} for λ(e) = σ. We sometimes avoid using names and just write the label σ when there is no risk of confusion.

Consider the labelled event structure formed by the set {1, 2, 3, 4}, where the order relation is defined such that 1 2 3 and 1 4, the conflict relation is defined such that 2#4 and 3#4, and the labelling function is defined such that λ(1) = (W x 0), λ(2) = (R x 0), λ(3) = (W y 1) and λ(4) = (R x 1). The event structure is visualised on the left (we elide conflict edges that can be inferred from order).

Given labelled event structures E1 and E2 define the *product* labelled event structure E1×E2 - (E, , #, λ). E is E1∪E2, assuming E1 and E2 to be disjoint, is 1 ∪ 2, # is #1 ∪ #2 and λ is λ1 ∪ λ2.

The *coproduct* labelled event structure E1 + E2 is the same as the product, except that the conflict relation # is #1 ∪ #2 ∪ {E1 × E2}∪{E2 × E1}. We can use a similar construction for the co-product of an infinite set of pairwisedisjoint labelled event structures, indexed by I: we take infinite unions on the underlying sets and relations, along with extra conflicts for every pair of indices. Where the Ei are not disjoint, we can make them so by renaming with fresh event identifiers. In particular, we will need the infinite coproduct - i∈I E with as many copies of E as the cardinality of the set I, and all the events between each copy in conflict. Each of these copies will by referred to as Ei .

For a labelled event structure E0 and an event e, where e ∈ E0, define the *prefix* labelled event structure, e • E0, as a labelled event structure (E, , #, λ) where E equals E0 ∪ {e}, equals 0 ∪ ({e} × E), and # equals #0.

#### **2.2 The fork-join event structure**

Our language supports parallel composition nested under sequential composition, so we will need to model spawning threads and a subsequent wait for their termination. To support this, we define the *fork-join* composition of two labelled event structures, E1 E2. First we define the leaves, ↓ (E), as the -maximal elements of E. Let I be the set of maximal conflict-free subsets of ↓ (E1). Intuitively, each event set in I corresponds to the last events4 of one way of executing the concurrent threads in E1. We then generate a fresh copy of E2 for each of the executions: E3 = - i∈I E2.

Now E1 E2 - (E, , #, λ) such that E is E1∪E3, # is #1∪#3, λ is λ1∪λ3, is the transitive closure of

$$\subseteq\_1 \cup \subseteq\_3 \cup \bigcup\_{i \in I} \{ (e, e') \mid e \in i \land e' \in \mathcal{E}\_2^E \} $$

The set of events, E, is the set E1 plus all the elements from the copies of E3. The order, , is constructed by linking every event in the copy Ei 2, with all the events in the set i, plus the obvious order from E1 and the order in the local copy Ei 2. Finally, the conflict relation is the union of the conflict in E1 and E3.

# **3 Coherent event structure**

The signature of labels, Σ, is defined as follows:

$$\Sigma = (\{\mathbf{R}, \mathbf{W}\} \times \mathcal{X} \times \mathcal{V}) + \{\mathbf{L}\} + \{\mathbf{U}\},$$

where (W x v) ∈ Σ and (R x v) ∈ Σ are the usual write and read operations and L, U are the lock and unlock operations respectively.

A *coherent event structure* is a tuple (E, S, , ≤) where E is a labeled event structure. S is a set of *partial executions*, where each execution is a tuple comprising a maximal conflict-free set of events, together with an intra-thread reads-from

4 We assume that there are no infinite increasing --chains in E1.

relation rfi, an extra-thread reads-from rfe, a dependency relation dp, and a *partial order* on lock/unlock events lk. The justification relation, , is a relation between conflict-free sets and events. Finally, the *preserved program order*, ≤X , is a restriction of the program order, , for events on the same variable. ≤L is the restriction of program order on events related in program order with locks or unlocks. Finally, we define rf to be rfe ∪ rfi and ≤ to be ≤X ∪ ≤L. For a partial execution, X ∈ S, we denote its components as lkX, rfX and dpX.

Justification, , collects dependency information in the program and is used to calculate dpX. For a conflict-free set C and an event e, we say C *justifies* e or e *depends* on C whenever C e. We collect dependencies between events modularly in order to identify the so-called independent writes which will be introduced shortly.