{"id":"8d3c2a00-7aea-498c-af1c-db070aaa83df","arxiv_id":"2509.07158","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.5,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"Bodega uses all-to-all roster leases to let any chosen replica serve linearizable reads locally even when writes are concurrent, cutting average client read latency 5.6x to 13.1x in tests.","lead":"This paper presents Bodega, a consensus protocol that lets any replica in a cluster answer a client's read immediately, even while writes are happening elsewhere. It matters because geodistributed databases and coordination services can serve reads from the nearest site without sacrificing linearizable consistency, improving user-perceived latency.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Roster-transition stale grants: a node that adopts a new ballot can keep old-ballot grants in its endowed set, so Condition (1) can hold while a majority still runs the old roster, breaking proof Case #1.","rationale":"The reader's weakest assumption was bounded clock drift. Clock drift is a standard, explicitly acknowledged prerequisite of any lease protocol and does not pinpoint a flaw in the protocol's own transition logic. The issue I found is more specific and more load-bearing: the written algorithm, as summarized in Figure 17, does not guarantee that the endowed set used in Condition (1) contains only grants for the node's current roster after a roster change. If a node counts stale old-ballot grants, the proof's Case #1 step ('it is impossible because the latest ballot on at least a majority is bal') is unjustified. This is an internal concern about the described protocol, not about external assumptions: the text of §3.3.2 promises that holding leases are revoked, but the pseudo-code omits that step and even ignores old-ballot Revoke messages. I agree with the reader that the verdict should remain conditional, but the condition should include a concrete fix or validation of the roster-transition stale-grant issue. The paper's positive contributions—the roster concept, write-quorum-covering-responders, optimistic holding, and the evaluation—are not undermined by this concern if the transition logic is corrected and model-checked. No ad hominem is intended; the issue is a technical gap between the prose and the protocol listing.","tokens_in":39443,"tokens_out":20821,"duration_ms":211095,"concrete_test":"Extend the Appendix B TLA+ model to track, for each node, the set of lease grants it currently holds as grantee, each tagged with the ballot of the roster it was granted for, together with asynchronous delivery of Heartbeat and Revoke messages. Model-check a 5-node (or 3-node) configuration in which one node adopts a higher ballot while the remaining nodes stay on the old ballot. The check should assert the stable-roster invariant: whenever a node serves a local read, every grant in its endowed set carries the node's current ballot. If TLC reaches a state where |endowed| >= m but some endowed grant is tagged with a lower ballot, the invariant is violated and the proof must be repaired (e.g., by clearing or filtering old-ballot grants before checking Condition (1)).","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The safety proof in §4.2 rests on Condition (1) in §3.3.1: when a responder S has |endowed| >= m, S may infer that at least a majority of nodes share the same latest <bal,ros> as S, and therefore no write can commit on a higher ballot. The protocol text in §3.3.2 says a node 'invokes the revoke_leases(bal) procedure synchronously to ensure that all the leases it is granting or holding with the older ballot bal are safely revoked and removed.' However, the detailed transition code in Figure 17 does not implement the 'holding' half. do_revoke_leases (lines 15-19) clears {}guarding and waits only on {}endowing, i.e., the leases S granted as grantor; it never purges S's grantee-side {}endowed set. Worse, Recv leaseRevoke (line 18) removes a grantor only if 'bal >= current ballot', so after S has already adopted a higher ballot, a Revoke carrying the old ballot is ignored and the stale grant remains in {}endowed until timer expiry. Consequently, when S adopts a new ballot bal' while its peers are still on bal, S's {}endowed can still contain a majority of old-ballot grants, and Condition (1) can pass for bal' even though no majority has adopted bal'. In that window, an old-ballot leader can commit a write without S (if S was not a responder under bal), and S can serve a linearizable read on bal' that misses that committed write, violating the Case #1 step and the 'at most one stable roster' claim. The TLA+ model in Appendix B does not model per-grantee endowed sets or Revoke handling; it only keeps one global grant per node, so this transition window is not explored by the model check.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Bodega, a consensus protocol that aims to serve linearizable reads locally at designated responder replicas even while writes are in flight. It introduces the roster, a ballot-tagged cluster metadata that assigns a leader and per-key responder sets, and protects roster agreement with all-to-all 'roster leases' that generalize leader leases. The authors argue that a node holding a majority of lease grants can serve reads locally, that writes commit only after reaching all active responders, and that optimistic holding and early accept notifications keep reads local during write interference. They implement Bodega and prior work in Vineyard, an async-Rust KV store, and report 5.6–13.1x read-latency improvements over prior linearizable-read protocols on WAN clusters, comparable write throughput, fast roster changes, and YCSB performance matching sequentially consistent etcd and ZooKeeper. Correctness is argued via a short proof sketch (§4.2) and a PlusCal/TLA+ model checked for a 3-node configuration (Appendix B).","tokens_in":39856,"tokens_out":10469,"duration_ms":92915,"significance":"If the protocol as written were sound, this would be a meaningful advance: it is the first self-contained consensus-based scheme we are aware of that extends local linearizable reads to arbitrary responders under active write interference, and the roster abstraction is a clean generalization of leadership. The implementation breadth and comparison against several protocols and production systems are valuable, and the reported speedups are substantial and measured rather than fitted to the claims. The paper also ships machine-checked TLA+ (though, as discussed below, an idealized lease model). The central correctness claim, however, rests on a stale-lease transition invariant that the detailed pseudocode does not preserve, so the contribution is currently not established as presented.","major_comments":[{"comment":"The revoke procedure does not implement the prose. §3.3.2 says a node S 'invokes the revoke_leases(bal) procedure synchronously to ensure that all the leases it is granting or holding with the older ballot bal are safely revoked and removed,' but do_revoke_leases (Figure 17 lines 15–19) clears only {}guarding (S's grantor-side guard set) and waits only on {}endowing; it never purges S's grantee-side {}endowed or {}guarded. Moreover, Recv leaseRevoke (line 18) removes the sender only if bal >= current ballot, so a Revoke carrying an old ballot is ignored by a node that has already adopted a higher ballot, and the stale grant remains until timer expiry. Consequently, when S adopts a new ballot bal' while peers are still on bal, S's {}endowed can still contain a majority of old-ballot grants; Condition (1) in §3.3.1 can then hold for bal' even though no majority has adopted bal'. In that window an old-ballot leader can commit a write without S, and S can serve a local read on bal' that misses that committed write, violating Case #1 of the proof in §4.2 and the claimed 'at most one stable roster' invariant. The pseudocode must clear all grantee-side entries whose roster ballot is not current at the moment of adopting a new ballot, and the Recv leaseRevoke predicate must also remove stale grants when the received ballot is older than the current ballot.","section":"§3.3.2, Figure 17; §4.2 Case #1"},{"comment":"The model-checked TLA+ specification does not exercise the revocation/transition logic that is the basis of the bug above. The global `grants` set and the `Lease` macro replace each grantor's grant with a single grant to the new roster, and the comment explicitly says messages are 'removed' to model expiry 'probably making way for switching to a different roster.' There are no per-grantee {}endowed sets, no Guard/Revoke messages, and no ordering constraint on revocation before adopting a higher ballot. The check of 3 nodes, 3 ballots, 2 writes, and 2 reads therefore cannot detect stale-grant violations of Condition (1), and the statement in Contribution 5 that the TLA+ specification verifies the protocol should be scoped to the idealized lease model.","section":"Appendix B (TLA+ model)"},{"comment":"The proof of Case #3 assumes that for any size-m subset E of S's {}endowed, at least one grantor P accepted the committed write W 'before granting to S,' implying thresh_p >= x. But thresh_p is recorded only in the initial Guard (Figure 17 line 24), and renewals (lines 25–28) do not update it. If the grant counted in E is an old-ballot grant that was established before W committed, thresh_p can be below x even though P is in a majority; the argument requires either that grants carry the ballot and are refreshed with fresh thresholds, or that old grants are provably purged at roster transitions. Neither is guaranteed by the present pseudocode.","section":"§4.2 Case #3"}],"minor_comments":[{"comment":"The guard 'bal >= current ballot' for Recv leaseRevoke is not explained and appears to have the wrong sign for the stale-grant case; the intended semantics should be stated in the text.","section":"Figure 17, line 18"},{"comment":"The phrase 'cheated' model in the inlined comments should be reflected in the main text's description of the formal verification, so readers know the TLA+ result does not cover the lease revocation ordering.","section":"Appendix B"},{"comment":"The evaluation figures do not report error bars, confidence intervals, or the number of runs; please state the run-to-run variability.","section":"§6, Figures 8–12, 14–15"},{"comment":"Table 1 cells contain '#' and 'G' markers that are not defined in the caption; the caption only defines the filled circle symbols.","section":"Table 1"},{"comment":"The sentence beginning 'Bodega 1 shortens' should read 'Bodega (1) shortens'.","section":"§6.2"},{"comment":"Figure 5's legend ('#20 x4', '#32 x1', '#11 x1') is cryptic without a pointer to §3.3; consider explaining the notation in the caption.","section":"Figure 5"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a strong systems contribution if the revocation gap is fixed; the evaluation and writing are otherwise careful. I would ask the authors to repair the pseudocode to implement the grantee-side purge, adjust the Revoke handling, and re-run the model checker with a non-cheated lease model. The 'first protocol' novelty claim should also be checked against the missing citations in the reference list of earlier read-leases variants (e.g., Chandra et al. 2016 is cited but not discussed in depth)."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing you should know: the headline contribution is real. All-to-all roster leases, optimistic holding, and early accept notifications form a coherent design that plausibly delivers local linearizable reads under write load, and the evaluation is one of the more thorough ones I've seen for this class of protocols. The paper deserves a serious referee. But it has a safety bug in the transition logic that the TLA+ model does not cover, so the result is conditional at best.\n\nWhat's new: the all-to-all generalization of leader/quorum leases is a natural but original step, and the paper works out the practical details—piggybacking on heartbeats, lightweight rosters, smart coverage, request batching—with real WAN experiments against EPaxos, PQR, Quorum Leases, etcd, and ZooKeeper. The 5.6-13.1x read speedup under write interference is credible from the plots. The implementation is substantial (25.6k lines Rust) and several protocols share one codebase, which raises confidence in fairness of comparison.\n\nThe soft spot is load-bearing. Section 3.3.2 says a node invoking revoke_leases(bal) will safely revoke all leases it is 'granting or holding' with the old ballot. Figure 17's do_revoke_leases only clears the grantor-side guarding set and waits on endowing; it never purges the grantee-side endowed set. And Recv leaseRevoke at line 18 ignores a Revoke carrying a ballot older than the node's current ballot. So after S adopts a higher ballot, old-ballot grants from peers can remain in S's endowed set until timer expiry. That can make Condition (1) pass on the new ballot while a majority still runs the old roster, exactly the window Case #1 of the proof assumes impossible. Old-leader writes can commit outside S's view, and S can serve a stale local read. The TLA+ spec in Appendix B uses one global set of lease grants rather than per-node endowed sets, so model checking cannot see this. This is not a nitpick; it's a direct mismatch between the prose promise and the implementation guide.\n\nOther issues are minor: the 'first' claim is overstrong given Chandra et al. 2016 and Bi et al. 2022 provide local-read algorithms, though those differ in model; the TLA+ model is admittedly simplified; no error bars; code not yet released. None of those alone would be fatal.\n\nIf the authors fix the revocation handling (e.g., discard held grants on ballot adoption, or accept and apply old-ballot Revokes), the protocol idea stands and the paper is a strong systems contribution. As written, I can't accept the safety proof. This deserves peer review and a major revision, not a desk reject.","headline":"The roster-lease idea is genuinely new and the evaluation is strong, but the transition logic as written has a safety bug that breaks the proof; a major revision is needed.","tokens_in":40403,"tokens_out":3755,"would_cite":true,"duration_ms":35756,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Bodega claims to be the first consensus protocol that serves linearizable reads locally from any designated replica even while interfering writes are in progress, via all-to-all roster leases.","keywords":["consensus","linearizable reads","leases","roster","local reads","replication","Paxos","wide-area systems"],"falsifier":"Crash or suspend a node long enough for clock drift or lease timers to violate the bounded-drift assumption, then check whether two nodes can simultaneously hold majority lease sets for different roster ballots; if the protocol's own stable condition ever allows that, a local read can miss a committed write and the central claim is false. A cheaper version: instrument the implementation to log grantor-side and grantee-side expiration times under skewed clocks and test whether the guard-then-renew invariant from the lease background is ever reversed.","tokens_in":39266,"feed_emoji":"⚡","tokens_out":7020,"duration_ms":61881,"temperature":0.7,"pith_summary":"Linearizable reads — reads that observe every acknowledged write in real time — usually force a client to contact a leader or a quorum, which is slow across wide-area networks. Bodega claims to break this constraint: any replica designated as a responder can answer reads locally, at any time, even while writes to the same key are actively committing. The protocol protects a generalization of leadership called the roster with all-to-all roster leases, and requires writes to reach all active responders before committing. The paper reports 5.6x–13.1x faster average read latency than prior approaches under moderate write interference, with comparable write performance, in a replicated key-value store implementation.","feed_headline":"Any replica can answer linearizable reads locally, even during writes","feed_subtitle":"A consensus protocol with roster leases keeps reads near clients while writes proceed, matching sequential-consistency services.","key_machinery":"The central mechanism is the roster lease, an all-to-all generalization of the one-to-one leader lease. Each replica grants timed, renewable leases for a specific roster (a ballot number together with the leader and per-key responder assignments) to every peer; piggybacked on heartbeats, these leases establish a stable roster when a node holds a majority of grants. A stable-roster check also requires the node to have committed every slot below a safety threshold learned from peers, and local reads are served only after that check passes. This off-critical-path leasing is what makes local reads safe: a write cannot commit before all active responders have acknowledged it, so a responder with a stable roster never misses a committed value.","core_discovery":"On its own terms, Bodega's discovery is that a consensus protocol can keep reads local without quiet periods or leader round-trips if the cluster agrees not just on who leads but on who may answer reads. That agreement is the roster, and it is protected by roster leases: every node grants timed leases to every other node for the current roster ballot, so holding leases from a majority of nodes proves that no other stable roster exists. Once that condition holds, a responder can serve the latest committed value directly, and when an interfering write is still in flight it can optimistically hold the read until the write commits or enough early accept notifications arrive. Bodega therefore locates reads at arbitrary replicas at all times, at the cost of requiring writes to be acknowledged by all responders.","pith_inferences":["Roster leases may protect other rare metadata beyond read responders — membership, asymmetric quorums, node-specific hints — extending local-read safety to those mutable settings.","The read-locality benefit is largest when the roster is tuned to read-heavy, location-skewed keys; an adaptive controller that changes responders as workload skew shifts could realize the paper's anytime promise in production, but that policy is not developed here.","The safety of the scheme depends on bounded clock drift; deployments could add clock-drift monitoring and refuse local reads when drift approaches the bound, a testable safeguard the paper does not specify.","The same all-to-all lease idea might extend to Byzantine fault tolerance by raising the majority threshold to 2f+1 and reusing early accept notifications, but Bodega itself targets crash faults."],"forward_implications":["A client near any responder gets read latency close to a local memory access even while writes to the same key are continuous; the only degraded period after an interfering write lasts about half a majority round trip.","Writes carry a modest tax: they must collect replies from all responders of the key, not just a majority, but the paper measures write throughput as comparable to classic consensus.","Roster changes can be applied proactively in two message rounds, while failure-triggered changes wait for lease expiration, preserving availability under minority faults.","The protocol retains the fault tolerance of classic consensus and needs no external membership or metadata service.","In YCSB workloads, Bodega matches the performance of sequentially consistent etcd and ZooKeeper, which do not offer linearizable local reads."],"supporting_citations":[{"why":"Defines the basic lease primitive and its expiration-based fault tolerance, which Bodega's roster leases generalize.","marker":"[51]"},{"why":"Introduces leader leases on top of Paxos, the one-to-one leasing baseline whose stable-leadership guarantee Bodega extends to arbitrary responder sets.","marker":"[29]"},{"why":"Presents Quorum Leases, the all-to-one leasing approach Bodega generalizes and the main comparison point for read performance under write interference.","marker":"[101]"},{"why":"Describes EPaxos, a leaderless consensus protocol that Bodega compares against as an alternative for wide-area reads and writes.","marker":"[100]"},{"why":"Introduces PQR's near-quorum read protocol, a baseline showing that local reads fail without a protected roster under interference.","marker":"[31]"},{"why":"Defines linearizability, the consistency property that Bodega's local reads are designed to preserve.","marker":"[60]"}],"fun_headline_variants":["Roster leases make any replica a local read point","Bodega: local linearizable reads from any node, anytime","Reads go local even during writes with roster leases","New consensus: serve reads from any replica, no leader hop","Bodega: local reads without quiet periods or leader round-trips"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The protocol's safety rests on the assumption that node clocks never drift apart by more than a fixed small bound, so that lease expiration times cannot overlap in a way that lets two competing rosters both appear stable.","fun_headline_variants_meta":{"raw":{"variants":["Roster leases make any replica a local read point","Bodega: local linearizable reads from any node, anytime","Reads go local even during writes with roster leases","New consensus: serve reads from any replica, no leader hop","Bodega: local reads without quiet periods or leader round-trips"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.0002,"raw_usage":{"total_tokens":1404,"prompt_tokens":1002,"completion_tokens":402,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":618,"completion_tokens_details":{"reasoning_tokens":317}},"tokens_in":618,"tokens_out":402,"duration_ms":3710,"temperature":1.0,"reasoning_tokens":317,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T16:12:57.944524+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Crash or suspend a node long enough for clock drift or lease timers to violate the bounded-drift assumption, then check whether two nodes can simultaneously hold majority lease sets for different roster ballots; if the protocol's own stable condition ever allows that, a local read can miss a committed write and the central claim is false. A cheaper version: instrument the implementation to log grantor-side and grantee-side expiration times under skewed clocks and test whether the guard-then-renew invariant from the lease background is ever reversed.","supporting_citations":[{"cited_title":"Gray and D","cited_arxiv_id":null,"evidence_quote":"Defines the basic lease primitive and its expiration-based fault tolerance, which Bodega's roster leases generalize."}],"review_version":2}