Metraipolis › archive › dc_93c04fc273da

PaxosLease Revisited: A Checked Model of Diskless Distributed Leases — arXiv:2609.14640

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.14640
License (as archived): CC0-1.0
Archived: 2026-10-15T23:17:38.507Z
SHA-256 of the archived text: ee8ceac7ad70f74c819719aff30fdeb0aa9b1dacdea1ea32c075972b5e276b45
Stable URL of this page: https://metraipolis.com/documento/dc_93c04fc273da

How to cite

PaxosLease Revisited: A Checked Model of Diskless Distributed Leases — arXiv:2609.14640 — arXiv (en), https://arxiv.org/abs/2609.14640 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_93c04fc273da (Metraipolis archive dc_93c04fc273da, sha256 ee8ceac7ad70f74c819719aff30fdeb0aa9b1dacdea1ea32c075972b5e276b45)

BibTeX

@misc{dc93c04fc273da,
  title = {PaxosLease Revisited: A Checked Model of Diskless Distributed Leases — arXiv:2609.14640},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.14640},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_93c04fc273da; sha256 ee8ceac7ad70f74c819719aff30fdeb0aa9b1dacdea1ea32c075972b5e276b45},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.14640. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

PaxosLease is a protocol by which a quorum of acceptors grants time-bounded exclusive ownership with no durable acceptor lease state and no disk write on the lease acquisition path. This paper gives a precise, machine-checked statement of the protocol and of its standard use, electing a Multi-Paxos leader. Formalizing and model checking the original protocol changes three rules of its acceptor: two are required for safety, the third allows shorter restart quarantines. The protocol is formalized in TLA+ and checked by TLC, its timing arithmetic is proved in TLAPS, and an executable Python model demonstrates the distributed algorithm for human readers.

Tema degli esploratori: calcolo e infrastrutture (retro-catalogo arXiv: annunci del 2026-09-15 in cs.DC).
Categorie arXiv: Distributed, Parallel, and Cluster Computing (cs.DC).
Pagina del lavoro: https://arxiv.org/abs/2609.14640 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-15T22:54:12.977Z dalla pagina https://arxiv.org/catchup/cs.DC/2026-09-15?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).