The starting point is a paper on "Non-blocking atomic commitment" by Babaoglu and Toueg, from Mulender's book on Distributed Systems. They present an algorithm for distributed atomic commitment that enjoys different sets of properties depending on what type of broadcast is used. They give an informal correctness proof which they claim is compositional, although I'd rather call it incremental (when the algorithm is modified, the proof is modified accordingly, some parts being reused).
A. Kogan, и E. Petrank. Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel Programming, стр. 141--150. New York, NY, USA, ACM, (2012)
A. Datta, A. Derek, J. Mitchell, и D. Pavlovic. Proceedings of the 2003 ACM workshop on Formal methods in security engineering, стр. 11--23. New York, NY, USA, ACM, (2003)
A. Datta, A. Derek, J. Mitchell, и A. Roy. Electronic Notes in Theoretical Computer Science, 172 (0):
311 - 358(2007)<ce:title>Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin</ce:title>.
S. Tasiran, A. Sezgin, и S. Quadeer. Design and Validation of Concurrent Systems, 09361, Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, (2010)
M. Kühnrich, и U. Nestmann. Proceedings of the Joint 11th IFIP WG 6.1 International Conference FMOODS '09 and 29th IFIP WG 6.1 International Conference FORTE '09 on Formal Techniques for Distributed Systems, стр. 198--212. Berlin, Heidelberg, Springer-Verlag, (2009)
D. Hughes. (2004)cite arxiv:math/0408282
Comment: Appears in Annals of Mathematics, 2006. 5 pages + references. Version
1 is submitted version; v3 is final published version (in two-column format
rather than Annals style). Changes for v2: dualised definition of
combinatorial truth, thereby shortening some subsequent proofs; added
references; corrected typos; minor reworking of some sentences/paragraphs;
added comments on polynomial-time correctness (referee request). Changes for
v3: corrected two typos, reworded one sentence, repeated a citation in Notes
section.
S. Owre, J. Rushby, N. Shankar, и F. von Henke. том 670 из Lecture Notes in Computer Science, стр. 482--500. Odense, Denmark, Springer-Verlag, (апреля 1993)