Verifying Semantic Conflict-Freedom in Three-Way Program Merges

TL;DR

This paper introduces a semantic approach and a compositional algorithm to verify conflict-freedom in three-way program merges, aiming to prevent subtle bugs and ensure correct integration of code changes.

Contribution

It presents a novel, compositional verification method for semantic conflict-freedom in three-way merges, combining dependence analysis and relational reasoning, with an effective tool called SafeMerge.

Findings

SafeMerge successfully verified 52 real-world merge scenarios.

The approach outperforms syntactic conflict detection in precision.

SafeMerge is practical and effective for real-world software merging.

Abstract

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 confict-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 confict-freedom and indicate that SafeMerge is both precise and practical.