REVIEW 2 major objections 4 minor 41 references
On the Correctness of Software Merge
T0 review · 2 major / 4 minor · reviewed 2026-07-10 · grok-4.5
Pith's one-line read A three-way merge is correct only when it is parsable and universal (a pushout of AST edits); d3j meets both while existing tools often do not.
desk verdict Solid operationalization of pushout-based merge correctness with large-scale evidence that existing tools silently produce non-universal results; d3j is a clean reference that reports zero violations under the stated criteria. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
Pushout of partial inclusion maps on AST nodes: the unique (up to isomorphism) commutative diagram that amalgamates the two edit sequences from the common ancestor while satisfying the four no-extra/no-missed insertion and deletion conditions; d3j constructs such pushouts by successive single-edit diagram completion under 32 language-specific conflict rules.
What would settle it
A concrete merge scenario in which d3j (or any tool claimed to satisfy the criteria) returns a conflict-free result that either fails to parse or violates one of the four universality conditions when the AST node maps are recomputed by an independent optimal tree-edit algorithm.
Extended reading notes
Core claim
A conflict-free three-way merge of program versions is correct if and only if the resulting text is syntactically parsable and the partial inclusion maps of AST nodes form a pushout: every inserted node appears, every deleted node disappears, common edits are applied once, and no extra nodes are introduced. The authors show that existing tools frequently violate these conditions while their own tool d3j never does on a large corpus of Java merges.
Load-bearing premise
The AST differencing step must produce partial inclusion maps that accurately reflect the intended insertions, deletions, renames and moves; if that matching is wrong, both the merge and the correctness check can fail.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes syntactic correctness criteria for three-way software merges: a conflict-free result must be parsable (syntactically valid) and universal (the partial inclusion maps on AST nodes induced by the edits form a pushout, satisfying no-extra/missed insertion or deletion conditions). It presents d3j, a structural Java merge tool that constructs commutative diagrams of tree edits while enforcing 32 language-specific conflict rules, and evaluates it against git-merge, imediff, jFSTMerge, JDime, IntelliMerge, AutoMerge-PTM, Spork and Mastery on 43,774 file-merge scenarios from 76 open-source projects (Table I), 2,582 developer-resolved merges, and 2,459 refactoring-heavy scenarios. d3j reports zero non-parsable or non-universal results while competitors report many; the criteria are used both to diagnose competitor errors and to compare against human resolutions.
Significance. If the criteria and experimental claims hold, the work supplies the first practical, checkable definition of merge correctness that is independent of any particular tool's output and grounded in the universal property of pushouts. The large-scale tables (I–III), violation breakdowns (Table II), mutual-coverage analysis (Fig. 11), and candid comparison with developer choices and refactorings give the community concrete evidence that existing tools silently produce non-universal or unparsable merges, while also exposing the limits of purely structural approaches. The publicly released replication package and the explicit separation of parsability from universality are strengths that make the contribution immediately usable for future tool evaluation and design.
major comments (2)
- [V-B, V-E, Table I] Section V-B and the threats discussion (V-E) acknowledge that universality of every competitor result is judged by partial inclusion maps produced by d3j’s own (approximated Zhang–Shasha) differencer. While the paper mitigates this by independent non-WP counts, concrete counter-examples (Figs. 10, 12) and a 100-case manual sample, a residual circularity remains: a tool whose internal matching differs systematically from d3j’s could be scored as non-universal even when its own intended edits form a pushout. A short sensitivity experiment that re-checks a stratified sample of “non-Univ” cases with an independent differencer (e.g., GumTree) would strengthen the comparative claim.
- [III-D] The 32 hand-crafted conflict rules (Section III-D) are presented as sufficient to guarantee that every conflict-free d3j merge is parsable. No completeness argument or systematic enumeration relative to the Java grammar is given; the rules are justified by “careful examination.” Because the zero non-WP count for d3j rests on these rules, a brief statement of how the rule set was validated (or an explicit list of the syntactic categories covered) would make the soundness claim more transparent.
minor comments (4)
- [II] Figure 2’s Diff3 example uses numeric tokens; a short caption note that they stand for the cooking-recipe fragments mentioned in the text would improve readability.
- [V-B] The phrase “perfect-CFM” is introduced in Table I without an explicit definition in the surrounding prose; a one-sentence clarification that it means textual identity with the repository merge commit would help.
- [IV] In Section IV the four universality conditions are numbered 1–4, yet later text refers to “conditions 1-3”; a consistent numbering or an explicit remark that commutativity is treated separately would avoid minor confusion.
- [VIII] The replication package DOI is given, but the manuscript promises source-code links “upon publication.” Adding a permanent repository URL (or noting that the Zenodo archive already contains the full tool chain) would improve reproducibility for the camera-ready version.
Circularity Check
No significant circularity: correctness criteria (parsable + pushout universality on partial inclusion maps) are defined independently of any fit or self-referential equation and then applied as an external checker to open-source histories and competitor outputs.
-
self definitional
[Section IV (Correctness Criteria) and V-B (Large-Scale Merge Experiment)]
"We developed our own merge tool d3j together with a tool to check the conditions 1-4 using our own AST comparison tool. In fact, the merging algorithm implemented in d3j is illustrated in Figures 6 and 7 and is designed to calculate pushouts while checking for conflicts. … d3j reports none."
d3j’s zero count of universality violations is guaranteed by construction once the algorithm is stipulated to compute pushouts; the experimental claim that “our tool reports none” therefore reduces, for d3j itself, to the definition of the algorithm rather than an independent empirical discovery. (The same maps are used to score competitors, but that does not create a circular prediction for the criteria themselves.)
full rationale
The paper defines a conflict-free merge as correct precisely when it is syntactically parsable and the induced partial inclusion maps of AST nodes form a pushout (conditions 1–4: no extra/missed insertions or deletions). These conditions are taken from the universal property of pushouts in the category of sets and partial inclusion maps; they are not fitted to any data set, nor are they reverse-engineered from d3j’s outputs. d3j is deliberately constructed to compute such pushouts while enforcing language-specific conflict rules, so its zero-violation count on the 43 774 scenarios is expected by design rather than a surprising prediction. Competitor results are judged by the same independent checker (the authors’ own AST differencer) against external Git histories, developer-resolved merges, and refactoring scenarios; the paper itself flags the dependence on that differencer as a threat to validity and mitigates it with manual sampling and non-WP counts. No load-bearing uniqueness theorem, ansatz, or fitted parameter is imported via self-citation. The single minor self-referential element is that the same maps used to build d3j are also used to score it, but this does not collapse the comparative claims or the proposed criteria. Hence circularity is negligible.
Assumptions & free parameters
assumptions (3)
- standard math A three-way merge of partial inclusion maps is correct precisely when the resulting maps form a pushout (commutativity + universality) in the category of sets with partial inclusions.
- domain assumption Tree edits (delete/insert/relabel/move) induce order-preserving partial inclusion maps on AST nodes that preserve ancestry and sibling order.
- ad hoc to paper 32 hand-crafted, Java-specific conflict rules (name clash, split deletion, broken dependency, cardinality mismatch, etc.) are sufficient to guarantee syntactic validity of any conflict-free merge.
invented entities (1)
-
d3j merge engine with relative-path AST patches
independent evidence
Cite this review
Pith. "Pith review of On the Correctness of Software Merge." pith.science (2026). https://pith.science/paper/45QIHH2I
@misc{pith2026260707987,
author = {Pith},
title = {Pith review of: On the Correctness of Software Merge},
year = {2026},
howpublished = {\url{https://pith.science/paper/45QIHH2I}},
note = {Machine review of arXiv:2607.07987}
}
read the original abstract
Three-way merge tools play crucial roles in modern software development, where a developer forks a branch to make local modifications and requests it to be merged into the main branch via a "pull request." Despite its importance, the task has traditionally been defined in an intuitive manner, and the results of merge tools are often accepted without scrutiny. In this paper, we present a new structural merge tool in comparison with existing tools based on the syntactic criteria we propose for evaluating the merge results. We require the merge result to be both parsable and universal. Being parsable means that the result is syntactically valid according to the grammar of the programming language. Being universal means that the result incorporates all and only the edit operations occurring in each branch while ensuring that edits common to both branches are applied only once. This requirement can be precisely defined using the notion of pushouts in category theory. In a large-scale experiment involving 43,774 file merge scenarios from 76 open-source Java projects, we found a number of incorrect results reported by existing tools such as the Git companion merge tool, whereas our tool reports none. We further compared d3j's results with 2,582 developer-resolved merges and with 2,459 merge scenarios involving 21 refactoring types. These experiments revealed both the strengths and current limitations of structural merge, and underscore the importance of clear correctness criteria. We expect that the proposed criterion will provide a foundation for developing more reliable and principled merge tools.
Figures
Figures from the paper (7 more)
Reference graph
Works this paper leans on
-
[1]
An exploratory study of the pull-based software development model,
G. Gousios, M. Pinzger, and A. v. Deursen, “An exploratory study of the pull-based software development model,” inProceedings of the 36th International Conference on Software Engineering, ser. ICSE. New York, NY , USA: ACM, 2014, pp. 345–355
work page 2014
-
[2]
Balancing precision and performance in structured merge,
O. Leßenich, S. Apel, and C. Lengauer, “Balancing precision and performance in structured merge,”Automated Software Engineering, vol. 22, no. 3, pp. 367–397, Sep 2015. [Online]. Available: https://doi.org/10.1007/s10515-014-0151-5
-
[3]
Spork: Struc- tured merge for java with formatting preservation,
S. Larsen, J.-R. Falleri, B. Baudry, and M. Monperrus, “Spork: Struc- tured merge for java with formatting preservation,”IEEE Transactions on Software Engineering, pp. 1–1, 2022
work page 2022
-
[4]
Intellimerge: A refactoring-aware software merging technique,
B. Shen, W. Zhang, H. Zhao, G. Liang, Z. Jin, and Q. Wang, “Intellimerge: A refactoring-aware software merging technique,”Proc. ACM Program. Lang., vol. 3, no. OOPSLA, oct 2019. [Online]. Available: https://doi.org/10.1145/3360596
-
[5]
A three-way merge for XML documents,
T. Lindholm, “A three-way merge for XML documents,” inProceedings of the 2004 ACM Symposium on Document Engineering, ser. DocEng ’04. New York, NY , USA: ACM, 2004, pp. 1–10. [Online]. Available: http://doi.acm.org/10.1145/1030397.1030399
-
[6]
F. Zhu, X. Xie, D. Feng, N. Meng, and F. He, “On the methodology of three-way structured merge in version control systems: Top-down, bottom-up, or both,”Journal of Systems Architecture, vol. 145, p. 103011, 2023. [Online]. Available: https://www.sciencedirect.com/ science/article/pii/S138376212300190X
work page 2023
-
[7]
A formal investigation of diff3,
S. Khanna, K. Kunal, and B. C. Pierce, “A formal investigation of diff3,” inFSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, V . Arvind and S. Prasad, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2007, pp. 485–496
work page 2007
-
[8]
Categorical approaches to merging software changes,
J. A. Goguen, “Categorical approaches to merging software changes,” 1995, unpublished draft
work page 1995
Show all 41 references
-
[9]
A categorical theory of patches,
S. Mimram and C. Di Giusto, “A categorical theory of patches,” Electron. Notes Theor. Comput. Sci., vol. 298, pp. 283–307, Nov. 2013. [Online]. Available: http://dx.doi.org/10.1016/j.entcs.2013.09.018
2013 doi
-
[10]
Diaconescu,Implicit Partiality of Signature Morphisms in Institution Theory
R. Diaconescu,Implicit Partiality of Signature Morphisms in Institution Theory. Cham: Springer International Publishing, 2021, pp. 81–123. [Online]. Available: https://doi.org/10.1007/978-3-030-64187-0 4
2021 doi
-
[11]
Moerdijk and J
I. Moerdijk and J. van Oosten,Sets, Models and Proofs. Springer Cham, 2018
2018
-
[12]
What is Menhir?
F. Pottier and Y . R ´egis-Gianas, “What is Menhir?” 2021. [Online]. Available: https://gallium.inria.fr/∼fpottier/menhir/
2021
-
[13]
Gosling, B
J. Gosling, B. Joy, G. Steele, and G. Bracha,The Java Language Specification, Third Edition. Prentice Hall, June 2005
2005
-
[14]
Gusfield,Algorithms on Strings, Trees, and Sequences: Computer Science and Computational Biology
D. Gusfield,Algorithms on Strings, Trees, and Sequences: Computer Science and Computational Biology. Cambridge University Press, 1997
1997
-
[15]
A survey on tree edit distance and related problems,
P. Bille, “A survey on tree edit distance and related problems,”Theoret- ical Computer Science, vol. 337, no. 1-3, pp. 217–239, Jun. 2005
2005
-
[16]
Simple fast algorithms for the editing distance between trees and related problems,
K. Zhang and D. Shasha, “Simple fast algorithms for the editing distance between trees and related problems,”SIAM Journal on Computing, vol. 18, no. 6, pp. 1245–1262, 1989
1989
-
[17]
Imediff - an interactive fullscreen merge tool for diff2/3,
J. Elonen, “Imediff - an interactive fullscreen merge tool for diff2/3,”
-
[18]
Available: https://github.com/osamuaoki/imediff/
[Online]. Available: https://github.com/osamuaoki/imediff/
-
[19]
Evaluating and improving semistructured merge,
G. Cavalcanti, P. Borba, and P. Accioly, “Evaluating and improving semistructured merge,”Proc. ACM Program. Lang., vol. 1, no. OOPSLA, pp. 59:1–59:27, Oct. 2017. [Online]. Available: http: //doi.acm.org/10.1145/3133883
2017 doi
-
[20]
Enhancing precision of structured merge by proper tree matching,
F. Zhu, F. He, and Q. Yu, “Enhancing precision of structured merge by proper tree matching,” in2019 IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), 2019, pp. 286–287
2019
-
[21]
Semistructured merge: Rethinking merge in revision control systems,
S. Apel, J. Liebig, B. Brandl, C. Lengauer, and C. K ¨astner, “Semistructured merge: Rethinking merge in revision control systems,” inProceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ser. ESEC/FSE ’11. New Y...
2011 doi
-
[22]
Conflict resolution for structured merge via version space algebra,
F. Zhu and F. He, “Conflict resolution for structured merge via version space algebra,”Proc. ACM Program. Lang., vol. 2, no. OOPSLA, pp. 166:1–166:25, Oct. 2018. [Online]. Available: http://doi.acm.org/10.1145/3276536
2018 doi
-
[23]
Fine-grained and accurate source code differencing,
J.-R. Falleri, F. Morandat, X. Blanc, M. Martinez, and M. Monperrus, “Fine-grained and accurate source code differencing,” inProceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ser. ASE ’14. New York, NY , USA: ACM, 2014, pp. 313–324
2014
-
[24]
Meaningful change detection in structured data,
S. S. Chawathe and H. Garcia-Molina, “Meaningful change detection in structured data,” inProceedings of the ACM SIGMOD International Conference on Management of Data, Tuscon, Arizona, May 1997, pp. 26–37
1997
-
[25]
Spoon: A Library for Implementing Analyses and Transformations of Java Source Code,
R. Pawlak, M. Monperrus, N. Petitprez, C. Noguera, and L. Seinturier, “Spoon: A Library for Implementing Analyses and Transformations of Java Source Code,”Software: Practice and Experience, vol. 46, pp. 1155–1179, 2015. [Online]. Available: https://hal.archives-ouvertes.fr/ ha...
2015
-
[26]
Type-safe generic differencing of mutually recursive families,
V . C. Miraldo, “Type-safe generic differencing of mutually recursive families,” Ph.D. dissertation, Utrecht University, October 2020
2020
-
[27]
On the nature of merge conflicts: A study of 2,731 open source java projects hosted by GitHub,
G. Ghiotto, L. Murta, M. Barros, and A. van der Hoek, “On the nature of merge conflicts: A study of 2,731 open source java projects hosted by GitHub,”IEEE Transactions on Software Engineering, vol. 46, no. 8, pp. 892–915, 2020
2020
-
[28]
DeepMerge: Learning to Merge Programs ,
E. Dinella, T. Mytkowicz, A. Svyatkovskiy, C. Bird, M. Naik, and S. Lahiri, “ DeepMerge: Learning to Merge Programs ,”IEEE Transactions on Software Engineering, vol. 49, no. 04, pp. 1599–1614, Apr. 2023. [Online]. Available: https://doi.ieeecomputersociety.org/10. 1109/TSE.202...
2023
-
[29]
Are refactorings to blame? an empirical study of refactorings in merge conflicts,
M. Mahmoudi, S. Nadi, and N. Tsantalis, “Are refactorings to blame? an empirical study of refactorings in merge conflicts,” inProceedings of the IEEE 26th International Conference on Software Analysis, Evolution and Reengineering, ser. SANER ’19, Feb 2019, pp. 151–162
2019
-
[30]
Refactoringminer 2.0,
N. Tsantalis, A. Ketkar, and D. Dig, “Refactoringminer 2.0,”IEEE Transactions on Software Engineering, vol. 48, no. 3, pp. 930–950, 2022
2022
-
[31]
Operation-based refactoring-aware merging: An empirical evaluation,
M. Ellis, S. Nadi, and D. Dig, “Operation-based refactoring-aware merging: An empirical evaluation,”IEEE Transactions on Software Engineering, vol. 49, no. 4, pp. 2698–2721, 2023
2023
-
[32]
A state-of-the-art survey on software merging,
T. Mens, “A state-of-the-art survey on software merging,”IEEE Trans- actions on Software Engineering, vol. 28, no. 5, pp. 449–462, May 2002
2002
-
[33]
Structure-oriented merging of revisions of software documents,
B. Westfechtel, “Structure-oriented merging of revisions of software documents,” inProceedings of the 3rd International Workshop on Software Configuration Management, ser. SCM ’91. New York, NY , USA: ACM, 1991, pp. 68–79. [Online]. Available: http://doi.acm.org/10.1145/111062.111071
1991 doi
-
[34]
Syntactic software merging,
J. Buffenbarger, “Syntactic software merging,” inSoftware Configuration Management, J. Estublier, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1995, pp. 153–172
1995
-
[35]
Evaluating software merge quality,
A.-N. Mehdi, P. Urso, and F. Charoy, “Evaluating software merge quality,” inProceedings of the 18th International Conference on Evaluation and Assessment in Software Engineering, ser. EASE ’14. New York, NY , USA: ACM, 2014, pp. 9:1–9:10. [Online]. Available: http://doi.acm.or...
2014 doi
-
[36]
Precise version control of trees with line-based version control systems,
D. Asenov, B. Guenat, P. M ¨uller, and M. Otth, “Precise version control of trees with line-based version control systems,” inFundamental Approaches to Software Engineering, M. Huisman and J. Rubin, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2017, pp. 152–169
2017
-
[37]
Verified three-way program merge,
M. Sousa, I. Dillig, and S. K. Lahiri, “Verified three-way program merge,”Proc. ACM Program. Lang., vol. 2, no. OOPSLA, pp. 165:1–165:29, Oct. 2018. [Online]. Available: http://doi.acm.org/10. 1145/3276535
2018
-
[38]
Deltaimpactfinder: Assessing semantic merge conflicts with dependency analysis,
M. Dias, G. Polito, D. Cassou, and S. Ducasse, “Deltaimpactfinder: Assessing semantic merge conflicts with dependency analysis,” in Proceedings of the International Workshop on Smalltalk Technologies, ser. IWST ’15. New York, NY , USA: ACM, 2015, pp. 8:1–8:6. [Online]. Availab...
2015 doi
-
[39]
Detecting semantic merge conflicts with variability-aware execution,
H. V . Nguyen, M. H. Nguyen, S. C. Dang, C. K ¨astner, and T. N. Nguyen, “Detecting semantic merge conflicts with variability-aware execution,” inProceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ser. ESEC/FSE 2015. New York, NY , USA: ACM, 201...
2015 doi
-
[40]
Diff/TS: A tool for fine-grained structural change analysis,
M. Hashimoto and A. Mori, “Diff/TS: A tool for fine-grained structural change analysis,” inProceedings of the 15th Working Conference on Reverse Engineering, ser. WCRE ’08. Washington, DC, USA: IEEE Computer Society, 2008, pp. 279–288
2008
-
[41]
Change distilling: Tree differencing for fine-grained source code change extraction,
B. Fluri, M. W ¨ursch, M. Pinzger, and H. Gall, “Change distilling: Tree differencing for fine-grained source code change extraction,”IEEE Transactions on Software Engineering, vol. 33, no. 11, pp. 725–743, 2007
2007
Reviewed July 10, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.