PaxosLease in Relativistic Inertial Frames

1. Introduction

• Classical lease safety requires at most one holder at any time, while liveness requires a crashed holder not to block the system.A lease grants one holder exclusive, time-limited authority, after which grantors may pass it on without hearing from the old holder.Source: §1 · p. 1
• Spacelike-separated events can have opposite time orders in different inertial frames, and no clock or measurement protocol removes that disagreement.The Lorentz transformation mixes space and time while preserving the speed of light.Source: §1 · p. 1
• If expiry P and a different holder’s acquisition Q are spacelike separated, observers can disagree whether the next lease starts before the previous one expires.The classical timing rules do not prevent this separation, while liveness rules out waiting for a signal from P because the holder may crash there.Source: §1 · p. 1
• The note asks how to make safety observer-agreeable and what PaxosLease [1] [2] must change to satisfy the restated property.Its motivating relay cannot arbitrate competing probes, so they use leases to exclude one another from commanding it.Source: §1 · p. 2

2. PaxosLease

• PaxosLease uses Paxos ballots and prepare/accept rounds decided by majorities to agree on who holds a lease for a limited time.Unlike Paxos, acceptors store nothing on disk; the version discussed omits optional early release.Source: §2 · p. 2
• A proposer starts its lease timer when sending Prepare and acquires the lease if a majority accepts before that timer expires.It may send Accept after a majority answers if none reports a live lease, or if the only reported lease is its own and is being renewed.Source: §2 · p. 2
• Acceptors promise to reject smaller ballots, report live leases, and refuse an Accept that would replace another owner’s live lease.A higher ballot from the same owner can renew the lease; after the recorded deadline, an acceptor may accept from anyone.Source: §2 · p. 2
• Because acceptors keep promises and leases only in memory, a restarting acceptor loses them and stays silent during quarantine DQ.DP, DA, and DQ are measured on the clock of the participant using each timer; the clocks are treated as ideal until Section 4.3.Source: §2 · p. 2

3. The safety property in relativistic inertial frames

• Classical PaxosLease safety says that at most one proposer holds the lease “at any time,” but that phrase depends on the frame in special relativity.The section identifies expiry P and the next owner’s acquisition Q as the events whose ordering matters.Source: §3 · pp. 2–3
• A participant’s directly measurable time is the proper time read by an ideal clock carried along its worldline.This is distinct from assigning distant events times in a chosen inertial frame.Source: §3 · p. 2
• When expiry P and acquisition Q are spacelike separated, observers in suitable frames can disagree about their order.The figure identifies P as one owner’s expiry and Q as the next owner’s acquisition.Source: §3 · p. 3

3.1. Exclusion definitions

• Each successful attempt gives a lease from acquisition to expiry along its owner’s worldline; renewals by one proposer may overlap, so the conditions compare different proposers.With more than two such leases, each condition applies to every pair.Source: §3.1 · p. 3
• Causal exclusion requires one of two different owners’ lease expiries to lie in the past cone of the other’s acquisition.The causal past and future are defined by which events can be connected by signals traveling no faster than light, making the condition frame-independent.Source: §3.1 · p. 3
• Resource exclusion requires the two owners’ authority regions to be disjoint along each resource worldline.The condition is frame-independent because it is expressed using causal cones.Source: §3.1 · p. 3
• Observer exclusion requires the two owners’ authority intervals on a chosen frame’s time axis to be disjoint.The intervals run from each owner’s acquisition to its expiry, with the expiry endpoint excluded.Source: §3.1 · p. 3

3.2.1. C ⇔E(W) for every W

• Causal exclusion holds exactly when resource exclusion holds on every resource worldline.When causal exclusion holds, the authority regions are disjoint everywhere; when it fails, some resource worldline encounters both owners.Source: §3.2.1 · p. 3

3.2.2. C ⇔F(S ) for every S

• Causal exclusion holds exactly when observer exclusion holds in every inertial frame.The proof uses causal order, which survives every boost, and rules out frames in which both owners’ authority intervals are disjoint in opposite orders.Source: §3.2.2 · pp. 3–4

3.2.4. E(W0) ⇏F(S )

• Resource exclusion on one worldline does not imply observer exclusion in every frame.Source: §3.2.4 · p. 4

3.2.6. F(S ) ⇏E(W0)

• Observer exclusion in one frame does not guarantee resource exclusion on a given worldline.Figure 3(b) shows F(S) holding while both owners’ regions overlap on Wb; observers moving from P’s side toward Q’s at 0.15c–0.95c see overlap.Source: §3.2.6 · p. 4

• Correct resource execution follows if holder-to-resource messages travel at light speed and are processed in arrival order.Source: §3.3 · p. 4
• The old owner’s commands, sent before expiry P, arrive before light from P reaches the resource.Source: §3.3 · p. 4
• The new owner’s commands, sent at or after acquisition Q, arrive no earlier than light from Q, and J+(Q) ⊆J+(P) orders them after the old owner’s commands.Source: §3.3 · p. 4

4.1. Relativistic Doppler factor

• The relativistic Doppler factor k = γ(1+β) stretches the interval between arriving proposer ticks; k is specific to a participant pair.When the pair’s relative-speed bound is unknown, an acceptor uses kmax based on an assumed speed bound.Source: §4.1 · p. 5

4.2. Containment

• At least kDP of acceptor exclusion places its end no earlier than light from the lease expiry arrives, regardless of participant separation.The proposer starts its attempt timer at Prepare; if acquisition succeeds, that timer becomes the lease timer.Source: §4.2 · p. 5
• For any two leases held by different proposers, one lease’s expiry lies in the past cone of the other’s acquisition, provided acceptors retain granted leases.The retention rules prevent a live lease from being replaced by another owner or cleared early.Source: §4.2 · p. 5

4.3. Quarantine

• After restart, an acceptor waits kmaxDP before responding, placing it in the future cone of every forgotten lease expiry.A Prepare arriving during quarantine receives no answer.Source: §4.3 · p. 6

5. Discussion

• The results require light-speed, arrival-ordered commands and assume flat spacetime and inertial participants.The paper describes flat-spacetime special relativity as a good approximation far from large masses and a poor one near them.Source: §5 · p. 6