pith. sign in

arxiv: 2605.19531 · v1 · pith:F34BE5ZHnew · submitted 2026-05-19 · 💻 cs.DC

Conflict-Freedom as a Progress Condition

Petr Kuznetsov , Pierre Sutra , Guillermo Toyos-Marfurt This is my paper

Pith reviewed 2026-05-20 02:21 UTC · model grok-4.3

classification 💻 cs.DC
keywords conflict-freedomprogress conditionobstruction-freedomlinearizabilityuniversal constructioncommit-adopt objectread-write shared memorysequential objects
0
0 comments X

The pith

Every sequential object has a read-write conflict-free linearizable implementation.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines conflict-freedom as a progress condition under which an operation completes whenever it runs long enough without overlapping incomplete non-commuting operations. This generalizes obstruction-freedom by permitting concurrent operations that commute with each other. The authors prove that every sequential object admits a linearizable implementation in read-write shared memory that satisfies this condition. Their proof rests on a novel generalization of the commit-adopt object that detects conflicts and fixes linearization points for arbitrary objects.

Core claim

Conflict-freedom guarantees progress to an operation that runs in isolation from non-commuting operations. We show that this condition is universal: there exists a read-write implementation, for any sequential object, that is both linearizable and conflict-free. The construction relies on a generalized commit-adopt object that correctly handles conflict detection and linearization for arbitrary operation semantics.

What carries the argument

Generalized commit-adopt object that detects conflicts between operations and determines their linearization order for any sequential object.

Load-bearing premise

A generalized commit-adopt object can be implemented to correctly detect conflicts and establish linearization points for every arbitrary sequential object.

What would settle it

An execution in the proposed construction that produces a non-linearizable history, or a specific sequential object for which no read-write conflict-free linearizable implementation exists.

Figures

Figures reproduced from arXiv: 2605.19531 by Guillermo Toyos-Marfurt, Petr Kuznetsov, Pierre Sutra.

Figure 1
Figure 1. Figure 1: Executions on a shared counter under (a) conflict-freedom and (b) weak conflict-freedom. Brackets [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Examples of (a) conflict-resolving and (b) conflict-forgetting executions on a shared counter. In both [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
read the original abstract

An obstruction-free implementation guarantees progress to every operation that is given enough time to take steps in isolation. But, as we show in this paper, the mere presence of concurrent operations alone does not have to prevent progress; only incomplete conflicting (non-commuting) operations may do so. This progress condition, that we call conflict-freedom, is a natural generalization of obstruction-freedom that promises efficient implementations for objects exhibiting semantic commutativity. We show that, as with obstruction-freedom, every sequential object has a read-write conflict-free linearizable implementation. Our conflict-free universal construction is based on a novel generalization of the instrumental commit-adopt object, interesting in its own right.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper introduces conflict-freedom as a progress condition generalizing obstruction-freedom: an operation makes progress provided no incomplete conflicting (non-commuting) operations exist. It claims that every sequential object admits a linearizable implementation from read-write registers under this condition, via a novel generalization of the commit-adopt object that detects conflicts and assigns linearization points.

Significance. If correct, the result strengthens the obstruction-free universal construction by weakening the progress assumption to exploit semantic commutativity, potentially enabling more efficient implementations for objects such as sets or counters. The generalized commit-adopt object is presented as independently interesting.

major comments (1)
  1. The central claim rests on the correctness of the generalized commit-adopt object introduced for arbitrary sequential objects. The manuscript must supply an explicit lemma (or §4.2) proving that conflict detection correctly identifies non-commuting pairs and that linearization points are placed only after all prior conflicting operations complete, for every possible commutativity relation; without this, the reduction to the universal construction does not go through.
minor comments (2)
  1. Clarify in the abstract and §1 whether conflict-freedom is strictly weaker than obstruction-freedom or incomparable in some schedules.
  2. Add a small example (e.g., a set with insert/delete) showing how the generalized commit-adopt permits concurrent non-conflicting operations.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the constructive feedback. We address the major comment below and will revise the paper to strengthen the presentation of the proof.

read point-by-point responses

  1. Referee: The central claim rests on the correctness of the generalized commit-adopt object introduced for arbitrary sequential objects. The manuscript must supply an explicit lemma (or §4.2) proving that conflict detection correctly identifies non-commuting pairs and that linearization points are placed only after all prior conflicting operations complete, for every possible commutativity relation; without this, the reduction to the universal construction does not go through.

    Authors: We agree that an explicit lemma is required to rigorously establish the correctness of the generalized commit-adopt object for arbitrary sequential objects. In the revised manuscript we will add a dedicated lemma (placed in a new §4.2) that proves two properties for any commutativity relation: (i) the conflict-detection mechanism returns true precisely when a pair of operations fails to commute under the object's sequential specification, and (ii) a linearization point is assigned to an operation only after every prior conflicting operation has completed. The lemma will be stated and proved in full generality, thereby justifying the reduction to the universal construction. revision: yes

Circularity Check

0 steps flagged

Self-contained construction using novel generalized commit-adopt object defined and proved internally

full rationale

The paper defines a novel generalization of the commit-adopt object to handle conflict detection and linearization for arbitrary sequential objects, then uses it to construct a read-write conflict-free linearizable implementation. This follows the standard pattern of introducing an auxiliary object and proving its properties within the same paper against external definitions of linearizability and read-write registers. No step reduces the central claim to a self-definition, fitted parameter, or self-citation chain by construction. The derivation remains independent of the target result and qualifies as self-contained against prior literature benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claim rests on standard definitions of linearizability and sequential objects plus the novel definition of conflict-freedom; no free parameters are introduced and no new physical entities are postulated.

axioms (2)
  • domain assumption Linearizability is the correctness condition for the implementation.
    Invoked when stating the universal construction produces linearizable implementations.
  • standard math Every sequential object has a well-defined sequential specification.
    Used as the base for the universal construction claim.
invented entities (2)
  • Conflict-freedom progress condition no independent evidence
    purpose: Defines when operations are allowed to make progress based on absence of conflicting incomplete operations.
    Newly defined in the paper as a natural generalization of obstruction-freedom.
  • Generalized commit-adopt object no independent evidence
    purpose: Instrumental object used to build the conflict-free universal construction.
    Novel generalization introduced to support the main result.

pith-pipeline@v0.9.0 · 5636 in / 1310 out tokens · 36833 ms · 2026-05-20T02:21:23.990661+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

39 extracted references · 39 canonical work pages

  1. [1]

    IJsbrand Jan Aalbersberg and Grzegorz Rozenberg. 1988. Theory of traces.Theoretical Computer Science60, 1 (1988), 1–82

    work page 1988

  2. [2]

    Ganger, Garth R

    Michael Abd-El-Malek, Gregory R. Ganger, Garth R. Goodson, Michael K. Reiter, and Jay J. Wylie. 2005. Fault-scalable Byzantine fault-tolerant services. InProceedings of the Twentieth ACM Symposium on Operating Systems Principles (Brighton, United Kingdom)(SOSP ’05). Association for Computing Machinery, New York, NY, USA, 59–74

    work page 2005

  3. [3]

    Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. 1993. Atomic snapshots of shared memory.J. ACM40, 4 (Sept. 1993), 873–890

    work page 1993

  4. [4]

    Agarwal and M

    A. Agarwal and M. Cherian. 1989. Adaptive backoff synchronization techniques.SIGARCH Comput. Archit. News17, 3 (April 1989), 396–406. doi:10.1145/74926.74970

    work page doi:10.1145/74926.74970 1989

  5. [5]

    Schneider

    Bowen Alpern and Fred B. Schneider. 1987. Recognizing Safety and Liveness.Distributed Comput.2, 3 (1987), 117–126

    work page 1987

  6. [6]

    James Aspnes and Maurice Herlihy. 1990. Wait-Free Data Structures in the Asynchronous PRAM Model. InProceedings of the 2nd Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA ’90, Island of Crete, Greece, July 2-6,

    work page 1990

  7. [7]

    Association for Computing Machinery, New York, NY, USA, 340–349

    work page

  8. [8]

    Hagit Attiya, Armando Castañeda, Danny Hendler, and Matthieu Perrin. 2022. Separating lock-freedom from wait- freedom at every level of the consensus hierarchy.J. Parallel Distributed Comput.163 (2022), 181–197

    work page 2022

  9. [9]

    Hagit Attiya, Rachid Guerraoui, Danny Hendler, and Petr Kuznetsov. 2009. The complexity of obstruction-free implementations.J. ACM56, 4 (2009), 24:1–24:33

    work page 2009

  10. [10]

    2004.Distributed computing: fundamentals, simulations, and advanced topics

    Hagit Attiya and Jennifer Welch. 2004.Distributed computing: fundamentals, simulations, and advanced topics. Vol. 19. John Wiley & Sons, New York, NY, USA

    work page 2004

  11. [11]

    James Cowling, Daniel Myers, Barbara Liskov, Rodrigo Rodrigues, and Liuba Shrira. 2006. HQ replication: a hybrid quorum protocol for byzantine fault tolerance. InProceedings of the 7th Symposium on Operating Systems Design and Implementation(Seattle, Washington)(OSDI ’06). USENIX Association, USA, 177–190

    work page 2006

  12. [12]

    Flaviu Cristian, Houtan Aghili, Ray Strong, and Danny Dolev. 1995. Atomic broadcast: From simple message diffusion to Byzantine agreement.Information and Computation118, 1 (1995), 158–179

    work page 1995

  13. [13]

    Tudor David and Rachid Guerraoui. 2016. Concurrent Search Data Structures Can Be Blocking and Practically Wait-Free. InSPAA, Christian Scheideler and Seth Gilbert (Eds.). Association for Computing Machinery, New York, NY, USA, 337–348

    work page 2016

  14. [14]

    Fischer, Nancy A

    Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. 1985. Impossibility of Distributed Consensus with one Faulty Process.JACM32, 2 (April 1985), 374–382

    work page 1985

  15. [15]

    Tuanir França Rezende and Pierre Sutra. 2020. Leaderless State-Machine Replication: Specification, Properties, Limits. In34th International Symposium on Distributed Computing (DISC 2020) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 179), Hagit Attiya (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 24:1–24:1...

    work page doi:10.4230/lipics.disc.2020.24 2020

  16. [16]

    Eli Gafni. 1998. Round-by-round fault detectors (extended abstract): unifying synchrony and asynchrony. InPODC. Association for Computing Machinery, New York, NY, USA, 143–152

    work page 1998

  17. [17]

    Rachid Guerraoui, Maurice Herlihy, and Bastian Pochon. 2005. Toward a theory of transactional contention managers. InProceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Distributed Computing(Las Vegas, NV, USA)(PODC ’05). Association for Computing Machinery, New York, NY, USA, 258–264

    work page 2005

  18. [18]

    Maurice Herlihy. 1991. Wait-Free Synchronization.ACM Trans. Program. Lang. Syst.13, 1 (1991), 124–149

    work page 1991

  19. [19]

    Maurice Herlihy, Victor Luchangco, and Mark Moir. 2003. Obstruction-Free Synchronization: Double-Ended Queues as an Example. InProceedings of the 23rd International Conference on Distributed Computing Systems (ICDCS ’03). IEEE Computer Society, USA, 522

    work page 2003

  20. [20]

    2008.The art of multiprocessor programming

    Maurice Herlihy and Nir Shavit. 2008.The art of multiprocessor programming. Morgan Kaufmann, San Francisco, CA, USA

    work page 2008

  21. [21]

    Maurice Herlihy and Nir Shavit. 2011. On the Nature of Progress. InOPODIS (Lecture Notes in Computer Science, Vol. 7109), Antonio Fernández Anta, Giuseppe Lipari, and Matthieu Roy (Eds.). Springer, Berlin, Heidelberg, 313–328. 18 Petr Kuznetsov, Pierre Sutra, and Guillermo Toyos-Marfurt

    work page 2011

  22. [22]

    Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects.ACM Trans. Program. Lang. Syst.12, 3 (1990), 463–492

    work page 1990

  23. [23]

    Petr Kuznetsov and Nathan Josia Schrodt. 2026. Resolving Conflicts with Grace: Dynamically Concurrent Universality. In29th International Conference on Principles of Distributed Systems (OPODIS 2025) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 361). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 33:1–33:29

    work page 2026

  24. [24]

    Petr Kuznetsov, Pierre Sutra, and Guillermo Toyos-Marfurt. 2026. Pending Conflicts Make Progress Impossible. arXiv:2602.04013 [cs.DC]

    work page arXiv 2026

  25. [25]

    Leslie Lamport. 1977. Proving the Correctness of Multiprocess Programs.IEEE Trans. Software Eng.3, 2 (1977), 125–143

    work page 1977

  26. [26]

    Leslie Lamport. 1998. The Part-Time Parliament.ACM Transactions on Computer Systems16, 2 (May 1998), 133–169

    work page 1998

  27. [27]

    Leslie Lamport. 2005. Generalized consensus and Paxos. Microsoft Research technical report MSR-TR-2005-33

    work page 2005

  28. [28]

    Loui and H.H

    M.C. Loui and H.H. Abu-Amara. 1987. Memory requirements for agreement among unreliable asynchronous processes. Advances in Computing Research4 (1987), 163–183

    work page 1987

  29. [29]

    N.A. Lynch. 1996.Distributed Algorithms. Morgan Kaufmann, San Francisco, CA, USA

    work page 1996

  30. [30]

    Mazurkiewicz

    Antoni. Mazurkiewicz. 1985. Semantics of concurrent systems: A modular fixed-point trace approach. InAdvances in Petri Nets 1984, G. Rozenberg (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 353–375

    work page 1985

  31. [31]

    Andersen, and Michael Kaminsky

    Iulian Moraru, David G. Andersen, and Michael Kaminsky. 2013. There is more consensus in Egalitarian parliaments. InProceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles(Farminton, Pennsylvania)(SOSP ’13). Association for Computing Machinery, New York, NY, USA, 358–372

    work page 2013

  32. [32]

    Sean Ovens. 2024. The Space Complexity of Consensus from Swap.J. ACM71, 1 (2024), 1:1–1:26

    work page 2024

  33. [33]

    Fernando Pedone and André Schiper. 1999. Generic Broadcast. InDistributed Computing, Prasad Jayanti (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 94–106

    work page 1999

  34. [34]

    Fedor Ryabinin, Alexey Gotsman, and Pierre Sutra. 2025. Making Democracy Work: Fixing and Simplifying Egalitarian Paxos. InOPODIS (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 22:1–22:19

    work page 2025

  35. [35]

    Johannes Schneider and Roger Wattenhofer. 2009. Bounds on Contention Management Algorithms. InAlgorithms and Computation, Yingfei Dong, Ding-Zhu Du, and Oscar Ibarra (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 441–451

    work page 2009

  36. [36]

    Florian Suri-Payer, Matthew Burke, Zheng Wang, Yunhao Zhang, Lorenzo Alvisi, and Natacha Crooks. 2021. Basil: Breaking up BFT with ACID (transactions). InProceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles(Virtual Event, Germany)(SOSP ’21). Association for Computing Machinery, New York, NY, USA, 1–17

    work page 2021

  37. [37]

    Michael Whittaker, Neil Giridharan, Adriana Szekeres, Joseph Hellerstein, and Ion Stoica. 2021. SoK: A Generalized Multi-Leader State Machine Replication Tutorial.Journal of Systems Research1 (09 2021). doi:10.5070/SR31154817

    work page doi:10.5070/sr31154817 2021

  38. [38]

    Leqi Zhu. 2021. A Tight Space Bound for Consensus.SIAM J. Comput.50, 3 (2021), STOC16–18–STOC16–29

    work page 2021

  39. [39]

    Piotr Zieliński. 2005. Optimistic Generic Broadcast. InDistributed Computing, Pierre Fraigniaud (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 369–383. A Full Proofs A.1 Relationships Among Liveness Conditions Proposition 3.3.The progress conditions form the following hierarchy: wait-freedom=⇒conflict-freedom=⇒weak conflict-freedom=⇒obstruction-fr...

    work page 2005