Verifying Semantic Conflict-Freedom in Three-Way
Program Merges
Marcelo Sousa

Isil Dillig

Shuvendu Lahiri

University of Oxford
United Kingdom
marcelo.sousa@cs.ox.ac.uk

University of Texas at Austin
United States
isil@cs.utexas.edu

Microsoft Research
United States
shuvendu.lahiri@microsoft.com

arXiv:1802.06551v1 [] 19 Feb 2018

Abstract

Base:

Even though many programmers rely on 3-way merge tools
to integrate changes from different branches, such tools can
introduce subtle bugs in the integration process. This paper aims to mitigate this problem by defining a semantic
notion of conflict-freedom, which ensures that the merged
program does not introduce new unwanted behaviors. We
also show how to verify this property using a novel, compositional algorithm that combines lightweight dependence
analysis for shared program fragments and precise relational
reasoning for the modifications. We evaluate our tool called
SafeMerge on 52 real-world merge scenarios obtained from
Github and compare the results against a textual merge tool.
The experimental results demonstrate the benefits of our
approach over syntactic conflict-freedom and indicate that
SafeMerge is both precise and practical.

1

Variant A:

int f(int x) {
return x;
}

int f(int x) {
x++;
return x;
}

Variant B:
int f(int x) {
x++;
return x;
}

Incorrect merge:
int f(int x) {
x++;
x++;
return x;
}

Figure 1. Simple motivating example
different than what either developer intended, we see that a
bug was introduced during the merge.
This paper takes a step towards eliminating bugs that arise
due to 3-way program merges by automatically verifying
semantic conflict-freedom, a notion inspired by earlier work
on program integration [25, 43]. To motivate what we mean
by semantic conflict-freedom, consider a base program P, two
variants A, B, and a merge candidate M. Intuitively, semantic
conflict freedom requires that, if variant A (resp. B) disagrees
with P on the value of some program variable v, then the
merge candidate M should agree with A (resp. B) on the value
of v. In addition to ensuring that the merge candidate does
not introduce new behavior that is not present in either of the
variants, conflict freedom also ensures that variants A and
B do not make changes that are semantically incompatible
with each other.
The main contribution of this paper is a novel compositional verification algorithm, and its implementation in a
tool called SafeMerge, for automatically proving semantic
conflict-freedom. Our method is compositional in that it analyzes different modifications to the program in isolation
and composes them to obtain an overall proof of semantic
conflict-freedom. A key idea that allows compositionality is
to model different versions of the program using edits applied
to a shared program with holes. Specifically, the shared program captures common statements between the program versions, and holes represent discrepancies between them. The
edits describe how to fill each hole in the shared program to
obtain the corresponding statement in a variant. Given such
a representation that is automatically generated by SafeMerge, our verification algorithm uses lightweight analysis
to reason about shared program fragments but resorts to
precise relational techniques to reason about modifications.
The overall workflow of our approach is illustrated schematically in Figure 2. Our method takes as input four related
programs, namely the original program P, two variants A
and B, and a merge candidate M, and represents them as edits

Introduction

Developers who edit different branches of a source code
repository rely on 3-way merge tools (like git-merge or
kdiff3) to automatically merge their changes. Since the vast
majority of these tools are oblivious to program semantics
and resolve conflicts using syntactic criteria, they may introduce bugs in the merge process. For example, many people
speculate that Apple’s infamous goto fail SSL bug was
introduced due to an erroneous program merge [15, 28, 38].
To see how bugs may be introduced in the merge process,
consider the simple base program shown in Figure 1 together
with its two variants A and B.1 Here, both A and B modify
the original program by incrementing variable x by 1. For
instance, such a situation may arise in practice when two
independent developers simultaneously fix the same bug
in different locations of the original program. Since both
variants effectively make the same change, the correct merge
should be either A or B. However, running a 3-way merge tool
(in this case, kdiff3) on these programs succeeds without
any warnings and generates the incorrect merge shown on
the right hand side of Figure 1. Since this program is clearly
1 The

example is inspired by the Apple SSL bug that resulted from duplicate
goto statements.
PL’17, January 01–03, 2017, New York, NY, USA
2017.
1

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri

P
A
B
M

4-way
diﬀ

Edit1

Shared

Edit3

Edit2

VC
Gen

Mini
product

Edit4

Figure 2. High-level overview of our approach

applied to a shared program by running a “4-way diff" algorithm on the abstract syntax trees. The verifier leverages the
result of the 4-way diff algorithm to identify which parts of
the program to analyze more precisely. Specifically, our verification algorithm summarizes shared program fragments
using uninterpreted functions of the form x = f (x 1 , . . . , x n )
that encode dependencies between program variables. In contrast, the verifier reasons about edited program fragments in
a more fine-grained way by constructing 4-way product programs that encode the simultaneous behavior of all four edits. Overall, this interplay between lightweight dependence
analysis and product construction allows our technique to
generate verification conditions whose complexity depends
on the size and number of the edits.
To evaluate our technique, we collect over 50 real-world
merge scenarios obtained by crawling Github commit histories and evaluate SafeMerge on these benchmarks. Our tool
is able to verify the correctness of the merge candidate in
75% of the benchmarks and identifies eleven real violations
of semantic conflict-freedom, some of which are not detected
by textual merge tools. Our evaluation also demonstrates
the scalability of our method and illustrates the advantages
of performing compositional reasoning.
In all, this paper makes the following key contributions:

1
2
3
4
5
6
7
8
9
10
11
12

int time; int value ;
void triggerActions (long targetTimeInNanos ) {
while (! queue . isEmpty ()){
TimedAction current = queue .peek ();
if( current .time > targetTimeInNanos ){
time = targetTimeInNanos ;
break;
}
time = current .time;
queue . remove ();
current . action .call( current .scheduler , current .state );
} }

Figure 3. Procedure from the base program in RxJava.
• Variant A moves the statement time = targetTimeInNanos
at line 6 to immediately after the while loop. This modification impacts the value of the variable time in A with
respect to the Base version.
• Variant B guards the call current.action.call(...) at
line 11 with a condition if(!current.isCancelled.get())
{...}. The call (at line 11) has a side effect on the variable
called value (we omit the implementation of this procedure). This modification changes the effect on value with
respect to the Base version.
• The merge M incorporates both of these changes.
This example is interesting in that both variants modify
code within a loop, and one of them (namely, B) changes
the control-flow by introducing a conditional. The loop in
turn depends on the state of an unbounded collection queue,
which is manipulated using methods such as queue.isEmpty
and queue.remove. Furthermore, while triggerActions has
no return value, it has implicit side-effects on variables time
and value, and on the collection queue. Together, these features make it challenging to ensure that the merge M preserves changes from both variants and does not introduce
any new behavior.
To verify semantic conflict-freedom, our techinque represents the changes formally using a list of edits over a shared
program with holes. Figure 4 shows the shared program Ŝ
along with the corresponding edits ∆ O , ∆ A , ∆ B , ∆ M . A hole
(denoted as <?HOLE?>) in Ŝ is a placeholder for a statement.
The shared program captures the statements that are common to all the four versions (O, A, B and M), and the holes
in Ŝ represent program fragments that differ between the
program versions. An edit ∆ P for program version P represents a list of statements that will be substituted into the
holes of the shared program to obtain P.
Given this representation, we express semantic conflictfreedom as an assertion for each of the return variables (in
this case, global variables modified by the triggerActions

• We introduce the merge verification problem based on the
notion of semantic conflict-freedom.
• We provide a compositional verification algorithm that
combines precise relational reasoning about the edits with
lightweight reasoning for unedited program fragments.
• We present a novel n-way product construction technique
for precise relational verification.
• We describe an n-way AST diff algorithm and use it to
represent program versions as edits applied to a shared
program with holes.
• We implement our method in a tool called SafeMerge
and evaluate our approach on real-world merge scenarios
collected from Github repositories.

2

Veriﬁer

Overview

In this section, we give an overview of our approach with the
aid of a merge example from the RxJava project 2 . Figure 3
shows the Base version (O) of the triggerActions method
from the TestScheduler.java file. The two variants A, B
and the merge M perform the following modifications:
2 https://github.com/ReactiveX/RxJava/commit/1c47b0c.

2

Verifying Semantic Conflict-Freedom in Three-Way Program Merges
Shared program with holes (Ŝ)

PL’17, January 01–03, 2017, New York, NY, USA

:= (Ŝ, ∆)
:= [ ] | S :: ∆
:= [·] | A | Ŝ1 ; Ŝ2 | C ? {Ŝ1 } : {Ŝ2 }
|
while(C) {Ŝ}
Stmt
S
:= A | S1 ; S2 | C ? {S1 } : {S2 }
|
while(C) {S}
Atom
A
:= skip | x := e | x[e 1 ] := e 2
Figure 5. Representation of program versions. Here, :: denotes list concatanation, and e and C represent expressions
and predicates respectively.
Program version
Edit
Stmt with hole

void triggerActions (long targetTimeInNanos ) {
while (! queue. isEmpty ()) {
TimedAction current = queue .peek ();
if ( current .time > targetTimeInNanos ) {
<?HOLE ?>;
break; }
time = current .time; queue . remove ();
<?HOLE ?>;
}
<?HOLE ?>;
}
Edit O (∆ O )
[ time = targetTimeInNanos , current . action .call (...) , skip ]

Pv
∆
Ŝ

Holes. When our RPC generation engine encounters a hole
in the shared program, it performs precise relational reason[ skip , current . action .call (...) , time = targetTimeInNanos ]
ing about different modifications by computing a 4-way prodEdit B (∆ B )
uct program of the edits. As is well-known in the relational
verification literature [12, 13], a product program P 1 × P2
[ time = targetTimeInNanos ,
if (! current . isCancelled .get ()) { current . action .call (...);} , is semantically equivalent to P 1 ; P 2 but is constructed in a
skip ]
way that facilitates the verification task. However, because
Edit M (∆ M )
product construction can result in a significant blow-up in
[ skip ,
if (! current . isCancelled .get ()) { current . action .call (...); }, program size, our technique generates mini-products by contime = targetTimeInNanos ]
sidering each hole in isolation rather than constructing a
full-fledged product of the four program versions.
Figure 4. Shared program with holes and the edits.
Loops. Our RPC generation engine infers relational loop invariants for loops that contain edited program fragments.
For instance, our method infers that (i) time O = time B and
method). Since the triggerActions method modifies time,
time A = time M , (ii) value O = value A and value B =
value and queue, we add an assertion for each of these varivalue M , and (iii) the state of collection queue is identical in
ables. For instance, we add the following assertion on the
all four versions for the shared loop from Figure 4.
value of time at exit from the four versions:
Using these ideas, our method is able to automatically
generate an RPC that implies semantic conflict-freedom of
Ô
(time O = time B = time A = time M )
Ó
this example. Furthermore, the entire procedure is push(time O , time A ⇒ time A = time M )
button, including the generation of edits, RPC computation,
(time O , time B ⇒ time B = time M )
and relational loop invariant generation.
Edit A (∆ A )

This assertion states that either (i) all four versions have
identical side-effects on time, or (ii) if the side-effect on
time A (resp. time B ) differs from time O , then time M in
the merge should have identical side-effect as time A (resp.
time B ). We add similar assertions for value and queue.
To prove these assertions, our method assumes that all
four versions start out in identical states and then generates a relational postcondition (RPC) ψ such that the merge
is semantically conflict-free if ψ logically implies the added
assertions. Our RPC generation engine reasons about modifications over the base program by differentiating between
three kinds of statements:

3

Representation of Program Versions

In this section, we describe our representation of program
versions as edits applied to a shared program with holes. As
shown in Figure 5, a program version Pv is a pair (Ŝ, ∆)
where Ŝ is a statement with holes (i.e., missing statements)
and an edit ∆ is a list of statements (without holes). Given
a program version Pv = (Ŝ, ∆), we can obtain a full program P = Ŝ[∆] by applying the edit ∆ to Ŝ according to
the ApplyEdit procedure of Figure 6. Effectively, ApplyEdit
traverses the AST in depth-first order and replaces each hole
with the next statement in the edit. Given n related programs
P1 , . . . , Pn , we assume the existence of a diff procedure that
generates a shared program Ŝ as well as n edits ∆1 , . . . , ∆n
such that ∀i ∈ [1, n]. ApplyEdit(Ŝ, ∆i ) = Pi . Since this diff
procedure is orthogonal to our verification algorithm, we
defer the discussion of our diff procedure until Section 6.
Since the language from Figure 5 uses standard imperative
language constructs (including arrays), we assume an operational semantics described using judgments of the form

Shared statements. We summarize the behavior of shared
statements using straight-line code snippets of the form
y = f (x 1 , . . . , x n ) where f is an uninterpreted function. Essentially, such a statement indicates that the value of variable
y is some (unknown) function of variables x 1 , . . . , x n . These
“summaries" are generated using lightweight dependence
analysis and allow our method to perform abstract reasoning
over unchanged program fragments.
3

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri

ApplyEdit(Ŝ, ∆) = S where(S, [ ]) = Apply(Ŝ, ∆)

applying these edits to Ŝ yields the same programs given
in Figure 1. These programs are conflict-free according to
the syntactic criterion given in Definition 4.1, but the merge
is clearly incorrect (both variants increment x by 1, but the
merge candidate ends up incrementing x by 2).

Apply :: (Ŝ, ∆) → (S, ∆ ′ )
Apply([·], S :: ∆)
Apply(A, ∆)
Apply(Ŝ1 ; Ŝ2 , ∆)

=
=
=

Apply(C ? {Ŝ1 } : {Ŝ2 }, ∆)

=

Apply(while(C) {Ŝ}, ∆)

=

(S, ∆)
(A, ∆)
let (S1 , ∆1 ) = Apply(Ŝ1 , ∆) in
let (S2 , ∆2 ) = Apply(Ŝ2 , ∆1 ) in
((S1 ; S2 ), ∆2 )
let (S1 , ∆1 ) = Apply(Ŝ1 , ∆) in
let (S2 , ∆2 ) = Apply(Ŝ2 , ∆1 ) in
(C ? {S1 } : {S2 }, ∆2 )
let (S, ∆ ′ ) = Apply(Ŝ, ∆) in
(while(C) {S}, ∆ ′ )

The above example illustrates that a syntactic notion of
conflict freedom is not suitable for ruling out incorrect merges.
Similarly, Definition 4.1 can also result in the rejection of
perfectly valid merge candidates.
Example 4.3. Consider the base program x > 0 ? {y := 1} :
{y := 0}; out[0] := y. Suppose this program has a bug that is
caused by using the wrong predicate, so one variant fixes the
bug by swapping the then and else branches, and the other
variant changes the predicate from x > 0 to x ≤ 0. Clearly,
choosing either variant as the merge would be acceptable
because they are semantically equivalent. However, there is
no merge candidate that can satisfy Definition 4.1 because
the shared program is [·]; out[0] := y and the two variants
fill the hole in syntactically conflicting ways.

Figure 6. Application of edit ∆ to program with holes Ŝ
σ ⊢ S ⇓ σ ′, where σ is a valuation that specifies the values
of free variables in S. Specifically, a valuation is a mapping
from (variable, index) pairs to their corresponding values.
The meaning of this judgment is that evaluating S under σ
yields a new valuation σ ′. In the rest of this paper, we also
assume the existence of a special array called out that serves
as the return value of the program. Any behavior that the
programmer considers relevant (e.g., side effects or writing
to the console) can be captured by storing the relevant values
into this out array.

4

Based on the shortcomings of syntactic conflict freedom,
we instead propose the following semantic variant:
Definition 4.4. (Semantic conflict freedom) Suppose that
we are given four program versions O, A, B, M representing the base program, its two variants, and the merge candidate respectively. We say that M is semantically conflict-free,
if for all valuations σ such that:

Semantic Conflict Freedom

In this section, we first introduce syntactic conflict-freedom,
which corresponds to the criterion used by many existing
merge tools. We then explain why it falls short and formally
describe the more robust notion of semantic conflict-freedom.

σ ⊢ O ⇓ σO

σ ⊢ A ⇓ σA

σ ⊢ B ⇓ σB

the following conditions hold for all i:

σ ⊢ M ⇓ σM

3

1. If σ O [(out, i)] , σ A [(out, i)], then σ M [(out, i)] = σ A [(out, i)]
2. If σ O [(out, i)] , σ B [(out, i)], then σ M [(out, i)] = σ B [(out, i)]
3. Otherwise, σ O [(out, i)] = σ A [(out, i)] = σ B [(out, i)] = σ M [(out, i)]

Definition 4.1. (Syntactic conflict freedom) Suppose that
we are given four program versions O = (Ŝ, ∆ O ), A =
(Ŝ, ∆ A ), B = (Ŝ, ∆ B ), M = (Ŝ, ∆ M ) representing the base
program, the two variants, and the merge candidate respectively. We say that the merge candidate M is syntactically
conflict free if the following conditions are satisfied for all
i ∈ [0, n), where n denotes the number of holes in Ŝ:
1. If ∆ O [i] , ∆ A [i], then ∆ M [i] = ∆ A [i]
2. If ∆ O [i] , ∆ B [i], then ∆ M [i] = ∆ B [i]
3. Otherwise, ∆ O [i] = ∆ A [i] = ∆ B [i] = ∆ M [i]

In contrast to syntactic conflict freedom, Definition 4.4
requires agreement between the values that are returned
by the program. Specifically, it says that, if the i’th value
returned by variant A (resp. B) differs from the i’th value
returned by base, then the i’th return value of the merge
should agree with A (resp. B). According to this definition,
the merge candidate from Example 4.2 is not conflict-free
because it returns 2 whereas both variants return 1. Furthermore, for Example 4.3, we can find a merge candidate (e.g.,
one of the variants) that satisfies semantic conflict freedom.

Intuitively, the above definition states that the candidate
merge M makes the same syntactic change as variant A
(resp. B) whenever A (resp. B) differs from O. While this
definition may seem intuitively sensible, it does not accurately capture what it means for a merge candidate to be
correct. In particular, some incorrect merges may be conflictfree according to the above definition, while some correct
merges may be rejected.

5

Verifying Semantic Conflict Freedom

We now turn our attention to the verification algorithm for
proving semantic conflict-freedom. The high-level structure
of the verification algorithm is quite simple and is shown in
Algorithm 1. It takes as input a shared program (with holes)
Ŝ, an edit ∆1 for the base program, edits ∆2 , ∆3 for the variants, and an edit ∆4 for the merge candidate. Conceptually,
the algorithm consists of three steps:

Example 4.2. Consider Ŝ = [·]; [·]; out[0] := x and the edits
∆ O = [skip, skip], ∆ A = [x := x + 1, skip], ∆ B = [skip, x :=
x + 1], and M = [x := x + 1; x := x + 1]. Observe that

3 We

4

assume that out [i] is a special value ⊥ if (out, i) < dom(σ )

Verifying Semantic Conflict-Freedom in Three-Way Program Merges
Algorithm 1 Algorithm for verifying conflict freedom
(1)
1:

procedure Verify(Ŝ, ∆1 , ∆2 , ∆3 , ∆4 )
assume vars({Ŝ[∆1 ], . . . , Ŝ[∆4 ]}) = V
φ := (V1 = V2 ∧ V1 = V3 ∧ V1 = V4 )
ψ := RelationalPost(Ŝ, ∆1 , ∆2 , ∆3 , ∆4 , φ)
χ1 := ∀i. (out 1 [i] , out 2 [i] ⇒ out 2 [i] = out 4 [i])
χ2 := ∀i. (out 1 [i] , out 3 [i] ⇒ out 3 [i] = out 4 [i])
χ2 := ∀i. (out 1 [i] = out 2 [i] = out 3 [i] = out 4 [i])
return ψ |= (χ 1 ∧ χ2 ) ∨ χ3

2:
3:
4:
5:
6:
7:
8:

(2)

(3)

Precondition. Algorithm 1 starts by generating a pre-condition
φ (line 3) stating that all variables initially have the same
value. 4 Note that V1 denotes the variables in the base program, V2 , V3 denote variables in the variants, and V4 refers
to variables in the merge candidate. We use the notation
Vi = Vj as short-hand for ∀v ∈ V . vi = v j .
RPC computation. The next step of the algorithm is to
compute a relational post-condition ψ of φ with respect to
the four program versions (line 4). Such a relational postcondition ψ states relationships between variables V1 , V2 , V3 ,
and V4 and has the property that it is also post-condition
of the program (Ŝ[∆1 ])[V1 /V ]; . . . ; (Ŝ[∆4 ])[V4 /V ]. We will
explain the RelationalPost procedure in detail shortly.

S = head(∆1 )[V1 /V ] ⊛ . . . ⊛ head(∆4 )[V4 /V ]
® φ ⊢ [·] : post(S, φ), [tail(∆1 ), . . . , tail(∆4 )]
∆,
Modifies(S) = {y1 , . . . , yn }
x®i = Dependencies(S, yi )
Si = (yi := Fi (x®i ))[V1 /V ]; . . . ; (yi := Fi (x®i ))[V4 /V ]
® φ ⊢ S : post(S1 ; . . . ; Sn , φ), ∆
®
∆,
® φ ⊢ Ŝ1 : φ ′, ∆
®′
∆,

® ′, φ ′ ⊢ Ŝ2 : φ ′′, ∆
® ′′
∆

® ′′
® φ ⊢ Ŝ1 ; Ŝ2 : φ ′′, ∆
∆,
Ó
φ |= i, j C[Vi /V ] ↔ C[Vj /V ]
® φ ∧ C[V1 /V ] ⊢ Ŝ1 : φ ′, ∆
®′
∆,
′
′′
®
® ′′
∆ , φ ∧ ¬C[V1 /V ] ⊢ Ŝ2 : φ , ∆

(4)

® φ ⊢ C ? {Ŝ1 } : {Ŝ2 } : φ ′ ∨ φ ′′, ∆
® ′′
∆,
φ |= I

(5)

(6)

® I ∧ Ói C[Vi /V ] ⊢ Ŝ : I ′, ∆
® ′ I ′ |= I
∆,
Ó
I |= i, j C[Vi /V ] ↔ C[Vj /V ]
Ó
®
®′
∆, φ ⊢ while(C) Ŝ : I ∧ i ¬C[Vi /V ], ∆

S = (Ŝ[∆1 ])[V1 /V ] ⊛ . . . ⊛ (Ŝ[∆4 ])[V4 /V ]
∆i = (∆i1 :: ∆i2 ) (|∆i1 | = numHoles(Ŝ))
® φ ⊢ Ŝ : post(S, φ), [∆2 , . . . , ∆2 ]
∆,
1
4

Figure 7. RPC inference

Checking conflict freedom. The last step of the algorithm
checks whether the relational post-condition ψ logically implies semantic conflict freedom (line 8). Specifically, observe
that the constraint (χ1 ∧ χ 2 ) ∨ χ3 encodes precisely the three
conditions from Definition 4.4, so the program is conflict-free
if ψ implies (χ 1 ∧ χ2 ) ∨ χ3 .
5.1

PL’17, January 01–03, 2017, New York, NY, USA

are holes in Ŝ, we use ∆®′ to denote the remaining edits that
were not “used” while analyzing Ŝ.
Let us now consider the rules in Figure 7 in more detail.
The first rule corresponds to the case where we encounter
a hole in the shared program and need to analyze the edits.
In this case, we construct a “mini” product program S that
describes the simultaneous execution of the edits. As we will
see in Section 5.2, an n-way product program S1 ⊛ . . . ⊛ Sn
is semantically equivalent to the sequential composition
S1 ; . . . ; Sn but has the advantage of being easier to analyze. Given such a “mini product” S, our RPC generation
engine computes the post-condition of S in the standard way
using a post function, where post(S, φ) yields a sound postcondition of φ with respect to S. Since S may contain loops
in the general case, the computation of post may require loop
invariant generation. As we discuss in Section 5.2, the key
advantage of constructing a product program is to facilitate
loop invariant generation using standard techniques.
Rule (2) corresponds to the case where we encounter a program fragment S without holes. Since S has not been modified by any of the variants, we analyze S in a lightweight
way using dependence analysis. Specifically, for each variable yi that is modified by S, we compute the set of variables
x 1 , . . . , x k that it depends on. We then “summarize” the behavior of S using statements of the form yi = Fi (x 1 , . . . , x k )
where Fi is a fresh uninterpreted function symbol. Hence,
rather than analyzing the entire code fragment S (which

Computing Relational Postconditions

Since the core part of the verification algorithm is the computation of RPCs, we now describe the RelationalPost procedure. As mentioned in Section 1, the key idea is to analyze
edits in a precise way by constructing product programs,
but perform lightweight reasoning for shared program parts
using dependence analysis.
Our RPC generation engine is described in Figure 7 using
® φ ⊢ Ŝ : φ ′, ∆®′. Here, φ is a precondition relating
judgments ∆,
® is a vector of
variables in different program versions, and ∆
n edits applied to a shared base program Ŝ. The meaning of
this judgment is that the following Hoare triple is valid:
{φ} Ŝ[∆1 ][V1 /V ]; . . . ; Ŝ[∆n ][Vn /V ] {φ ′ }
In other words, φ ′ is a sound relational post-condition of
the four program versions with respect to precondition φ.
® may contain more statements than there
Since the edits in ∆
4 Observe

that this precondition also applies to local variables, not just
arguments, and allows our technique to handle cases in which one of the
variants introduces a new variable.
5

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri
such that |∆i | = numHoles(Ŝ). Let φ ′ be the result of call® φ ⊢ Ŝ : φ ′, [] according to
® φ) (i.e., ∆,
ing RelationalPost(Ŝ, ∆,
Figure 7). Then, the following Hoare triple is valid:

could potentially be very large), we analyze its behavior in
a lightweight way by modeling it as straight-line code over
uninterpreted functions. 5
Rule (3) for sequencing is similar to its corresponding
proof rule in standard Hoare logic: Given a statement Ŝ1 ; Ŝ2 ,
we first compute the relational post-condition φ ′ of Ŝ1 and
then use φ ′ as the precondition for Ŝ2 . Since Ŝ1 and Ŝ2 may
contain edits nested inside them, this proof rule combines
reasoning about Ŝ1 and Ŝ2 in a precise, yet lightweight way,
without constructing a 4-way product for the entire program.
Rule (4) allows us to analyze conditionals C ? {Ŝ1 } : {Ŝ2 }
in a modular way whenever possible. As in the sequencing case, we would like to analyze Ŝ1 and Ŝ2 in isolation
and then combine the results. Unfortunately, such compositional reasoning is only possible if all program versions take
the same path. For instance, consider the shared program
[·]; x > 0 ? {y := 1} : {y := 2} and two versions A, B given
by the edits [x := y] and [x := z]. Since A could take the
then branch while B takes the else branch (or vice versa),
we need to reason about all possible combinations of paths.
Hence, the first premise of this rule checks whether each
C[Vi /V ] can be proven to be equivalent to all other C[Vj /V ]’s
under precondition φ. If this is the case, all program versions
take the same path, so we can reason compositionally. Otherwise, our analysis falls back upon the conservative, but
non-modular, proof rule (6) that we will explain shortly.
Rule (5) uses inductive relational invariants for loops that
have been edited in different ways by each program variant.
Specifically, the first premise of this rule states that the relational invariant I is implied by the loop pre-condition, and
the next two premises enforce that I is preserved by the
loop body (i.e., I is inductive). Thus, assuming that all loops
execute the same number of times
Ó (checked by line 2 of rule
5), we can conclude that I ∧ i ¬C[Vi /V ] holds after the
loop. Note that rule (5) does not describe how to compute
such relational loop invariants; it simply asserts that I is
inductive. As we describe in Section 7, our implementation
uses standard techniques based on conjunctive predicate
abstraction to infer such relational loop invariants.
Rule (6) allows us to fall back upon non-modular reasoning
when it is not sound to analyze edits in a compositional
way. Given a statement Ŝ with holes, rule (6) constructs the
product program (Ŝ[∆1 ])[V1 /V ] ⊛ . . . ⊛ (Ŝ[∆4 ])[V4 /V ] and
computes its post-condition in the standard way. While rule
(6) is a generalization of rule (1), it is only used in cases where
compositional reasoning is unsound, as product construction
can cause a blow up in program size.

{φ} (Ŝ[∆1 ])[V1 /V ]; . . . ; (Ŝ[∆n ])[Vn /V ] {φ ′ }
5.2

Construction of Product Programs

In this section, we describe our method for constructing nway product programs. While there are several strategies
for generating 2-way product programs in the literature
(e.g., [12, 13]), our method differs from these approaches in
that it uses similarity metrics to guide product construction
and also generalizes these techniques to n-way products.
The use of similarity metrics allows our method to generate more verification-friendly product programs while obviating the need for performing backtracking search over
non-deterministic product construction rules.
Before we describe our product construction technique,
we first give a simple example to illustrate how product
construction facilitates relational verification:
Example 5.2. Consider the following programs S1 and S2 :
S1 :
S2 :

i 1 := 0; while(i 1 < n 1 ) {i 1 := i 1 ∗ x 1 }
i 2 := 0; while(i 2 < n 2 ) {i 2 := i 2 ∗ x 2 }

and the precondition n 1 = n 2 ∧ x 1 = x 2 . It is easy to see that
i 1 and i 2 will have the same value after executing S1 and
S2 . Now, consider analyzing the program S1 ; S2 . While a
static analyzer can in principle infer this post-condition by
coming up with a precise loop invariant that captures the
exact symbolic value of i 1 and i 2 during each iteration, this
is clearly a very difficult task. To see why product programs
are useful, now consider the following program S:
(1)
(2)
(3)

i 1 := 0; i 2 := 0;
while(i 1 < n 1 ∧ i 2 < n 2 ) {i 1 := i 1 ∗ x 1 ; i 2 := i 2 ∗ x 2 ; }
(i 1 < n 1 )?{while(i 1 < n 1 ) {i 1 := i 1 ∗ x 1 }}
: {(i 2 < n 2 )?{while(i 2 < n 2 ) {i 2 := i 2 ∗ x 2 }} : {skip}}

Here, S is equivalent to S1 ; S2 because it executes both loops
in lockstep until one of them terminates and then executes
the remainder of the other loop. While this code may look
complicated, it is much easier to statically reason about S
than S1 ; S2 . In particular, since i 1 = i 2 ∧ x 1 = x 2 ∧ n 1 = n 2 is
an inductive invariant of the first loop in S, we can easily
prove that line (3) is dead code and that i 1 = i 2 is a valid postcondition of S. As this example illustrates, product programs
can make relational verification easier by executing loops
from different programs in lockstep.
Our n-way product construction method is presented in
Figure 8 using inference rules that derive judgments of the
form ⊢ S1 ⊛ . . . ⊛ Sn ⇝ S where programs S1 , . . . , Sn do
not share any variables (i.e., each Si refers to variables Vi
such that Vi ∩ Vj = ∅ for i , j). The generated product S is
semantically equivalent to S1 ; . . . ; Sn but is constructed in
a way that makes S easier to be statically analyzed. Similar

Theorem 5.1. (Soundness of relational post-condition) 6
® be the edits
Let Ŝ be a shared program with holes and ∆
5 There

are rare cases in which this abstraction would lead to imprecision.
Section 7 describes how our implementation handles such cases.
6 Proofs of all theorems are available in the Appendix.
6

Verifying Semantic Conflict-Freedom in Three-Way Program Merges

PL’17, January 01–03, 2017, New York, NY, USA

synchronize any loops within St and Se with loops from P =
S2 , . . . , Sn . Therefore, we construct the product program as
⊢ A; S1 ⊛
⇝ A; S
C ? {S ′ } : {S ′′ } where S ′ (resp. S ′′) is the product of the
then (resp. else) branch with P⊛ . 7
⊢ St ; S1 ⊛ P⊛ ⇝ S ′ ⊢ Se ; S1 ⊛ P⊛ ⇝ S ′′
(2)
Because the main point of product construction is to gen⊢ (C ? {St } : {Se }); S1 ⊛ P⊛ ⇝ (C ? {S ′ } : {S ′′ })
erate a verification-friendly program by executing loops in
∃Si ∈ P. Si [0] , while(Ci ) {SBi }
lock-step, all of the remaining rules deal with loops. Specifi⊢ Si ⊛ (P \ Si )⊛ ⊛ (while(C 1 ) {SB1 }); S1 ⇝ S
cally, rule (3) considers the case where the first program starts
(3)
⊢ (while(C 1 ) {SB1 }); S1 ⊛ P⊛ ⇝ S
with a loop but there is some program Si in P = (S2 , . . . , Sn )
that does not start with a loop. In this case, we want to “get
∀Si ∈ P. Si [0] = while(Ci ) {SBi }
rid of” program Si by using rules (1) and (2); thus, we move
∃H ⊆ P. ∀L ⊆ P. sim(H) ≥ sim(L)
Si to the beginning and construct the product program S
⊢ (H[0])⊛ ⇝ S ′ ⊢ (H[1 . . .])⊛ ⊛ (P \ H)⊛ ⇝ S ′′
for Si ⊛ (P\Si )⊛ ⊛ while(C 1 ) {SB1 }; S1 .
(4)
P⊛ ⇝ S ′ ; S ′′
Before we continue to the other rules, we make two important
observations about rule (3). First, this rule exploits the
⊢ SB1 ⊛ SB2 ⇝ S
commutativity
and associativity of the ⊛ operator 8 ; howW := while(C 1 ∧ C 2 ) {S}
R := C 1 ? {while(C 1 ) {SB1 }} : {(C 2 ? {while(C 2 ) {SB2 }} : {skip})} ever, it uses these properties in a restricted form by applying
them only where they are useful. Second, after exhaustively
⊢ W ; R ⊛ P⊛ ⇝ S ′
(5)
applying rules (1), (2), and (3) on some P0⊛ , note that we
⊢ (while(C 1 ) {SB1 }) ⊛ (while(C 2 ) {SB2 }) ⊛ P⊛ ⇝ S ′
will end up with a new P1⊛ where all programs in P1 are
Figure 8. Product construction. The base case is the trivial
guaranteed to start with a loop.
rule ⊢ S ⇝ S, and we assume that every program ends in a
Rule (4) considers the case where all programs start with a
skip and that skip ⊛ P⊛ is the same as P⊛ .
loop and utilizes the similarity metric sim to identify which
loops to synchronize. In particular, let H be the subset of
to prior relational verification techniques, the key idea is
the programs in P that are “most similar" according to our
to synchronize loops from different program versions as
similarity metric. Since all programs in H start with a loop,
much as possible. However, our method differs from existing
we first construct the product program S ′ of these loops. We
techniques in that it uses similarity metrics to guide product
then construct the product program S ′′ for the remaining
construction and generalizes them to n-way products.
programs P\H and the remaining parts of the programs in H .
Notation. Before discussing Figure 8, we first introduce
The final rule (5) defines what it means to “execute loops
some useful notation: We abbreviate S1 ⊛ . . . ⊛ Sn using the
in
lockstep as much as possible”. Given two programs that
⊛
notation P , and we write P to denote the list (S1 , . . . , Sn ).
start
with loops while(C 1 ) {S1 } and while(C 2 ) {S2 }, we first
Also, given a statement S, we write S[i] to denote the i’th
construct
the product S1 ⊛ S2 and generate the synchronized
element in the sequence (i.e., S[0] denotes the first element).
loop as while(C 1 ∧C 2 ) {S1 ⊛S2 }. Since these loops may not exSimilarity metric. As mentioned earlier, our algorithm uses
ecute the same number of times, we still need to generate the
similarity metrics between different program fragments to
“continuation” R, which executes any remaining iterations of
guide product construction. Thus, our algorithm is parameone of the loops. Thus, W ; R in rule (5) is semantically equivterized by a function sim : S ∗ → IR+0 that returns a positive
alent to while(C 1 ) {S1 }; while(C 2 ) {S2 }. Now, since there
real number representing similarity between different statemay be further synchronization opportunities between W ; R
ments. While the precise definition of sim is orthogonal to
and the remaining programs S3 , . . . , Sn , we obtain the final
our product construction algorithm, our implementation
product program by computing W ; R ⊛ S3 ⊛ . . . ⊛ Sn .
uses Levensthein distance as the similarity metric.
Example 5.3. Consider again the programs S1 and S2 from
Product construction algorithm. We are now ready to exExample 5.2. We can use rules (1) and (5) from Figure 8 to
plain the product construction rules shown in Figure 8. Rule
compute the product program for S1 ⊛ S2 . The resulting
(1) is quite simple and deals with the case where the first
product is exactly the program S shown in Example 5.2.
program starts with an atomic statement A. Since we can
(1)

⊢ S1 ⊛ P⊛ ⇝ S
P⊛

always compute a precise post-condition for atomic statements, it is not necessary to “synchronize” A with any of the
statements from other programs. Therefore, we first compute the product program S1 ⊛ P⊛ , i.e. S1 ⊛ S2 ⊛ . . . ⊛ Sn ,
and then sequentially compose it with A.
Rule (2) considers the case where the first program starts
with a conditional C ? {St } : {Se }. In general, St and Se
may contain loops; therefore, there may be an opportunity to

Since rules (4) or (5) are both applicable when all programs
start with a loop, our product construction algorithm first
applies rule (4) and then uses rule (5) when constructing the
7 Observe that our handling of if statements can cause a blow-up in program

size, since we essentially embed the continuation S1 inside the then and
else branches. However, because our product construction applies to small
program fragments, we have not found it to be a problem in practice.
8 Recall that different programs do not share variables
7

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri

Algorithm 2 n-way AST differencing algorithm

between Ŝ and the new program S and then use the result
to update the existing edits ∆1 , . . . , ∆k .
In more detail, the Diff2 procedure used in GenEdit yields
ˆ such that
the 2-way diff of Ŝ and S as a triple (Ŝ ′, ∆, ∆)
ˆ = Ŝ. 9 The core insight underlying
Ŝ ′[∆] = S and Ŝ ′[∆]
GenEdit is to use ∆ˆ to update the existing edits ∆1 , . . . , ∆k
for the first k programs. Specifically, we use a procedure
Compose to combine each existing edit ∆i with the output ∆ˆ
of 2Diff. The Compose procedure is defined recursively and
inspects the first element of ∆ˆ in each recursive call. If the
first element is a hole, we preserve the existing edit; otherˆ Thus, if Compose(∆,
ˆ ∆i ) yields
wise, we use the edit from ∆.
′
′
′
∆i , we have Ŝ [∆i ] = Ŝ[∆i ]. In other words, the Compose
procedure allows us to update the diff of the first k programs
to generate a sound diff of k + 1 programs.

1:
2:
3:
4:
5:

procedure NDiff(S1 , . . . , Sn )
® ← []; i ← 2;
Ŝ ← S1 ; ∆
while i ≤ n do
® ← GenEdit(Ŝ, Si , ∆)
®
(Ŝ, ∆)
®
return (Ŝ, ∆)

procedure GenEdit(Ŝ, S, ∆1 , . . . , ∆k )
ˆ := Diff2(S, Ŝ)
(Ŝ ′, ∆, ∆)
for i in [1, k] do
ˆ ∆i )
9:
∆i′ := Compose(∆,
6:

7:
8:

10:
11:
12:
13:
14:
15:

return (Ŝ ′, ∆1′ , . . . , ∆k′ , ∆)
ˆ ∆)
procedure Compose(∆,
ˆ
if ∆ = [ ] then return [ ]
ˆ = [·] then
else if head(∆)
ˆ tail(∆))
return head(∆) :: Compose(tail(∆),
ˆ
ˆ ∆)
else return head(∆) :: Compose(tail(∆),

Theorem 6.1. (Soundness of NDiff) Let NDiff(S1 , . . . , Sn )
ˆ i ] = Si for all i ∈ [1, n].
® Then we have ∆[∆
be (Ŝ, ∆).

7
(H [0])⊛

product for
in rule (4). Thus, our method ensures
that loops that are most similar to each other are executed
in lockstep, which in turn greatly facilitates verification.

We implemented the techniques proposed in this paper in
a tool called SafeMerge for checking semantic conflictfreedom of Java programs. SafeMerge is written in Haskell
and uses the Z3 SMT solver [16]. In what follows, we describe
relational invariant generation, our handling of various aspects of the Java language and other implementation choices.

Theorem 5.4. (Soundness of product) Let S1 , . . . , Sn be
statements with disjoint variables, and let ⊢ S1 ⊛. . .⊛Sn ⇝ S
according to Figure 8. Then, for all valuations σ , we have
σ ⊢ S1 ; . . . ; Sn ⇓ σ ′ iff σ ⊢ S ⇓ σ ′.

6

Implementation

Relational invariant generation. The RPC computation
engine from Section 5.1 requires an inductive loop invariant
relating variables from the four program versions. Our implementation automatically infers relational loop invariants
using the Houdini framework for (monomial) predicate abstraction [20]. Specifically, we consider predicate templates
of the form x i = x j relating values of the same variable
from different program versions, and compute the strongest
conjunct that satisfies the conditions of rule (5) of Figure 7.

Edit Generation

The verification algorithm we described in Section 5 requires
all program versions to be represented as edits applied to
a shared program with holes. This representation is very
important because it allows our verification algorithm to
reason about modifications to different program parts in a
compositional way. In this section, we describe an n-way
AST differencing algorithm that can be used to generate the
desired program representation.
Our n-way diff algorithm is presented in Algorithm 2.
Procedure NDiff takes as input n programs S1 , . . . , Sn and
® where Ŝ is a shared program with holes
returns a pair (Ŝ, ∆)
® is a list of edits such that Ŝ[∆i ] = Si . The loop inside
and ∆
the NDiff procedure maintains the key invariant ∀j. 1 ≤ j <
i ⇒ Ŝ[∆ j ] = Sj . Thus, upon termination, NDiff guarantees
that Ŝ[∆i ] = Si for all i ∈ [1, n].
The bulk of the work of the NDiff procedure is performed
by the auxiliary GenEdit function, which uses a 2-way AST
differencing algorithm to extend the diff from k to k + 1
programs. Specifically, GenEdit takes as input a new program
S as well as the diff of the first k programs, where the diff
is represented as a shared program Ŝ with holes as well as
edits ∆1 , . . . , ∆k . The key idea underlying GenEdit is to use
a standard 2-way AST diff algorithm to compute the diff

Modeling the heap and collections. As standard in prior
verification literature [21], we model each field f in the program as follows: We introduce a map f from object identifiers
to values and model reads and writes to the map using the
select and update functions in the theory of arrays. Similarly,
our implementation models collections, such as ArrayList
and Queue, using arrays. Specifically, we use an array to represent the contents of the collection and use scalar variables
to model the size of the collection as well as the current
position of an iterator over the collection [17].
Side effects of a method. Our formalization uses an out
array to model all relevant side effects of a method. Since
real Java programs do not contain such a construct, our
implementation checks semantic conflict freedom on the
9 Existing

2-way AST diff algorithms can be adapted to produce diffs in this
form. We provide our Diff2 implementation under supplementary materials.
8

Verifying Semantic Conflict-Freedom in Three-Way Program Merges
method’s return value, the final state of the receiver object
as well as any field modified in the method.

freedom. Specifically, our crawler considers a merge scenario
to be relevant if (a) a method is modified by both variants
in different ways, (b) this method involves externally visible
side effects 10 , (c) the merge candidate is different from either
of the variants, and (d) the code does not involve features
that are not handled by our prototype.
To perform this experiment, we run our crawler on nine
popular Java applications, namely Elasticsearch [18], libGDX [4],
iosched [1], kotlin [3], MPAndroidChart [5], okhttp [6], retrofit [7], RxJava [8] and the Spring Boot framework [9]. Out
of 1998 merge instances where a Java source file is modified in both variants, 235 cases involve modifications to the
same method where the merge differs from Base, A and B.
After filtering methods with no side-effects or containing
unhandled features, we obtain a total of 52 benchmarks and
evaluate SafeMerge on all of them. 11

Analysis of shared statements. Recall that our technique
abstracts away shared program statements using uninterpreted functions (rule (2) from Figure 7). However, because
unconditional use of such abstraction can result in false
positives, our implementation checks for certain conditions
before applying rule (2) from Figure 7. Specifically, given precondition ϕ and variables V accessed by shared statement
S, our implementation applies rule (2) only when ϕ implies
semantic conflict freedom on all variables in set V ; otherwise, our implementation falls back on product construction
(i.e., rule (6) from Figure 7). While this check fails rarely in
practice, it is nonetheless useful for avoiding false positives.
7.1 Limitations
Our current prototype implementation has a few limitations:

Main results. The results of our evaluation are presented
in Table 1. For each benchmark, Table 1 shows the abbreviated name of the application it is taken from (column “App”),
the number of lines of code in the merge candidate (“LOC”),
the running time of SafeMerge in seconds (“Time”), and
the results produced by SafeMerge and kdiff3. Specifically,
for SafeMerge, a checkmark (✓) indicates that it was able
to verify semantic conflict-freedom, whereas ✗ means that
it produced a warning. In the case of kdiff3, a checkmark
indicates the absence of syntactic conflicts.
As we can see from Table 1, SafeMerge is able to verify
semantic conflict-freedom for 39 of the 52 benchmarks and reports a warning for the remaining 13. We manually inspected
these thirteen benchmarks and found eleven instances of an
actual semantic conflict (i.e., the merge candidate is indeed
incorrect with respect to Definition 4.4). The remaining two
warnings are false positives caused by imprecision in the
dependence analysis and modeling of collections. In all, these
results indicate that SafeMerge is quite precise, with a false
positive rate around 15%. Furthermore, this experiment also
corroborates that SafeMerge is practical, taking an average
of 0.5 second to verify each benchmark.
Next, Table 2 compares the results produced by SafeMerge and kdiff3 on the 52 benchmarks used in our evaluation. This comparison is very relevant because the merge
candidate in these benchmarks matches exactly the merge
produced by kdiff3 whenever it does not report a textual
conflict. As shown in Table 2, 33 benchmarks are classified as
conflict-free by both SafeMerge and kdiff3, meaning that
SafeMerge can verify the correctness of the textual merge
generated by kdiff3 in these cases. For instance, the merge
with ID 41 in Table 1 corresponds precisely to the example
from RxJava present in Section 2 ( Figure 3). Perhaps more
interestingly, we find five benchmarks for which kdiff3

Analysis scope. Because SafeMerge only analyzes the class
file associated with the modified procedure, it may suffer
from both false positives and negatives. In particular, our
analysis results are only sound under the assumption that the
external callees from other classes have not been modified.
Changes to method signature. SafeMerge currently does
not support renamed methods or methods with parameter
reordering, introduction, or deletion. However, our tool does
not place any requirements on the mapping of local variables.
Similarly, new fields can be introduced or deleted in different
variants — we assume they are present in all four versions
and that they start out in an arbitrary but equal state.
Concurrency, termination, and exceptions. Neither our
formalism nor our prototype implementation support sound
reasoning in the presence of concurrency. Our soundness
claims also rely on the assumption that none of the variants
introduce non-terminating behavior. Finally, although exceptions can be conceptually desugared in our formalism, our
implementation does not handle exceptional control flow.

8

Experimental Evaluation

To assess the usefulness of the proposed method, we perform
a series of three experiments. In our first experiment, we use
SafeMerge to verify semantic conflict-freedom of merges
collected from Github commit histories. In our second experiment, we run SafeMerge on erroneous merge candidates
generated by kdiff3 [2], a widely-used textual merge tool.
Finally, in our third experiment, we assess the scalability of
our method and the importance of various design choices.
All experiments are performed on Quad-core Intel Xeon CPU
with 2.4 GHz and 8 GB memory.
8.1

PL’17, January 01–03, 2017, New York, NY, USA

Evaluation on Merge Candidates from Github

To perform our first experiment, we implemented a crawler
that examines git merge commit histories and extracts interesting methods that have the potential to violate conflict

10 Our

crawler considers a method to have side-effects if it its return value
is not void or if it makes an assignment to a field.
11 All benchmarks can be found under supplementary materials.
9

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri

ID

App

LOC

Time (s)

Result
(SafeMerge)

Result
(kdiff3)

ID

App

LOC

Time (s)

Result
(SafeMerge)

Result
(kdiff3)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

ESearch
ESearch
ESearch
ESearch
ESearch
ESearch
ESearch
ESearch
ESearch
ESearch
iosched
iosched
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin
kotlin

18
25
101
63
90
136
15
30
25
21
63
64
96
54
53
53
104
86
127
56
11
77
11
38
67
7

0.05
0.07
0.20
0.49
4.45
4.07
2.09
0.11
0.09
0.15
0.19
0.07
0.16
0.57
0.48
0.11
0.49
0.31
4.19
0.62
0.06
0.18
0.06
0.15
0.33
0.19

✓
✓
✓
✓
✓
✓
✓
✗
✗
✗
✓
✓
✗
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✗

✗
✓
✓
✓
✓
✓
✓
✗
✗
✗
✓
✓
✓
✓
✓
✓
✓
✓
✗
✓
✓
✓
✓
✓
✗
✗

27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

libgdx
libgdx
libgdx
MPAndroid
MPAndroid
MPAndroid
MPAndroid
MPAndroid
MPAndroid
MPAndroid
MPAndroid
okhttp
retrofit
retrofit
RxJava
spring
spring
spring
spring
spring
spring
spring
spring
spring
spring
spring

30
32
71
47
66
109
44
62
43
35
37
28
66
78
28
107
77
82
81
44
37
42
36
64
13
20

0.12
0.21
0.16
0.44
0.17
0.16
0.10
0.16
0.11
0.23
0.39
0.10
1.67
1.76
0.20
0.12
0.23
0.15
0.21
0.15
0.30
0.07
0.06
0.20
0.09
0.05

✓
✓
✓
✗
✓
✓
✓
✓
✓
✗
✗
✗
✓
✓
✓
✓
✗
✓
✓
✓
✓
✓
✓
✗
✗
✗

✓
✓
✓
✓
✓
✓
✓
✓
✗
✗
✗
✓
✓
✓
✓
✓
✗
✓
✓
✗
✗
✓
✓
✓
✗
✓

Table 1. Summary of experimental results.
SafeMerge
✓
✓
✗
✗

kdiff3
✓
✗
✓
✗

Count
33
6
5
8

Implication
Verified textual merge
Verified manual merge
Fail to verify textual merge
Fail to verify manual merge

For example, in the merge with ID 36 from Table 1, both
variants A and B weaken a predicate in two different ways
by adding two and one additional disjuncts respectively12 .
However, the merge M only picks the weaker predicate from
A, thereby effectively discarding some of the changes from
variant B.

Table 2. Summary of differences between SafeMerge and
kdiff3. “Count” denotes the number of instances in Table 1.

8.2
generates a textual merge that is semantically incorrect according to SafeMerge. Among these five instances, two
correspond (with IDs 13, 30) to the false positives discussed
earlier, leaving us with three benchmarks where the merge
generated by kdiff3 violates Definition 4.4 and should be
further investigated by the developers.
As we can see from Table 2, there are fourteen benchmarks that are syntactically conflicting according to kdiff3
and were likely resolved manually by a developer. Among
these, SafeMerge can verify the correctness of the merge
candidate for six instances (spread over four different applications), thereby confirming the existence of real-world
scenarios where syntactic conflict-freedom results in false
positives. Finally, there are eight cases where the manual
merge cannot be verified SafeMerge. While these examples
indeed violate semantic conflict-freedom, they do not necessarily correspond to bugs (e.g., a developer might have
intentionally discarded changes made by another developer).

Evaluation on Erroneous Merge Candidates

In our second experiment, we explore whether SafeMerge
is able to pinpoint erroneous merges generated by kdiff3.
To perform this experiment, we consider base program with
ID = 25 from Table 1 and generate variants by performing
various kinds of mutations to the base program. Specifically,
we design pairs of mutations that cause kdiff3 to generate
buggy merge candidates.
The results of this experiment are summarized in Table 3,
where the column labeled “Description" summarizes the nature of the mutation. For each pair of variants that are semantically conflict-free, the version named -kdiff3 shows
the incorrect merge generated by kdiff3, where as the one
labeled -manual shows the correct merge that we generated
manually. For benchmarks that are semantically conflicting,
12 Merge

commit https://github.com/PhilJay/MPAndroidChart/commit/
9531ba69895cd64fce48038ffd8df2543eeea1d2

10

Verifying Semantic Conflict-Freedom in Three-Way Program Merges
Name
B1-kdiff3
B1-manual
B2-kdiff3
B2-manual
B3-kdiff3
B4-kdiff3
B5-kdiff3
B6-kdiff3
B6-manual
B7-kdiff3

PL’17, January 01–03, 2017, New York, NY, USA

Description
Patch gets duplicated in merge
Correct version of above
Semantically same, syntactically different patches
Correct version of above
Inconsistent changes in assignment (conflict)
Interference between refactoring and insertion (conflict)
Interference between insertion and deletion (conflict)
One patch supercedes the other
Correct version of above
Inconsistent patches due to off-by-one error (conflict)

Time (s)
0.36
0.38
0.42
0.33
0.34
0.31
0.30
0.32
0.29
0.29

Result
✗
✓
✗
✓
✗
✗
✗
✗
✓
✗

Table 3. Results of our evaluation on merges generated by kdiff3.

Figure 9. Lines of code vs. running time.

Figure 10. Number of holes (edits) vs. running time. Lines
of code varies between 50 and 800.

we only provide results for the incorrect merge generated
by kdiff3 since a correct merge simply does not exist.
The results from Table 3 complement those from Section 8.1 and provide further evidence that a widely-used
merge tool like kdiff3 can generate erroneous merges and
that these buggy merges can be detected by our proposed
technique. This experiment also demonstrates that SafeMerge can verify conflict-freedom in the manually constructed correct merges.
8.3

method computes the product of the four program versions
using the rules from Figure 8 and allows us to assess the
benefits of representing program versions as edits applied to
a shared program. In another variant called No dependence,
we do not abstract away shared program fragments using
uninterpreted functions and analyze them by constructing a
4-way product. However, we still combine reasoning from
different product programs in a compositional way.
Figure 9 compares the running time of SafeMerge against
these two variants as we vary the number of lines of code
but not the number of edits. Observe that the y-axis is shown
in log scale. As we can see from this plot, SafeMerge scales
quite well and analyzes each benchmark in under a second.
In contrast, the running time of Product grows exponentially
in the lines of code. As expected, the No dependence variant is
better than Product but significantly worse than SafeMerge.
Next, Figure 10 compares the running time of SafeMerge
against Product and No dependence as we vary both the number of lines of code and the number of edits. Specifically, a
benchmark containing n holes contains 25n lines of code,
and the y-axis shows the running time of each variant in
log scale. As expected, SafeMerge is more sensitive to the
number holes than it is to the number of lines of code because it abstracts away shared program fragments. However,

Evaluation of Scalability and Design Choices

To assess the scalability of the proposed technique, we performed a third experiment in which we compare the running
time of SafeMerge against the number of lines of code and
number of edits. To perform this experiment, we start with
an existing benchmark from the SafeMerge test suite and
increase the number of lines of code using loop unrolling.
We also vary the number of edits by injecting a modification
in the loop body. This way, the number of holes in the shared
program increases with each loop unrolling.
To evaluate the benefits of the various design choices that
we adopt in this paper, we also compare SafeMerge with
two variants of itself. In one variant, namely Product, we
model the shared program using a single hole, so each edit
corresponds to one of the program versions. Essentially, this
11

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri

SafeMerge still significantly outperforms both Product and
No Dependence. In particular, for a program with 32 edits and
800 lines of code, SafeMerge can verify semantic conflict
freedom in approximately 10 seconds, while No Dependence
takes approximately 100 seconds and Product times out.
In summary, this experiment shows that SafeMerge scales
well as we vary the lines of code and that its running time is
still feasible when program variants perform over 30 modifications to the base program in this example. This experiments also corroborates the practical importance of representing program versions as edits applied to a shared program as well as the advantage of abstracting away shared
program fragments using uninterpreted functions.

9

Relational verification. Verification of conflict freedom is
related to a line of work on relational program logics [14, 39,
42] and product programs [12, 13, 44]. For instance, Benton’s
Relational Hoare Logic (RHL) [14] allows proving equivalence between a pair of structurally similar programs. Sousa
and Dillig generalize Benton’s work by developing Cartesian Hoare Logic, which is used for proving k-safety of programs [39]. Barthe et al. propose another technique for relational verification using product programs [12, 13] and apply
their technique to relational properties, such as equivalence
and 2-safety [40]. In this work, we build on the notion of
product programs used in prior work [12, 13, 44]. However,
rather than constructing a monolithic product of the four
program version, we construct mini-products for each edit.
Furthermore, our proposed product construction algorithm
differs from prior techniques in that it uses similarity metrics
to guide synchronization and generalizes to n-way products.

Related Work

In this section, we compare our technique with prior work
on program merging and relational verification.
Structure-aware merge. Most algorithms for program merging are textual in nature, hardly ever formally described [29],
and without semantic guarantees. To improve on this situation, previous work has proposed structured and semistructured merge techniques to better resolve merge conflicts. For example, FSTMerge [11] uses syntactic structure to
resolve conflicts between AST nodes that can be reordered
(such as method definitions), but it falls back on unstructured
textual merge for other kinds of nodes. Follow-up work on
JDime [10, 33] improves the poor performance of structurebased merging by using textual-based mode (fast) as long
as no conflicts are detected, but switches to structure-based
mode in the presence of conflicts. However, none of these
techniques guarantee semantic conflict freedom.
Semantics-aware merge. Our work is inspired by earlier
work on program integration, which originated with the HPR
algorithm [25] for checking non-interference and generating
valid merges. The HPR algorithm was later refined by the
work of Yang et al. [43], which is one of the first attempts to
incorporate semantics for merge generation. In that context,
the notion of conflict-freedom is parameterized by a classification of nodes of the variants as unchanged such that the
backward slices of unchanged nodes in the two variants are
equivalent modulo a semantic correspondence. Thus, their
classification algorithm is parameterized by a semantic congruence relation. Our approach tackles the slightly different
merge verification (rather then merge generation) problem,
but improves on these prior techniques in several dimensions:
First, we do not require annotations to map statements across
the different versions — this information is computed automatically using our edit generation algorithm (Sec 6). Second,
we show how to formulate conflict freedom directly with
verification conditions and assertion checking. Finally, our
approach performs precise, compositional reasoning about
edits by combining lightweight dependence analysis with
relational reasoning using product programs.

Cross-version program analysis. There has been renewed
interest in program analysis techniques for answering questions about program differences across versions [32]. Prior
work on comparing closely related programs versions include regression verification that checks semantic equivalence using uninterpreted function abstraction of equivalent
callees [19, 22, 30], mutual summaries [23, 41], relational
invariant inference to prove differential properties [31] and
verification modulo versions [34]. Other approaches include
static analysis for abstract differencing [27, 35], symbolic
execution for verifying assertion-equivalence [37] and differential symbolic execution to summarize differences [36]. Our
work is perhaps closest to differential assertion checking [31]
in the use of product programs and invariant inference. However, we do not require an assertion and verify a more complex property involving four different programs. We note
that bugs arising from 3-way merges could potentially also
be uncovered using multi-version testing [26].

10

Conclusion and Future Work

We have proposed a notion of semantic conflict freedom for
3-way merges and described a verification algorithm for proving this property. Our verification algorithm analyzes the
edited parts of the program in a precise way using product
programs, but leverages lightweight dependence analysis to
reason about program fragments that are shared between all
program versions. Our evaluation shows that the proposed
approach can verify semantic conflict-freedom for many realworld benchmarks and identify issues in problematic merges
that are generated by textual 3-way merge tools.
We view this work as a first step towards precise, semanticsaware merge synthesis. In future work, we plan to explore
synthesis techniques that can automatically generate correctby-construction 3-way program merges. Since correct merge
12

Verifying Semantic Conflict-Freedom in Three-Way Program Merges
candidates should obey semantic conflict freedom, the verification algorithm proposed in this paper is necessarily a key
ingredient of such semantics-aware merge synthesis tools.
[24]

References
[25]

[1] [n. d.]. Google I/O Android App. https://github.com/google/iosched.
([n. d.]).
[2] [n. d.]. KDiff3 Project. http://kdiff3.sourceforge.net/. ([n. d.]).
[3] [n. d.]. Kotlin. git@github.com:JetBrains/kotlin.git. ([n. d.]).
[4] [n. d.]. libGDX. https://github.com/libgdx/libgdx. ([n. d.]).
[5] [n. d.].
MPAndroidChart.
https://github.com/PhilJay/
MPAndroidChart. ([n. d.]).
[6] [n. d.]. okhttp. https://github.com/square/okhttp. ([n. d.]).
[7] [n. d.]. retrofit. https://github.com/square/retrofit. ([n. d.]).
[8] [n. d.]. RxJava. https://github.com/ReactiveX/RxJava. ([n. d.]).
[9] [n. d.]. Spring Boot. https://github.com/spring-projects/spring-boot.
([n. d.]).
[10] Sven Apel, Olaf Lessenich, and Christian Lengauer. 2012. Structured
Merge with Auto-tuning: Balancing Precision and Performance. In Proceedings of the 27th IEEE/ACM International Conference on Automated
Software Engineering (ASE 2012).
[11] Sven Apel, Jörg Liebig, Benjamin Brandl, Christian Lengauer, and
Christian Kästner. 2011. Semistructured Merge: Rethinking Merge in
Revision Control Systems. In Proceedings of the 19th ACM SIGSOFT
Symposium and the 13th European Conference on Foundations of Software Engineering (ESEC/FSE ’11).
[12] Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational
verification using product programs. In FM 2011: Formal Methods.
Springer, 200–214.
[13] Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2013. Beyond
2-safety: Asymmetric product programs for relational program verification. In Logical Foundations of Computer Science. Springer, 29–43.
[14] Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. In ACM SIGPLAN Notices, Vol. 39.
ACM, 14–25.
[15] David Wheeler. [n. d.]. The Apple goto fail vulnerability: lessons
learned. http://www.dwheeler.com/essays/apple-goto-fail.html. ([n.
d.]).
[16] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT
solver. In Tools and Algorithms for the Construction and Analysis of
Systems. Springer, 337–340.
[17] Isil Dillig, Thomas Dillig, and Alex Aiken. 2011. Precise reasoning for
programs using containers. In ACM SIGPLAN Notices, Vol. 46. ACM,
187–200.
[18] Shay Banon et al. [n. d.]. ElasticSearch project. ([n. d.]). https://github.
com/elastic/elasticsearch
[19] Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer,
and Mattias Ulbrich. 2014. Automating regression verification. In
ACM/IEEE International Conference on Automated Software Engineering,
ASE ’14, Vasteras, Sweden - September 15 - 19, 2014. 349–360.
[20] Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an Annotation Assistant for ESC/Java. In FME 2001: Formal Methods for Increasing
Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings. 500–517.
[21] Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson,
James B. Saxe, and Raymie Stata. 2002. Extended Static Checking for
Java. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI ’02). ACM, New York,
NY, USA, 234–245. https://doi.org/10.1145/512529.512558
[22] Benny Godlin and Ofer Strichman. 2008. Inference rules for proving
the equivalence of recursive procedures. Acta Inf. 45, 6 (2008), 403–439.
[23] Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebêlo. 2013. Towards Modularly Comparing Programs Using

[26]

[27]

[28]
[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]

[38]

[39]

13

PL’17, January 01–03, 2017, New York, NY, USA

Automated Theorem Provers. In Automated Deduction - CADE-24 24th International Conference on Automated Deduction, Lake Placid, NY,
USA, June 9-14, 2013. Proceedings (Lecture Notes in Computer Science),
Vol. 7898. Springer, 282–299.
Daniel S. Hirschberg. 1977. Algorithms for the Longest Common
Subsequence Problem. J. ACM 24, 4 (1977), 664–675.
Susan Horwitz, Jan Prins, and Thomas Reps. 1989. Integrating noninterfering versions of programs. ACM Transactions on Programming
Languages and Systems (TOPLAS) 11, 3 (1989), 345–387.
Petr Hosek and Cristian Cadar. 2015. Varan the Unbelievable: An Efficient N-version Execution Framework. In 20th International Conference
on Architectural Support for Programming Languages and Operating
Systems (ASPLOS’15). 339–353.
Daniel Jackson and David A. Ladd. 1994. Semantic Diff: A Tool for
Summarizing the Effects of Modifications. In Proceedings of the International Conference on Software Maintenance, ICSM 1994, Victoria, BC,
Canada, September 1994. IEEE Computer Society, 243–252.
John Gruber. [n. d.]. On the Timing of iOS’s SSL Vulnerability. https:
//daringfireball.net/2014/02/apple_prism. ([n. d.]).
Sanjeev Khanna, Keshav Kunal, and Benjamin C Pierce. 2007. A formal investigation of diff3. In FSTTCS 2007: Foundations of Software
Technology and Theoretical Computer Science. Springer, 485–496.
Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Rebêlo. 2012. SYMDIFF: A Language-agnostic Semantic Diff
Tool for Imperative Programs. In Proceedings of the 24th International
Conference on Computer Aided Verification (CAV’12).
Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, and Chris
Hawblitzel. 2013. Differential assertion checking. In Joint Meeting of
the European Software Engineering Conference and the ACM SIGSOFT
Symposium on the Foundations of Software Engineering, ESEC/FSE’13,
Saint Petersburg, Russian Federation, August 18-26, 2013. ACM, 345–355.
Shuvendu K. Lahiri, Kapil Vaswani, and C. A. R. Hoare. 2010. Differential static analysis: opportunities, applications, and challenges. In
Proceedings of the Workshop on Future of Software Engineering Research,
FoSER 2010, at the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, Santa Fe, NM, USA, November
7-11, 2010. ACM, 201–204.
Olaf Lebetaenich, Sven Apel, and Christian Lengauer. 2015. Balancing
Precision and Performance in Structured Merge. Automated Software
Engg. 22, 3 (Sept. 2015).
Francesco Logozzo, Shuvendu K. Lahiri, Manuel Fähndrich, and Sam
Blackshear. 2014. Verification modulo versions: towards usable verification. In ACM SIGPLAN Conference on Programming Language Design
and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 11, 2014. ACM, 32.
Nimrod Partush and Eran Yahav. 2014. Abstract semantic differencing
via speculative correlation. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages
& Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA,
October 20-24, 2014. ACM, 811–828.
Suzette Person, Matthew B. Dwyer, Sebastian G. Elbaum, and Corina S.
Pasareanu. 2008. Differential symbolic execution. In Proceedings of
the 16th ACM SIGSOFT International Symposium on Foundations of
Software Engineering, 2008, Atlanta, Georgia, USA, November 9-14, 2008.
ACM, 226–237.
David A. Ramos and Dawson R. Engler. 2011. Practical, Low-Effort
Equivalence Verification of Real Code. In Computer Aided Verification 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20,
2011. Proceedings. 669–685.
SlashDot. [n. d.].
Apple SSL Bug In iOS Also Affects
OS X.
http://apple.slashdot.org/story/14/02/22/2143224/
apple-ssl-bug-in-ios-also-affects-os-x. ([n. d.]).
Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare logic for verifying
k-safety properties. In Proceedings of the 37th ACM SIGPLAN Conference

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri

on Programming Language Design and Implementation. ACM, 57–69.
[40] Tachio Terauchi and Alex Aiken. 2005. Secure information flow as a
safety problem. Springer.
[41] Tim Wood, Sophia Drossopoulou, Shuvendu K. Lahiri, and Susan Eisenbach. 2017. Modular Verification of Procedure Equivalence in the Presence of Memory Allocation. In Programming Languages and Systems 26th European Symposium on Programming, ESOP 2017, Held as Part
of the European Joint Conferences on Theory and Practice of Software,
ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. 937–963.
[42] Hongseok Yang. 2007. Relational separation logic. Theoretical Computer Science 375, 1 (2007), 308–334.
[43] Wuu Yang, Susan Horwitz, and Thomas Reps. 1990. A Program Integration Algorithm That Accommodates Semantics-preserving Transformations. SIGSOFT Softw. Eng. Notes 15, 6 (Oct. 1990), 133–143.
[44] Anna Zaks and Amir Pnueli. 2008. Covac: Compiler validation by
program analysis of the cross-product. In FM 2008: Formal Methods.
Springer, 35–51.

14

Verifying Semantic Conflict-Freedom in Three-Way Program Merges

σ ⊢ skip ⇓ σ

σ ⊢ e ⇓ c σ ′ = σ [(x, 0) 7→ c]
σ ⊢ x := e ⇓ σ ′

σ ⊢ e1 ⇓ c1 σ ⊢ e2 ⇓ c2
σ ′ = σ [(x, c 1 ) 7→ c 2 ]
σ ⊢ x[e 1 ] := e 2 ⇓ σ ′

σ [(x, 0)] = c
σ ⊢ out(x) ⇓ σ

σ ⊢ S 1 ⇓ σ1
σ1 ⊢ S 2 ⇓ σ2
σ ⊢ S 1 ; S 2 ⇓ σ2

σ ⊢ C ⇓ true
σ ⊢ S 1 ⇓ σ1
σ ⊢ C ? {S 1 } : {S 2 } ⇓ σ1

σ ⊢ C ⇓ false
σ ⊢ S 2 ⇓ σ2
σ ⊢ C ? {S 1 } : {S 2 } ⇓ σ2

PL’17, January 01–03, 2017, New York, NY, USA

Rule 3. Let Sx = while(C 1 ) {SB1 }; S1 . Suppose we have σ ⊢
Sx ; S2 ; . . . ; Sn ⇓ σ ′. Suppose there is exists Si that satisfies
first premise of the proof rule. Observe that S1 ; S2 ; . . . ; Sn ;
is semantically equivalent to Sn ; S2 ; . . . ; Sn−1 ; S1 ; as long
as S1 , Sn , do not share variables between them and also
with S2 . . . Sn−1 . Since Sx and Si have no shared variables
between them and with any other program Sj different
than Sx and Si , we have
σ ⊢ Si ; S2 ; . . . ; Si−1 ; Si+1 ; . . . Sn ; while(C 1 ) {SB1 }; S1 ⇓ σ ′
Then, by the premise of the proof rule and the inductive
hypothesis, we have σ ⊢ S ⇓ σ ′.

σ ⊢ C ⇓ false
σ ⊢ while(C) {S } ⇓ σ

Rule 4. Suppose we have σ ⊢ S1 ; S2 ; . . . ; Sn ⇓ σ ′′ where
each Si is of the form while(Ci ) {SBi }; Si′. By the same reason as in Rule 3. we can move any loop in each Si to the
beginning as they don’t share any variable with any other Sj .
That is, considering H = S1 ; . . . ; So be the set of programs
satisfying the second premise we have

σ ⊢ C ⇓ true
σ ⊢ S ⇓ σ1
σ1 ⊢ while(C) {S } ⇓ σ2
σ ⊢ while(C) {S } ⇓ σ2

σ ⊢ while(C 1 ) {SB1 }; . . . while(Co ) {SBo } ⇓ σ ′

Figure 11. Operational semantics

and considering So+1 ; . . . Sn a sequence of the original
programs excluding the ones in H we have

Appendix A: Operational Semantics
σ ′ ⊢ S1′ ; . . . So′ ; So+1 ; . . . Sn ⇓ σ ′′
Then, by the last premises of the proof rule and the inductive hypothesis, we have that σ ⊢ S ′; S ′′ ⇓ σ ′′.

Figure 11 shows the operational semantics of the language
from Figure 5. Recall that σ maps (variable, index) pairs to
values, and we view scalar variables as arrays with a single
valid index at 0. Since the semantics of expressions is completely standard, we do not show them here. However, one
important point worth noting is the semantics of expressions
involving array reads:

Rule 5. Suppose we have
σ ⊢ while(C 1 ) {S1 }; while(C 2 ) {S2 }; S3 ; . . . ; Sn ⇓ σ ′
Let W ′ be the loop while(C 1 ∧ C 2 ) {S1 ; S2 }. Since C 1 , C 2 and
S1 , S2 have disjoint sets of variables, the program fragment
while(C 1 ) {S1 }; while(C 2 ) {S2 } is semantically equivalent
to W ′; R (where R comes from the third line of the proof
rule). Hence, we have σ ⊢ W ′; R; S3 ; . . . ; Sn ⇓ σ ′. By the
first premise of the proof rule and the inductive hypothesis,
if σ0 ⊢ S1 ; S2 ⇓ σ1 for any σ0 , σ1 , then σ0 ⊢ S ⇓ σ1 . Thus,
σ ⊢ W ′ ⇓ σ ∗ implies σ ⊢ W ⇓ σ ∗ , which in turn implies
σ ⊢ W ; R; S3 ; . . . ; Sn ⇓ σ ′. By the last premise of the proof
rule and the inductive hypothesis, we know σ ⊢ S ′ : σ ′;
hence, the property holds.

σ ⊢e ⇓c
σ ⊢e ⇓c
(a, c) ∈ dom(σ )
(a, c) < dom(σ )
σ ⊢ a[e] ⇓ σ [(a, c)]
σ ⊢ a[e] ⇓ ⊥
In other words, reads from locations that have not been
initialized yield a special constant ⊥.
Appendix B: Soundness of Product
Here, we provide a proof of Theorem 5.4. The proof is by
structural induction over the product construction rules
given in Figure 8. Since the two directions of the proof are
completely symmetric, we only prove one direction. Note
that the base case is trivial because ⊢ S ⇝ S.

Appendix C: Proof of Soundness of Relational
Post-conditions

Rule 1. Suppose σ ⊢ A ⇓ σ ′ and σ ′ ⊢ S1 ; S2 ; . . . ; Sn ⇓ σ ′′.
By the premise of the proof rule and the inductive hypothesis,
we have σ ′ ⊢ S ⇓ σ ′′. Thus, σ ⊢ A; S ⇓ σ ′′.

The proof is by structural induction on Ŝ.
Case 1. Ŝ = [·], and the edits are S1 , . . . , S4 . In this case,
Figure 7 constructs the relational post-condition by first computing the product program S as S1 [V1 /V ] ⊛ . . . ⊛ S[V4 /4]
and then computing the standard post-condition of S. By
Theorem 5.4, we have σ ⊢ S ⇓ σ ′ iff σ ⊢ S1 [V1 /V ] ⊛ . . . ⊛
S[V4 /4] ⇓ σ ′. Furthermore, by the correctness of post operator, we know that {φ}S{φ ′ } is a valid Hoare triple. This

Rule 2. Suppose σ ⊢ (C ? {St } : {Se }); S1 ; S2 ; . . . ; Sn ⇓
σ ′′. Without loss of generality, suppose σ ⊢ C ⇓ true, and
suppose σ ⊢ St ; S1 ⇓ σ ′, so σ ′ ⊢ S2 ; . . . ; Sn ⇓ σ ′′. By the
first premise of the proof rule and the inductive hypothesis,
we have σ ⊢ S ′ ⇓ σ ′′. Hence, σ ⊢ C ? {S ′ } : {S ′′ } ⇓ σ ′′.
15

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri

implies {φ}S1 [V1 /V ]; . . . ; S4 [V4 /V ]{φ ′ } is also a valid Hoare
triple.

{φ} C 1 ?(Ŝ1 [∆A1 ])[V1 /V ]); . . . ; (Ŝ1 [∆A4 ])[V4 /V ]) :
(Ŝ2 [∆B1 ])[V1 /V ]); . . . ; (Ŝ2 [∆B4 ])[V4 /V ])
{φ 1 }
Ó
Now, since φ logically entails i, j Ci ↔ C j , the statement
above is equivalent to:

Case 2. Ŝ = S (i.e., Ŝ does not contain holes). By the second rule in Figure 7, we know that {φ}S1 ; . . . ; Sn {φ ′ } is
a valid Hoare triple. Now, consider any valuation σ satisfying φ. By the correctness of the Hoare triple, if σ ⊢
S1 ; . . . ; Sn ⇓ σ ′, we know that σ ′ also satisfies φ ′. Now, recall that S1 ; . . . ; Sn contains uninterpreted functions, and we
assume that F (®
x) can return any value, as long as it returns
something consistent for the same input values. Let Σ represent the set of all valuations σi such that σ ⊢ S1 ; . . . ; Sn ⇓ σi .
By the correctness of the Hoare triple, we know that any
σi ∈ Σ satisfies φ ′. Assuming the correctness of the mod
and dependence analysis, for any valuation σ such that
σ ⊢ S[V1 /V ]; . . . ; S[V4 /V ] ⇓ σ ′, we know that σ ′ ∈ Σ. Since
all valuations in Σ satisfy φ ′, this implies σ ′ also satisfies φ ′.
Thus, {φ}S[V1 /V ]; . . . ; S[V4 /V ]{φ ′ } is also a valid Hoare
triple.

C 1 ? {(Ŝ1 [∆A1 ])[V1 /V ]} : {(Ŝ2 [∆B1 ])[V1 /V ]};
...
C 4 ? {(Ŝ1 [∆A4 ])[V4 /V ]} : {(Ŝ2 [∆B4 ])[V4 /V ]};
Next, using the fact that Ŝ[∆i ] = (C ? {Ŝ1 } : {Ŝ2 })[∆i ] =
® Bi ]}, we can conclude:
C ? {Ŝ1 [∆Ai ]} : {Ŝ2 [∆
{φ}

{I} (Ŝ[∆1 ])[V1 /V ]; . . . (Ŝ[∆4 ])[V4 /V ] {I}
Since we also have φ |= I from the premise, this implies:
{φ} while(C 1 ) {(Ŝ[∆1 ])[V1 /V ]; . . . (Ŝ[∆4 ])[V4 /V ]} {I∧¬C 1 }

{φ}(Ŝ1 [∆A1 ])[V1 /V ]); . . . ; (Ŝ1 [∆A4 ])[V4 /V ]){φ 1 }

Next, since we can commute
statements over different variÓ
ables and I implies i j C[Vi /V ] ↔ C[Vj /V ], we can conclude:

as well as
{φ 1 }(Ŝ2 [∆B1 ])[V1 /V ]); . . . ; (Ŝ2 [∆B4 ])[V4 /V ]){φ 2 }

{φ}

Using these and the standard Hoare rule for composition,
we can conclude:
(Ŝ1 [∆A1 ])[V1 /V ]); . . . ; (Ŝ1 [∆A4 ])[V4 /V ]);
(Ŝ2 [∆B1 ])[V1 /V ]); . . . ; (Ŝ2 [∆B4 ])[V4 /V ])

(Ŝ1 [∆A1 ]; Ŝ2 [∆B1 ])[V1 /V ]); . . . ;
(Ŝ1 [∆A4 ]; Ŝ2 [∆B4 ])[V4 /V ])

while(C 1 ) {(Ŝ[∆1 ])[V1 /V ]}; . . . ;
while(C 4 ) {(Ŝ[∆4 ])[V4 /V ]}

{I ∧ ¬C 1 }

Finally, because the loop while(Ci ) {Ŝ[∆i ]} is the same as
(while(Ci ) {Ŝ})[∆i ], we have:

{φ 2 }

Since we can commute statements over different variables,
this implies:
{φ}

{φ ′ }

Case 5. Ŝ = while(C) {Ŝ}. As in case (4), let Ci denote
C[Vi /V ]. From the premise of rule (5) of Figure 7 and the
inductive hypothesis, we know:

® A denote the prefix of ∆
® that is
Case 3. Ŝ = Ŝ1 ; Ŝ2 . Let ∆
®
®1
used for filling holes in Ŝ1 , and ∆B denote the prefix of ∆
that is used for filling holes in Ŝ2 . By the premise of the third
rule and inductive hypothesis, we have

{φ}

((C 1 ? {Ŝ1 } : {Ŝ2 })[∆1 ])[V1 /V ]; . . . ;
((C 4 ? {Ŝ1 } : {Ŝ2 }))[∆4 ])[V4 /V ]

{φ}

(while(C 1 ) {Ŝ[V1 /V ]})[∆1 ]; . . . ;
(while(C 4 ) {Ŝ[V4 /V ]})[∆4 ]

{I ∧ ¬C 1 }

{φ 2 }

Case 6. First, assuming the soundness of the standard post
Next, using the fact that Ŝ[∆i ] = (Ŝ1 ; Ŝ2 )[∆i ] = Ŝ1 [∆Ai ]; Ŝ2 [∆Bi ], operator, we have {φ}S{post(S, φ)}. Using the premise of
the proof rule and Theorem 5.4, we obtain:
we can conclude:
{φ}(Ŝ[∆1 ])[V1 /V ]); . . . ; (Ŝ[∆4 ])[V4 /V ]){φ 2 }

{φ} (Ŝ[∆11 ])[V1 /V ]; . . . (Ŝ[∆14 ])[V4 /V ] {post(S, φ)}

® A, ∆
® B denote the prefixes
Case 4. Ŝ = C ? {Ŝ1 } : {Ŝ2 }. Let ∆
® ∆®1 that is used for filling holes in Ŝ1 and Ŝ2 respectively.
of ∆,
Also, let Ci denote C[Vi /V ]. By the first premise of rule 4
from Figure 7 and the inductive hypothesis, we have:

Since ∆i1 is the prefix of ∆i that contains as many holes as
Ŝ, we also know Ŝ[∆i1 ] = Ŝ[∆i ]. Thus, we get:
{φ} (Ŝ[∆1 ])[V1 /V ]; . . . (Ŝ[∆4 ])[V4 /V ] {post(S, φ)}
Appendix D: Soundness of n-way Diff Algorithm

{φ ∧ C 1 } (Ŝ1 [∆A1 ])[V1 /V ]); . . . ; (Ŝ1 [∆A4 ])[V4 /V ]) {φ 1 }

Theorem 6.1 follows directly from the following two lemmas:

Now, using the second premise and the inductive hypothesis,
we also have:

ˆ then Compose ensures
Lemma 10.1. If |∆| = numHoles(∆),
the following post-conditions:
ˆ
• |∆ ′ | = | ∆|
ˆ (Ŝ[∆])[∆]
ˆ
• For any Ŝ s.t. numHoles(Ŝ) = | ∆|,
= Ŝ[∆ ′]

{φ ∧ ¬C 1 } (Ŝ2 [∆B1 ])[V1 /V ]); . . . ; (Ŝ2 [∆B4 ])[V4 /V ]) {φ 2 }
Using these two facts and the standard Hoare logic rule for
if statements, we get:
16

Verifying Semantic Conflict-Freedom in Three-Way Program Merges

PL’17, January 01–03, 2017, New York, NY, USA

Proof. Consider the two postconditions of Compose. For the
[1, . . . , k], the first postcondition of Compose at line 9 imˆ = |∆ ′ |. Together, they imply that numHoles(Ŝ ′) =
branch ∆ˆ = [ ], it is easy to see that ∆ ′ = ∆ˆ = [ ] and thus
plies | ∆|
i
′
′
ˆ For any Ŝ with 0 holes, applying any edits gets
|∆i |.
|∆ | = | ∆|.
′ ] = Ŝ follows directly from the
back Ŝ, satisfying the second postcondition.
The postcondition Ŝ ′[∆k+1
ˆ
ˆ
third postcondition of Diff2 at line 7 and line ??. Now conFor the branch head(∆) = [·], we know numHoles(tail(∆)) =
ˆ − 1 = |tail(∆)| (given the precondition), which
sider ∆i′ for i ∈ [1, . . . , k]. We know from the postcondition
numHoles(∆)
ˆ Therefore, from the postsatisfies the precondition of Compose at line 14. The first
of Diff2 that numHoles(Ŝ ′) = | ∆|.
postcondition of the recursive call to Compose implies that
condition of Compose at line ?? (where we substitute Ŝ ′ for
ˆ =
′ ′
size of the return value (|∆ ′ |) equals |head(∆)| + |tail(∆)|
ˆ
the bound variable Ŝ), we know that (Ŝ ′[∆])[∆
i ] = Ŝ [∆i ].
ˆ
ˆ
1+ | ∆| −1 = | ∆|. Now consider a Ŝ such that numHoles(Ŝ) =
′
ˆ = Ŝ.
From the postconditon of Diff2 at line 7, we know Ŝ [∆]
ˆ Let ∆ ′′ be the return from the recursive call to Compose.
| ∆|.
′ [∆ ′ ].
Together,
they
imply
Ŝ[∆
]
=
Ŝ
□
i
i
Then Ŝ[∆ ′] = Ŝ[head(∆) :: ∆ ′′] = (Ŝ[head(∆)])[∆ ′′] (by
definition of applying an edit). Since numHoles(Ŝ[head(∆)]) =
Appendix E: Example of 4-way diff
ˆ we know that (Ŝ[head(∆)])[∆ ′′] = We illustrate the 4-way diff using a simple example:
numHoles(Ŝ)−1 = |tail(∆)|,
ˆ
(from the second postcondi((Ŝ[head(∆)])[tail(∆)])[tail(∆)]
O  c ? {x := 1} : {y := 2}; z := 3
ˆ = [·] in this branch,
tion of the recursive call). Since head(∆)
A  c ? {x := 2} : {y := 2};
ˆ = (Ŝ[[·] :: tail(∆)])[head(∆)]
ˆ
ˆ
(Ŝ[head(∆)])[tail(∆)]
= (Ŝ[∆])[head(∆)].
B  c ? {x := 1} : {y := 3}; z := 3
This follows from the fact that applying head(∆) to the first
M  c ? {x := 2} : {y := 3};
ˆ is identical to applying
hole in Ŝ followed by applying tail(∆)
According to Algorithm 2, we start out with the shared proˆ fola hole in the first hole in Ŝ followed by applying tail(∆),
gram Ŝ = O and ∆ O = [ ].
lowed by applying head(∆) which applies it to the first hole
Now consider the first call to GenEdit(Ŝ, A, ∆ O ). After
ˆ
ˆ
in Ŝ. Further, ((Ŝ[∆])[head(∆)])[tail(∆)]
= (Ŝ[∆])[∆]
by the
ˆ
invoking
Diff2(A, Ŝ) at line 7, it returns the tuple (Ŝ ′, ∆, ∆)
rule of applying edits, which proves this postcondition.
′
where Ŝ  c ? {[·]} : {y := 2}; [·], ∆  [x := 2, skip] and
ˆ , [·], we know numHoles(tail(∆))
ˆ =
For the branch head(∆)
∆ˆ  [x := 1, z := 3]. The reader can verify that Ŝ ′[∆] = A
ˆ
numHoles(∆). This along with the precondition of Compose
ˆ = Ŝ = O. Next, consider the call to Compose(∆,
ˆ ∆1 )
and Ŝ ′[∆]
establishes the preconditon to the call to Compose at line 15.
′′
where ∆1 = [ ]. The call executes the branch in line ?? twice
Let ∆ denote the return of the recursive call to Compose.
ˆ
ˆ = | ∆|
ˆ − 1.
(since ∆ˆ does not contain any holes) and returns ∆ ′ as ∆.
The recursive call ensures that |∆ ′′ | = |tail(∆)|
′
′
′′
ˆ :: ∆ | = | ∆|,
ˆ which establishes the first
Therefore, the call to GenEdit returns the tuple (Ŝ , [x :=
Thus |∆ | = |head(∆)
1, z := 3], [x := 2, skip]), which constitutes Ŝ, ∆ O , ∆ A for
postcondition. Now consider a Ŝ such that numHoles(Ŝ) =
′
′′
′′
ˆ
ˆ
ˆ
the next call to GenEdit.
| ∆|. Then Ŝ[∆ ] = Ŝ[head(∆) :: ∆ ] = (Ŝ[head(∆)])[∆ ].
ˆ
ˆ
The next call to GenEdit(Ŝ, B, ∆ O , ∆ A ) calls Diff2(B, c ? {[·]} :
Since numHoles(Ŝ[head(∆)]) = numHoles(Ŝ)−1 = |tail(∆)|,
ˆ where Ŝ ′  c ? {[·]} :
′′
ˆ
ˆ
ˆ
{y
:= 2}; [·]) and returns (Ŝ ′, ∆, ∆),
we know that (Ŝ[head(∆)])[∆ ] = ((Ŝ[head(∆])[tail(∆)])[∆]
{[·]}; [·] and ∆  [x := 1, y := 2, z := 3] (which becomes ∆ B )
(from the second postcondition of the recursive call), which
ˆ :: tail(∆)])[∆]
ˆ
ˆ
and ∆ˆ  [[·], y := 2, [·]]. The reader can verify that Ŝ ′[∆] = B
simplifies to (Ŝ[head(∆)
= (Ŝ[∆)])[∆]
by the
ˆ = Ŝ. The loop at line 8 updates ∆ O and ∆ A —
and Ŝ ′[∆]
property of applying an edit.
□
ˆ ∆A )
we only describe the latter. The return of Compose(∆,
updates ∆ A to [x := 2, y := 2, skip] by walking the first arLemma 10.2. If |∆i | = numHoles(Ŝ) for all i ∈ [1, . . . , k]
gument and replacing [·] with corresponding entry from
ˆ ∆ O ) to
and 2Diff satisfies the contract provided in Algorithm 3, then
∆ A . Similarly, the ∆ O is updated by Compose(∆,
GenEdit ensures the following post-conditions:
[x := 1, y := 2, z := 3].
The final call to GenEdit(Ŝ, M, ∆ O , ∆ A , ∆ B ) returns the
• |∆i′ | = numHoles(Ŝ ′) for i ∈ [1, . . . , k + 1]
tuple
(Ŝ, ∆ O , ∆ A , ∆ B , ∆ M ), where Ŝ, ∆ O , ∆ A , ∆ B remain
• Ŝ ′[∆k′ +1 ] = S and Ŝ ′[∆i′ ] = Ŝ[∆i ] for i ∈ [1, . . . , k]
unchanged (since Ŝ already contains holes at all the changed
locations), and ∆ M is assigned [x := 2, y := 3, skip]. The
ˆ of Compose
Proof. First, the precondition |∆i | = numHoles(∆)
reader can verify that Ŝ[∆ O ] = O, Ŝ[∆ A ] = A, Ŝ[∆ B ] =
in line 9 is satisfied from the precondition |∆i | = numHoles(Ŝ)
B, Ŝ[∆ M ] = M.
ˆ =
of GenEdit and the second postcondition numHoles(∆)
numHoles(Ŝ) of Diff2.
Appendix F: An abstract implementation of Diff2
′
′
Now, consider the postcondition |∆i | = numHoles(Ŝ )
Algorithm 3 describes Diff2 algorithm for computing the
for i ∈ [1, . . . , k + 1]. From the first postcondition of Diff2
2-way diff. It takes as input a program S and a program
ˆ For any i ∈
at line 7, we know that numHoles(Ŝ ′) = | ∆|.
with holes Ŝ and returns the shared program with holes
17

PL’17, January 01–03, 2017, New York, NY, USA

Marcelo Sousa, Isil Dillig, and Shuvendu Lahiri
ˆ such that Ŝ ′[∆] = S and Ŝ ′[∆]
ˆ = Ŝ.
Ŝ ′ and edits ∆ and ∆,
Since Ŝ may contain holes, the edit ∆ˆ may contain holes.
The algorithm recursively descends down the structure of
the two programs and tries to identify the common program
and generate respective edits for the differences. We use nondeterministic conditional to abstract from actual heuristics
to match parts of the two ASTs. For example, when matching
S with Ŝ1 ; Ŝ2 , a heuristic may decide to match S with Ŝ1
and create a shared program [·]; [·] and edits ∆ = [S, skip],
∆ˆ = [Ŝ1 , Ŝ2 ]; it may also choose to match S with Ŝ2 and create a shared program [·]; [·] and edits ∆ = [skip, S], [Ŝ1 , Ŝ2 ].
The decision is often based on algorithms based on variants of longest-common-subsequence [24]. However, these
decisions only help maximize the size of the shared program, and do not affect the soundness of the edit generation.
Lines 9 to 12 allow us to model all such heuristics by nondeterministically inserting skip statemnets before or after
a statement. Line 24 ensures that the diff procedure can always return by constructing the trivial shared program [·]
and S and Ŝ as the respective edits. Line 7 checks if Ŝ is
a hole, then the shared program is a hole [·] and the two
edits contain S and Ŝ respectively. Line 8 is the case when
S equals Ŝ. We use = to denote the syntactic equality of
the two syntax trees. The remaining rules are standard and
recurse down the AST structure and match the subtrees.

Algorithm 3 Algorithm for 2-way AST Diff
1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:

procedure Diff2(S, Ŝ)
Input: A program S and a shared program Ŝ
Output: Shared program Ŝ ′ and edits ∆, ∆ˆ
ˆ = numHoles(Ŝ ′)
Ensures: |∆| = | ∆|
ˆ = numHoles(Ŝ)
Ensures: numHoles(∆)
′
ˆ = Ŝ
Ensures: Ŝ [∆] = S, Ŝ ′[∆]
if Ŝ = [·] then return ([·], [S], [Ŝ])
else if Ŝ = S then return (S, [ ], [ ])
else if * then return Diff2(S; skip, Ŝ)
▷
Non-deterministic skip introduction
else if * then return Diff2(skip; S, Ŝ)
▷
Non-deterministic skip introduction
else if * then return Diff2(S, Ŝ; skip)
▷
Non-deterministic skip introduction
else if * then return Diff2(S, skip; Ŝ)
▷
Non-deterministic skip introduction
else if S = S1 ; S2 and Ŝ = Ŝ1 ; Ŝ2 then
(Ŝ1′, ∆1 , ∆ˆ 1 ) := Diff2(S1 , Ŝ1 )
(Ŝ2′, ∆2 , ∆ˆ 2 ) := Diff2(S2 , Ŝ2 )
return (Ŝ1′ ; Ŝ2′, ∆1 :: ∆2 , ∆ˆ 1 :: ∆ˆ 2 )
else if S = C ? {S1 } : {S2 } and Ŝ = C ′ ? {Ŝ1 } :
{Ŝ2 } and C = C ′ then
(Ŝ1′, ∆1 , ∆ˆ 1 ) := Diff2(S1 , Ŝ1 )
(Ŝ2′, ∆2 , ∆ˆ 2 ) := Diff2(S2 , Ŝ2 )
return (C ? {Ŝ1′ } : {Ŝ2′ }, ∆1 :: ∆2 , ∆ˆ 1 :: ∆ˆ 2 )
else if S = while(C) {S1 } and Ŝ = while(C ′) {Ŝ1 }
and C = C ′ then
(Ŝ1′, ∆1 , ∆ˆ 1 ) := Diff2(S1 , Ŝ1 )
return (while(C) {Ŝ1′ }, ∆1 , ∆ˆ 1 )
else
return ([·], [S], [Ŝ])

18

