rsp2k/headscale
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

state, servertest: property-test HA election + invariant catalogue

Browse source 
Expand TestPrimaryRoutesProperty (5 -> 9 ops). New ops mirror the
production shapes the failure cases hit: BatchProbeResults via
UpdateNodes, SimultaneousDisconnect via UpdateNodes, SetApprovedRoutes
that leaves announced RoutableIPs intact, OfflineExpiry that keeps
Unhealthy set. The model now tracks announced and approved separately
and recomputes the intersection.

Strengthen the per-op assertions to cover invariants the model alone
cannot prove: every primary must be online, every primary must
currently advertise its prefix, no flap onto an unhealthy candidate
when a healthy one was available, no flap off a previous primary that
remains a healthy candidate. The check now takes a pre-op snapshot so
the anti-flap rule has a stable reference.

Add TestHAProberProperty in servertest. It drives a real TestServer
with three HA-route-advertising clients through rapid-drawn sequences
of ClientDisconnect / ClientReconnect / ProberTick / WaitForSnapshot
ops and re-checks the same shape invariants after every step.

Document the system in hscontrol/state/HA_INVARIANTS.md: a state
machine over (Healthy+Online, Unhealthy+Online, Offline,
OfflineExpired), fifteen numbered invariants with predicates and
violation paths, and a coverage matrix mapping each invariant to its
unit, servertest, and integration tests. Three rows pin the recent
fixes to the invariants they enforce.
This commit is contained in:
Kristoffer Dalby 2026-05-17 20:32:53 +00:00
parent c7630b505b
commit e2f2f9211f
5 changed files with 968 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

10
hscontrol/state/node_store.go
View file

@ -633,14 +633,14 @@ func snapshotFromNodes(
}
// electPrimaryRoutes picks the primary advertiser for each non-exit
// prefix. Inputs are restricted to online nodes that advertise the
// prefix. The previous primary is preserved when it is still online
// and healthy (anti-flap); otherwise the lowest-NodeID healthy
// advertiser wins. When every advertiser is unhealthy the previous
// primary is preserved if still a candidate, falling back to the
// lowest-NodeID candidate so peers see *some* primary instead of
// none. Anti-flap in the all-unhealthy case matters under cable-pull
// where IsOnline lags reality and a naive lowest-ID fallback churns
// primaries to a node that is itself unreachable (issue #3203).
// primary is preserved only if still a candidate — falling back to
// any other candidate would point peers at a node the prober has
// already declared unreachable, so leaving the prefix unmapped is
// preferred until a probe cycle finds one that responds.
func electPrimaryRoutes(
nodes map[types.NodeID]types.Node,
prev map[netip.Prefix]types.NodeID,

330
hscontrol/state/primaries_property_test.go
View file

@ -2,6 +2,7 @@ package state
import (
"fmt"
"maps"
"net/netip"
"slices"
"testing"
@ -23,6 +24,19 @@ import (
// the same answer from a separate, deliberately direct implementation.
type primariesModel struct {
connected map[types.NodeID]bool
// announced mirrors Hostinfo.RoutableIPs — what the client says
// it can route. The election does not look at this directly; it
// is used to recompute the effective set whenever ApprovedRoutes
// changes without a Hostinfo update.
announced map[types.NodeID][]netip.Prefix
// approved mirrors node.ApprovedRoutes — what the admin policy
// allows. SetApprovedRoutes touches this without touching
// announced; ConnectAdvertise / ApprovedRoutesChange touch both.
approved map[types.NodeID][]netip.Prefix
// prefixes is the effective per-node route set —
// AllApprovedRoutes in the implementation, i.e. (announced ∩
// approved) excluding exit routes. This is what the election
// sees, and what the model uses in advertisersByPrefix.
prefixes map[types.NodeID][]netip.Prefix
unhealthy map[types.NodeID]bool
@ -36,12 +50,42 @@ type primariesModel struct {
func newPrimariesModel() *primariesModel {
return &primariesModel{
connected: map[types.NodeID]bool{},
announced: map[types.NodeID][]netip.Prefix{},
approved: map[types.NodeID][]netip.Prefix{},
prefixes: map[types.NodeID][]netip.Prefix{},
unhealthy: map[types.NodeID]bool{},
primary: map[netip.Prefix]types.NodeID{},
}
}
// recomputeEffective sets m.prefixes[id] to the intersection of
// m.announced[id] and m.approved[id]. Empty intersections clear the
// node from m.prefixes entirely. Matches Node.AllApprovedRoutes /
// SubnetRoutes semantics (exit routes excluded — none of the test
// prefixes hit that branch).
func (m *primariesModel) recomputeEffective(id types.NodeID) {
ann := m.announced[id]
app := m.approved[id]
if len(ann) == 0 || len(app) == 0 {
delete(m.prefixes, id)
return
}
eff := make([]netip.Prefix, 0, len(ann))
for _, p := range ann {
if slices.Contains(app, p) {
eff = append(eff, p)
}
}
if len(eff) == 0 {
delete(m.prefixes, id)
} else {
m.prefixes[id] = eff
}
}
// advertisersByPrefix returns the connected nodes that announce each
// prefix, sorted by NodeID (matches computePrimaries' iteration).
func (m *primariesModel) advertisersByPrefix() map[netip.Prefix][]types.NodeID {
@ -99,10 +143,8 @@ func (m *primariesModel) updatePrimaries() {
// All-unhealthy fallback: preserve the previous primary if it
// is still a candidate, otherwise leave the prefix unmapped.
// electPrimaryRoutes was changed to drop the candidates[0]
// fallback so the Phase-5 (simultaneous dual-disconnect)
// regression cannot pick an already-unhealthy node as
// primary; the model has to track the same behaviour.
// Choosing any candidate would point peers at a node already
// declared unreachable; the model mirrors that policy.
if !found && len(nodes) >= 1 {
if cur, ok := m.primary[p]; ok && slices.Contains(nodes, cur) {
selected = cur
@ -155,8 +197,16 @@ func samePrefixSet(a, b []netip.Prefix) bool {
}
// checkPrimariesProperties asserts every rule we expect of the snapshot's
// primaries map given the model.
func checkPrimariesProperties(rt *rapid.T, ns *NodeStore, m *primariesModel, nodeIDs []types.NodeID) {
// primaries map given the model. prevSnapshotPrimaries is the snapshot's
// PrimaryRoutes() reading taken before the just-applied op, used to
// catch flap regressions that move primary off a still-eligible owner.
func checkPrimariesProperties(
rt *rapid.T,
ns *NodeStore,
m *primariesModel,
nodeIDs []types.NodeID,
prevSnapshotPrimaries map[netip.Prefix]types.NodeID,
) {
rt.Helper()
expectedByNode := map[types.NodeID][]netip.Prefix{}
@ -184,9 +234,9 @@ func checkPrimariesProperties(rt *rapid.T, ns *NodeStore, m *primariesModel, nod
}
// Every prefix that has at least one connected advertiser must
// have a primary in the snapshot. Issue #3203 manifests as a
// prefix silently losing its primary after a disconnect/reconnect
// cycle.
// have a primary in the snapshot: a prefix silently losing its
// primary after a disconnect/reconnect cycle would leave peers
// without a route.
for _, p := range m.allPrefixes() {
want, expectExists := m.primary[p]
if !expectExists {
@ -208,6 +258,105 @@ func checkPrimariesProperties(rt *rapid.T, ns *NodeStore, m *primariesModel, nod
)
}
}
// Structural invariants on the live snapshot, independent of the
// model. These catch shapes the model alone cannot — e.g. an owner
// that is offline but still has the prefix attributed to it.
snapshotPrimaries := ns.PrimaryRoutes()
// A primary that owns ≥1 prefix in `routes` must also light up
// `isPrimaryRoute` (PrimaryRoutesForNode returns nil unless the
// id is in that map). The inverse check — PrimaryRoutesForNode
// returning the right prefixes — is already covered above; this
// catches the reverse direction.
ownersInRoutes := map[types.NodeID]bool{}
for _, owner := range snapshotPrimaries {
ownersInRoutes[owner] = true
}
for owner := range ownersInRoutes {
if got := ns.PrimaryRoutesForNode(owner); len(got) == 0 {
rt.Fatalf(
"node %d owns a prefix in routes but PrimaryRoutesForNode is empty",
owner,
)
}
}
// Per-owner structural checks: every primary must currently be
// online and must currently advertise the prefix it owns.
advertisersByPrefix := m.advertisersByPrefix()
for prefix, owner := range snapshotPrimaries {
nv, ok := ns.GetNode(owner)
if !ok || !nv.Valid() {
rt.Fatalf(
"prefix %s primary %d not present in NodeStore",
prefix, owner,
)
}
// Primary is online: an offline node cannot move packets, so
// election must never leave one as the snapshot's primary.
online, known := nv.IsOnline().GetOk()
if !known || !online {
rt.Fatalf(
"prefix %s primary %d is not online",
prefix, owner,
)
}
// Primary advertises the prefix: AllApprovedRoutes (subnet ∪
// exit) must contain it. A primary that no longer advertises
// is a stale assignment the snapshot rebuild failed to clear.
approved := nv.AllApprovedRoutes()
if !slices.Contains(approved, prefix) {
rt.Fatalf(
"prefix %s primary %d does not advertise it (approved=%v)",
prefix, owner, approved,
)
}
// Healthy preference: if any candidate for this prefix is
// healthy, the elected primary must also be healthy. Leaving
// the prefix unmapped is fine; pointing at an unhealthy
// candidate while a healthy one was available is not.
candidates := advertisersByPrefix[prefix]
anyHealthy := false
for _, c := range candidates {
if !m.unhealthy[c] {
anyHealthy = true
break
}
}
if anyHealthy && m.unhealthy[owner] {
rt.Fatalf(
"prefix %s primary %d is unhealthy but %v had a healthy candidate",
prefix, owner, candidates,
)
}
// Anti-flap: if the previous snapshot already had a primary
// for this prefix AND that primary is still a healthy
// candidate after the op, the election must keep it. Flapping
// the primary for an unrelated reason violates the contract
// the integration tests rely on (HA failover only moves on
// loss of candidacy or health).
if prev, hadPrev := prevSnapshotPrimaries[prefix]; hadPrev {
stillCandidate := slices.Contains(candidates, prev)
stillHealthy := !m.unhealthy[prev]
if stillCandidate && stillHealthy && owner != prev {
rt.Fatalf(
"prefix %s flapped primary %d -> %d "+
"while previous primary was still a healthy candidate",
prefix, prev, owner,
)
}
}
}
}
// nodeForRapid builds a minimal types.Node for use in property
@ -229,16 +378,41 @@ func nodeForRapid(id types.NodeID) types.Node {
}
}
// snapshotPrimariesCopy returns a defensive copy of the snapshot's
// prefix→primary map so the caller can compare against a later
// snapshot without aliasing the live map.
func snapshotPrimariesCopy(ns *NodeStore) map[netip.Prefix]types.NodeID {
live := ns.PrimaryRoutes()
out := make(map[netip.Prefix]types.NodeID, len(live))
maps.Copy(out, live)
return out
}
// TestPrimaryRoutesProperty drives NodeStore with a randomised
// sequence of high-level operations and checks that the snapshot's
// primaries map matches a reference model after every step.
//
// Background: issue #3203 reports that HA tracking enters a stuck
// state after a sequence of disconnect/reconnect events. The narrow
// integration and servertest reproductions written for the bug do
// not fail on upstream/main, so this property test broadens the
// search by letting rapid generate sequences we have not enumerated
// by hand.
// Op set (covers the dual-disconnect, batched-probe, and
// all-unhealthy-fallback shapes that election has to handle):
//
// - ConnectAdvertise: online + advertise prefs, clear Unhealthy
// - Disconnect: offline; ApprovedRoutes persists
// - ProbeUnhealthy: set Unhealthy
// - ProbeHealthy: clear Unhealthy
// - ApprovedRoutesChange: change advertised prefs without touching health
// - BatchProbeResults: apply a batch of health flips through
// UpdateNodes so the election runs once for the cycle, matching
// State.BatchSetNodeHealth
// - SimultaneousDisconnect: mark multiple nodes offline atomically
// via UpdateNodes (the dual-cable-pull shape)
// - SetApprovedRoutes: change ApprovedRoutes while leaving
// Hostinfo.RoutableIPs alone — exercises the asymmetry between
// announced and approved
// - OfflineExpiry: IsOnline=false WITHOUT clearing Unhealthy
// (matches the Disconnect path's actual semantics versus
// ConnectAdvertise's full reset)
func TestPrimaryRoutesProperty(t *testing.T) {
rapid.Check(t, func(rt *rapid.T) {
const numNodes = 4
@ -270,14 +444,29 @@ func TestPrimaryRoutesProperty(t *testing.T) {
0, len(prefixes),
func(p netip.Prefix) string { return p.String() },
)
// nodeSubsetGen draws 1..N distinct node IDs for the batched
// ops. SliceOfNDistinct's lower bound is inclusive, so 1 is
// the smallest sensible batch — a zero-size batch is a no-op
// the rapid harness should not waste shrinking cycles on.
nodeSubsetGen := rapid.SliceOfNDistinct(
nodeGen,
1, numNodes,
func(id types.NodeID) types.NodeID { return id },
)
opCount := rapid.IntRange(5, 60).Draw(rt, "opCount")
opCount := rapid.IntRange(5, 200).Draw(rt, "opCount")
for step := range opCount {
op := rapid.IntRange(0, 4).Draw(rt, fmt.Sprintf("op_%d", step))
id := nodeGen.Draw(rt, fmt.Sprintf("id_%d", step))
op := rapid.IntRange(0, 8).Draw(rt, fmt.Sprintf("op_%d", step))
// Snapshot primaries before applying the op so the
// anti-flap invariant has a stable reference. Reading
// after the model has already changed would compare a
// stale snapshot to a moved model.
prevPrimaries := snapshotPrimariesCopy(ns)
switch op {
case 0: // ConnectAdvertise — Connect path clears Unhealthy.
id := nodeGen.Draw(rt, fmt.Sprintf("id_%d", step))
prefs := prefixSubsetGen.Draw(rt, fmt.Sprintf("prefs_%d", step))
ns.UpdateNode(id, func(n *types.Node) {
@ -287,35 +476,41 @@ func TestPrimaryRoutesProperty(t *testing.T) {
n.ApprovedRoutes = prefs
})
m.announced[id] = prefs
m.approved[id] = prefs
m.recomputeEffective(id)
if len(prefs) == 0 {
delete(m.connected, id)
delete(m.prefixes, id)
} else {
m.connected[id] = true
m.prefixes[id] = prefs
}
delete(m.unhealthy, id)
case 1: // Disconnect — IsOnline=false; ApprovedRoutes persists.
id := nodeGen.Draw(rt, fmt.Sprintf("id_%d", step))
ns.UpdateNode(id, func(n *types.Node) {
n.IsOnline = new(false)
})
delete(m.connected, id)
case 2: // ProbeUnhealthy — HA prober marks node bad.
id := nodeGen.Draw(rt, fmt.Sprintf("id_%d", step))
ns.UpdateNode(id, func(n *types.Node) {
n.Unhealthy = true
})
m.unhealthy[id] = true
case 3: // ProbeHealthy — HA prober marks node good.
id := nodeGen.Draw(rt, fmt.Sprintf("id_%d", step))
ns.UpdateNode(id, func(n *types.Node) {
n.Unhealthy = false
})
delete(m.unhealthy, id)
case 4: // ApprovedRoutesChange — change advertised prefs without touching health.
id := nodeGen.Draw(rt, fmt.Sprintf("id_%d", step))
prefs := prefixSubsetGen.Draw(rt, fmt.Sprintf("prefs_%d", step))
ns.UpdateNode(id, func(n *types.Node) {
@ -324,18 +519,107 @@ func TestPrimaryRoutesProperty(t *testing.T) {
n.ApprovedRoutes = prefs
})
m.announced[id] = prefs
m.approved[id] = prefs
m.recomputeEffective(id)
if len(prefs) == 0 {
delete(m.connected, id)
delete(m.prefixes, id)
} else {
m.connected[id] = true
m.prefixes[id] = prefs
}
case 5: // BatchProbeResults — atomic health flips per cycle.
// Mirrors State.BatchSetNodeHealth: per-node
// (id, unhealthy) pairs applied through UpdateNodes
// so the election runs once on the post-batch state.
// Per-call publication would let an intermediate
// "one unhealthy, one healthy" snapshot re-elect off
// the still-healthy node before the second flip
// landed.
ids := nodeSubsetGen.Draw(rt, fmt.Sprintf("batch_ids_%d", step))
results := make(map[types.NodeID]bool, len(ids))
for i, id := range ids {
unhealthy := rapid.Bool().Draw(rt, fmt.Sprintf("batch_h_%d_%d", step, i))
results[id] = unhealthy
}
fns := make(map[types.NodeID]UpdateNodeFunc, len(results))
for id, unhealthy := range results {
fns[id] = func(n *types.Node) {
n.Unhealthy = unhealthy
}
}
ns.UpdateNodes(fns)
for id, unhealthy := range results {
if unhealthy {
m.unhealthy[id] = true
} else {
delete(m.unhealthy, id)
}
}
case 6: // SimultaneousDisconnect — multiple offline in one batch.
// Dual-cable-pull shape: two HA routers' poll
// sessions both close in the same NodeStore tick.
// Per-call Disconnect could leave the snapshot
// momentarily pointing at an offline owner; the
// batched form forces a single rebuild.
ids := nodeSubsetGen.Draw(rt, fmt.Sprintf("disc_ids_%d", step))
fns := make(map[types.NodeID]UpdateNodeFunc, len(ids))
for _, id := range ids {
fns[id] = func(n *types.Node) {
n.IsOnline = new(false)
}
}
ns.UpdateNodes(fns)
for _, id := range ids {
delete(m.connected, id)
}
case 7: // SetApprovedRoutes — change ApprovedRoutes only.
// SetApprovedRoutes in production updates only
// node.ApprovedRoutes; Hostinfo.RoutableIPs (what
// the client announced) is set by the next
// MapRequest. SubnetRoutes intersects the two, so
// dropping ApprovedRoutes mid-flight shrinks the
// advertised set immediately while announcement
// alone never extends it.
id := nodeGen.Draw(rt, fmt.Sprintf("setapp_id_%d", step))
prefs := prefixSubsetGen.Draw(rt, fmt.Sprintf("setapp_prefs_%d", step))
ns.UpdateNode(id, func(n *types.Node) {
n.ApprovedRoutes = prefs
})
m.approved[id] = prefs
m.recomputeEffective(id)
case 8: // OfflineExpiry — IsOnline=false, KEEP Unhealthy.
// The Disconnect path does not clear Unhealthy
// (only ConnectAdvertise does on the way back
// up). A probe that marks unhealthy and a grace-
// period disconnect that lands later leaves the
// node with a stale Unhealthy bit; the test
// exercises that shape.
id := nodeGen.Draw(rt, fmt.Sprintf("expire_id_%d", step))
ns.UpdateNode(id, func(n *types.Node) {
n.IsOnline = new(false)
})
delete(m.connected, id)
// m.unhealthy[id] is intentionally NOT cleared.
}
m.updatePrimaries()
checkPrimariesProperties(rt, ns, m, nodeIDs)
checkPrimariesProperties(rt, ns, m, nodeIDs, prevPrimaries)
}
})
}

23
hscontrol/state/primaries_test.go
View file

@ -218,12 +218,12 @@ func TestPrimaries_AllUnhealthyKeepsAPrimary(t *testing.T) {
}
func TestPrimaries_AllUnhealthyPreservesPrevious(t *testing.T) {
// Issue #3203: once a failover has moved primary to a higher-ID
// node, a subsequent all-unhealthy state must NOT churn primary
// back to the lowest-ID candidate. Under cable-pull semantics
// both nodes can linger as IsOnline=true (half-open TCP) and
// both go Unhealthy — naive `candidates[0]` would flap the
// primary to a node that is itself unreachable.
// Once a failover has moved primary to a higher-ID node, a
// subsequent all-unhealthy state must NOT churn primary back to
// the lowest-ID candidate. Under cable-pull semantics both nodes
// can linger as IsOnline=true (half-open TCP) and both go
// Unhealthy — naive `candidates[0]` would flap the primary to a
// node that is itself unreachable.
prefix := mp("10.0.0.0/24")
f := newPrimariesFixture(t, 1, 2)
f.advertise(1, prefix)
@ -247,12 +247,11 @@ func TestPrimaries_ExitRouteNotElected(t *testing.T) {
f.requireNoPrimary(exitV4)
}
func TestPrimaries_RegressionIssue3203_BothOfflineThenOneReturns(t *testing.T) {
// Issue #3203: with two HA advertisers, dropping both then
// bringing one back used to leave the prefix without any
// primary. After the refactor the snapshot recomputes primaries
// on every NodeStore write, so the returning advertiser must
// be elected.
func TestPrimaries_BothOfflineThenOneReturns(t *testing.T) {
// With two HA advertisers, dropping both then bringing one back
// used to leave the prefix without any primary. The snapshot
// recomputes primaries on every NodeStore write, so the
// returning advertiser must be elected.
prefix := mp("10.0.0.0/24")
f := newPrimariesFixture(t, 1, 2)
f.advertise(1, prefix)