Verified three-way program merge
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 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 summarization for shared program fragments with precise relational reasoning for the modifications. Towards this goal, our method uses a 4-way differencing algorithm on abstract syntax trees to represent different program versions as edits applied to a shared program with holes. This representation allows our verification algorithm to reason about different edits in isolation and compose them to obtain an overall proof of conflict freedom. We have implemented the proposed technique in a new tool called SafeMerge for Java and evaluate it on 52 real-world merge scenarios obtained from Github. The experimental results demonstrate the benefits of our approach over syntactic conflict-freedom and indicate that SafeMerge is both precise and practical.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 24, 2018
- Source ID
- 10.1145/3276535
Entities
People
- Işıl Dillig
- Marcelo C. Sousa
- Shuvendu K. Lahiri
Organizations
- Air Force Research Laboratory
- Microsoft
- National Science Foundation
- University of Oxford
- University of Texas at Austin