research-article

Open access

Verified three-way program merge

Authors:

Shuvendu K. LahiriAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue OOPSLA

Article No.: 165, Pages 1 - 29

https://doi.org/10.1145/3276535

Published: 24 October 2018 Publication History

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.

Supplementary Material

WEBM File (a165-sousa.webm)

Download
100.90 MB

References

[1]

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) .

Digital Library

[2]

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) .

Digital Library

[3]

Dimitar Asenov, Balz Guenat, Peter Müller, and Martin Otth. 2017. Precise version control of trees with line-based version control systems. In International Conference on Fundamental Approaches to Software Engineering. Springer, 152–169.

Digital Library

[4]

Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational verification using product programs. In FM 2011: Formal Methods . Springer, 200–214.

Digital Library

[5]

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.

[6]

Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. In ACM SIGPLAN Notices, Vol. 39. ACM, 14–25.

Digital Library

[7]

Yuriy Brun, Reid Holmes, Michael D Ernst, and David Notkin. 2013. Early detection of collaboration conflicts and risks. IEEE Transactions on Software Engineering 39, 10 (2013), 1358–1375.

Digital Library

[8]

Guilherme Cavalcanti, Paulo Borba, and Paola R. G. Accioly. 2017. Evaluating and improving semistructured merge. PACMPL 1, OOPSLA (2017), 59:1–59:27.

Digital Library

[9]

David Wheeler. 2017. The Apple goto fail vulnerability: lessons learned. http://www.dwheeler.com/essays/apple-goto-fail. html . (2017).

[10]

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.

Digital Library

[11]

Isil Dillig, Thomas Dillig, and Alex Aiken. 2011. Precise reasoning for programs using containers. In ACM SIGPLAN Notices, Vol. 46. ACM, 187–200.

Digital Library

[12]

H Christian Estler, Martin Nordio, Carlo A Furia, and Bertrand Meyer. 2013. Unifying configuration management with merge conflict detection and awareness systems. In Software Engineering Conference (ASWEC), 2013 22nd Australian. IEEE, 201–210.

Digital Library

[13]

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.

Digital Library

[14]

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.

Digital Library

[15]

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.

Digital Library

[16]

Fowler, Martin. 2011. Semantic Conflict. https://martinfowler.com/bliki/SemanticConflict.html . (2011).

[17]

Benny Godlin and Ofer Strichman. 2008. Inference rules for proving the equivalence of recursive procedures. Acta Inf. 45, 6 (2008), 403–439.

Digital Library

[18]

Mário Luís Guimarães and António Rito Silva. 2012. Improving early detection of software merge conflicts. In Proceedings of the 34th International Conference on Software Engineering . IEEE Press, 342–352.

Digital Library

[19]

Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebêlo. 2013. Towards Modularly Comparing Programs Using 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.

Digital Library

[20]

Daniel S. Hirschberg. 1977. Algorithms for the Longest Common Subsequence Problem. J. ACM 24, 4 (1977), 664–675.

Digital Library

[21]

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.

Digital Library

[22]

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.

Digital Library

[23]

John Gruber. 2014. On the Timing of iOS’s SSL Vulnerability. https://daringfireball.net/2014/02/apple_prism . (2014).

[24]

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.

Digital Library

[25]

Knoy, Gabriel. 2012. How Often Does Gitmerge make mistakes? https://news.ycombinator.com/item?id=9871042 . (2012).

[26]

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) .

Digital Library

[27]

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.

Digital Library

[28]

Olaf Lebetaenich, Sven Apel, and Christian Lengauer. 2015. Balancing Precision and Performance in Structured Merge. Automated Software Engg. 22, 3 (Sept. 2015).

Digital Library

[29]

Lee, TK. 2012. The Problem of Automatic Code Merging. http://www.personal.psu.edu/txl20/blogs/tks_tech_notes/2012/03/ the-problem-of-automatic-code-merging.html . (2012).

[30]

Lenski, Dan. 2015. Is it possible for Git merging to make a mistake without detecting a conflict? https://www.quora.com/ Is-it-possible-for-Git-merging-to-make-a-mistake-without-detecting-a-conflict . (2015).

[31]

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.

Digital Library

[32]

Lutton, Mark. 2014. Infinite Loop Caused by Git Merge. https://stackoverflow.com/questions/23523713/ how-can-i-trust-git-merge . (2014).

[33]

Ahmed-Nacer Mehdi, Pascal Urso, and François Charoy. 2014. Evaluating software merge quality. In Proceedings of the 18th International Conference on Evaluation and Assessment in Software Engineering . ACM, 9.

Digital Library

[34]

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.

Digital Library

[35]

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.

Digital Library

[36]

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.

Digital Library

[37]

Reddit. 2017a. Automatic Merge Mistakes. https://www.reddit.com/r/git/comments/5bssjv/automatic_merge_mistakes/ . (2017).

[38]

Reddit. 2017b. How Do you Deal with Auto Merge? https://www.reddit.com/r/git/comments/5hn80k/how_do_you_deal_ with_auto_merge/ . (2017).

[39]

Rostedt, Steven. 2011. Fix Bug Caused by Git Merge. http://lkml.iu.edu/hypermail/linux/kernel/1106.0/00645.html . (2011).

[40]

SlashDot. 2014. 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 . (2014).

[41]

Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare logic for verifying k-safety properties. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation . ACM, 57–69.

Digital Library

[42]

Tachio Terauchi and Alex Aiken. 2005. Secure information flow as a safety problem. Springer.

[43]

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.

Digital Library

[44]

Hongseok Yang. 2007. Relational separation logic. Theoretical Computer Science 375, 1 (2007), 308–334.

Digital Library

[45]

Wuu Yang, Susan Horwitz, and Thomas Reps. 1990. A Program Integration Algorithm That Accommodates Semanticspreserving Transformations. SIGSOFT Softw. Eng. Notes 15, 6 (Oct. 1990), 133–143.

Digital Library

[46]

Anna Zaks and Amir Pnueli. 2008. Covac: Compiler validation by program analysis of the cross-product. In FM 2008: Formal Methods . Springer, 35–51.

Digital Library

Cited By

Dong JSun JLin YZhang YMa MDong JHao DFilkov VRay BZhou M(2024)Revisiting the Conflict-Resolving Problem from a Semantic PerspectiveProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3694993(141-152)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3694993
De Jesus GBorba PBonifácio RDe Oliveira MRoychoudhury APaiva AAbreu RStorey M(2024)Lightweight Semantic Conflict Detection with Static AnalysisProceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings10.1145/3639478.3643118(343-345)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3639478.3643118
Da Silva LBorba PMaciel TMahmood WBerger TMoisakis JGomes ALeite V(2024)Detecting semantic conflicts with unit testsJournal of Systems and Software10.1016/j.jss.2024.112070214(112070)Online publication date: Aug-2024
https://doi.org/10.1016/j.jss.2024.112070
Show More Cited By

Index Terms

Verified three-way program merge
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

A Relational Program Logic with Data Abstraction and Dynamic Framing
Dedicated to Tony Hoare.

In a paper published in 1972, Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that comprise the API of ...
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the ...
From verified model to executable program: the PAT approach

CSP# is a formal modeling language that emphasizes the design of communication in concurrent systems. PAT framework provides a model checking environment for the simulation and verification of CSP# models. Although the desired properties can be formally ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue OOPSLA

November 2018

1656 pages

EISSN:2475-1421

DOI:10.1145/3288538

Issue’s Table of Contents

Copyright © 2018 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 October 2018

Published in PACMPL Volume 2, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

AFRL
NSF

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
1,033
Total Downloads

Downloads (Last 12 months)121
Downloads (Last 6 weeks)11

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dong JSun JLin YZhang YMa MDong JHao DFilkov VRay BZhou M(2024)Revisiting the Conflict-Resolving Problem from a Semantic PerspectiveProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3694993(141-152)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3694993
De Jesus GBorba PBonifácio RDe Oliveira MRoychoudhury APaiva AAbreu RStorey M(2024)Lightweight Semantic Conflict Detection with Static AnalysisProceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings10.1145/3639478.3643118(343-345)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3639478.3643118
Da Silva LBorba PMaciel TMahmood WBerger TMoisakis JGomes ALeite V(2024)Detecting semantic conflicts with unit testsJournal of Systems and Software10.1016/j.jss.2024.112070214(112070)Online publication date: Aug-2024
https://doi.org/10.1016/j.jss.2024.112070
Milovančević DKunčak V(2023)Proving and Disproving Equivalence of Functional Programming AssignmentsProceedings of the ACM on Programming Languages10.1145/35912587:PLDI(928-951)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591258
Pirk H(2023)Collaborative Data Science using Scalable HomoiconicityACM SIGMOD Record10.1145/3582302.358231651:4(54-55)Online publication date: 25-Jan-2023
https://dl.acm.org/doi/10.1145/3582302.3582316
Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Shen BGulzar MHe FMeng N(2023)A Characterization Study of Merge Conflicts in Java ProjectsACM Transactions on Software Engineering and Methodology10.1145/354694432:2(1-28)Online publication date: 31-Mar-2023
https://dl.acm.org/doi/10.1145/3546944
Dinella EMytkowicz TSvyatkovskiy ABird CNaik MLahiri S(2023)DeepMerge: Learning to Merge ProgramsIEEE Transactions on Software Engineering10.1109/TSE.2022.318395549:4(1599-1614)Online publication date: 1-Apr-2023
https://doi.org/10.1109/TSE.2022.3183955
Muylaert WHärtel JDe Roover C(2023)Symbolic Execution to Detect Semantic Merge Conflicts2023 IEEE 23rd International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM59687.2023.00028(186-197)Online publication date: 2-Oct-2023
https://doi.org/10.1109/SCAM59687.2023.00028
Dong JZhu QSun ZLou YHao DBissyandé TKlein JBird CSarro F(2023)Merge Conflict Resolution: Classification or Generation?Proceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE56229.2023.00155(1652-1663)Online publication date: 11-Nov-2023
https://dl.acm.org/doi/10.1109/ASE56229.2023.00155
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents