Repository navigation
Releases
Releases · lua-lunet/uvr-core
v0.16.0
The ephemeral-lease core moves into the core
The pivot's whole arc, landed: the advisory locks machinery is core
surface now, not a demo.
The feature set since the pivot
- The CAS lock table is core surface (
locksfeature): hold,
renew, release, break, over one client table, with the generation
watermark that never hands a generation out twice on a lock, the
truthful release (one that retires nothing says so), the
nil-unrepresentableClientId, and the clock-parametricexecute.
The expiry window is the ephemeral lease of the fast-reads design
([VR-2012] §6.3/§6.3.1,
docs/references.md): the primary
answers reads unilaterally only while it holds valid leases from f
other replicas, and a new view starts only after the leases at f + 1
participants expire. The lease arithmetic the cluster owner owns —
the leader lease outlasting the reader lease plus the clock drift
margin, theStartViewChange/DoViewChangequorum rounds as a
safety margin beyond the expiry, no renewal while the cluster is
idle, and the application's own judgement of whether a rare stale
read during a leader crash is noise or an outage — is documented on
the machinery itself (src/locks.rs). - The SPI the machinery is written against is core surface:
StateStore(flush eager, load lazy, a crashed boot distrusts the
state file),BootFencewith itsFenceWord(one file, one status
word, one forced write per transition),CommitHook(a trigger at
each applied commit), andlazy_loadwith its guard stated once. A
consumer implements the store and the fence over its own storage
engine — a heavyweight superblock and WAL, a double-write, a custom
flush — mounts its own hook and its own timeouts, and changes
nothing above the traits. - The demo is scaffold, and only scaffold (
demofeature, renamed
fromdemo-locks): the plain-file store and fence over the demo's
own disk seam (the one placestd::fsis named), the
single-threaded node loop, the resend ledger, the join gossip, and
the PAXE-sealed UDP transport, pinned by revision. - The sans-I/O law is kept: zero default dependencies;
locks
rides the existing optionalserdelane;demoadds the optional
pinned paxe-core. No timers, no WAL, no snapshots, no superblock:
heavy IO is the host's to mount behind the traits. - The release flow verifies the version: a tag publishes only when
the manifest the tag points at declares the tag's version; a
forgotten bump blocks the release instead of shipping a lie. The
release note itself is a reviewed file in the repository
(.github/release-body.md), carried by the tag that earns it.
What's Changed
- The ephemeral-lease core moves into the core: the locks machinery graduates (#162) by @simbo1905 in #166
Full Changelog: v0.15.2...v0.16.0
v0.14.0
What's Changed
- The CI action installs the exact pinned toolchain by @simbo1905 in #141
- State the reference client deployment by @simbo1905 in #142
- The era advances per slot of the reconfiguration and the nomination rides with it by @simbo1905 in #144
- The gateway role, the application protocol note, and the per-slot view-jump law by @simbo1905 in #146
- The 0.14.0 bump by @simbo1905 in #147
Full Changelog: v0.13.1...v0.14.0
v0.13.1
What's Changed
- The manifest meets its tag: the release is 0.13.0, shipping the conformance host over HTTP by @simbo1905 in #133
- The Fuse envelope ends in a promise to the tail ballot: the docs carry the law before the code does by @simbo1905 in #137
- The 0.13.1 patch series: the accept perimeter judges the chain fold, the toolchain pin is load-bearing by @simbo1905 in #140
Full Changelog: v0.13.0...v0.13.1
v0.13.0
What's Changed
- Drive the compliance corpus over HTTP, and ship the conformance host as a binary by @simbo1905 in #130
- Citation graph, compliance HTTP corpus, and paper build fixes by @simbo1905 in #132
Full Changelog: v0.12.0...v0.13.0
v0.12.0
v0.11.0
v0.11.0
Pre-alpha: no compatibility is kept; deletions are outright and the durable formats refuse the files the previous release wrote.
This is the consolidated movement since v0.9.0: the documentation is restructured into one place to look each, every reference the code and the documents make is mechanically resolved, and the leader-assignment question is settled in the protocol rather than in the operator's hands.
The protocol
- NOMINATE leader assignment across reconfiguration (#102): the leader of a view is a ballot outcome, and a reconfiguration that changes the positive-weight sequence would move the arithmetic mid-plan. The NOMINATE letter is a view increment carried as a compare-and-swap at a committed slot: the bump publishes the bumped ballot as current and retained on the same transition, so every §1.3 relation holds at every instant, the leader the old arithmetic elected is the leader the new arithmetic re-elects, and crash mid-transition is a no-op. The weighted solver emits the wrap-only nominations; the era-only jump is admitted and proven safe (ViewJump), so the scaling steps need no rider (#103, #105).
- The ABDICATE command is deleted (#106): a leader that must leave issues a StartViewChange to a higher view and shuts down.
- The drop discipline is codified by name (#108): the frontier clause and the view clause, each refusal named in the durability model and pinned in the public interface tests.
The verification
- The uVRR compliance suite (#94): a language-agnostic corpus of state x message -> state' + outputs cases, one JSON case per transition over the abstract host interface, 73 cases in ten families seeded per Lean rung, each case naming its theorem; the reference runner executes the corpus through the crate's public sans-I/O interface and the exporter's regeneration is a CI gate.
- The flavoured-timeout model (#100): the state enum and the timeout enum are closed, the policy matcher is exhaustive over every pair with no default arm, opinions are the legal family with Sorry carrying the recorded runbook for the unflushed stop, and the timeout-policy tool prints the matcher's answer as living documentation.
- The verification gate runs the Lean lane: formal/uvrr-lean is elaborated on every push (#113).
- The documentation reference gate: every doc comment's references are mechanically resolved — cited documents exist, sections name real headings, decision identifiers and rules and citations resolve — and rustdoc's intra-doc links are hard errors. The external works are cited from one references file. A comment that lies about the section it cites is now a failing build.
The durability boundary
- The boot gate and the termination obligations are stated in one document, uvrr-io-obligations.md, with the host notes pointing at it as the normative source; the compliance suite is the host's artefact, uvrr-host-compliance.md; the reconfiguration rules, reincarnation, rejoin gossip and witnesses, the weighted solver, and the NOMINATE letter are consolidated into uvrr-protocols.md.
- Liveness is stated as host documentation (#101): the resend, the heartbeat, and the retransmit are suggestions the host weighs, never obligations the core prescribes.
Identity and naming
- The (era, view) pair is named Ballot across the crate, the tests, the documents, and the Lean formalisation: the code, the proofs, and the paper speak one vocabulary.
- The crate name is uvrr everywhere: the lib target the hosts dlopen is libuvrr, the environment variable is MAELSTROM_UVRR_STATE_DIR (#95).
- Release tags correspond to the manifest version, verified before the build lanes start (#97).
Harness
- The gate-classification flake is dead (#115, #116): gate roots are unique per process, so two harness binaries cannot collide on the same directory.
- Cargo.lock is committed as policy; the maelstrom adapter is compile-gated so the default test lane never boots the harness; CI runs the fast lane then the full lane.