PosseBeacons

--------------------------- MODULE PosseBeacons --------------------------- (***************************************************************************) (* Crew position beacons over a lossy, flooded, multi-hop mesh. *) (* *) (* N nodes each periodically broadcast a *beacon* carrying (id, ts, pos). *) (* `ts` is a per-node strictly increasing timestamp, so the position is *) (* "where this node was at time ts" and `ts` alone stands in for the whole *) (* payload: two beacons from the same node are ordered exactly by ts. *) (* *) (* Propagation is a bounded flood: *) (* - the originator broadcasts with hops = 0; *) (* - a node that processes a packet it has NOT seen before, and whose *) (* hop count is < MaxHops, rebroadcasts it once with hops + 1; *) (* - packet identity is (src, ts) -- the hop path is deliberately not *) (* part of it, so the seen-table suppresses every later copy of the *) (* same beacon no matter which way it came; *) (* - the originator marks its own packet seen at send time, so a copy *) (* flooding back to it is never re-relayed; *) (* - a node ignores beacons whose id is its own (self loop-back). *) (* *) (* Receiver rule (the interesting part): node n keeps one record per peer *) (* p, view[n][p], and overwrites it only when the incoming ts is strictly *) (* newer than the stored one. Without that guard a delayed relayed copy *) (* of an *old* beacon overwrites a peer's fresh position -- that is the *) (* negative result in PosseBeaconsNoGuard.tla. *) (* *) (* The medium is `air`: a monotonically growing set of transmitted *) (* packets. A packet in `air` may be delivered to any node at any later *) (* time, any number of times, or never. That one abstraction covers loss, *) (* arbitrary delay, reordering and duplication at once, and it makes the *) (* randomised relay backoff unobservable, so a relay may be folded into *) (* the receive step without weakening any safety property. *) (* *) (* Abstracted away, because no invariant here depends on it: the hop count *) (* the receiver records alongside the position (display only), the *) (* channel encryption, and the 32-bit wrap in the real ts comparison. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Nodes, \* set of crew nodes Senders, \* the subset of Nodes that originate beacons in this model MaxHops, \* relay budget (a packet at hops >= MaxHops is not forwarded) MaxBeacons \* beacons each node may originate (this is what bounds the model) \* Senders exists purely to buy depth. Every node beaconing three times does \* not fit in memory; dropping one originator lets the same module run with a \* longer timestamp sequence, which is where deep reordering lives. Relaying \* is always done by every node, whether or not it originates. ASSUME /\ Senders \subseteq Nodes /\ MaxHops \in Nat /\ MaxBeacons \in Nat \ {0} TimeStamps == 1..MaxBeacons \* a node's per-beacon unique, increasing ts NoTs == 0 \* "nothing heard from this peer yet" PacketIds == [src: Nodes, ts: TimeStamps] \* the seen-table key Packets == [src: Nodes, ts: TimeStamps, hops: 0..MaxHops] VARIABLES clock, \* clock[n]: beacons n has originated; its next ts is clock[n]+1 air, \* set of Packets ever transmitted and still deliverable seen, \* seen[n]: PacketIds n has already processed (the seen-table) relayed, \* relayed[n]: PacketIds n has rebroadcast view, \* view[n][p]: ts of the freshest beacon of p that n has accepted \* ---- history variables, used only by the invariants ---- maxRecv, \* maxRecv[n][p]: greatest ts of p ever *delivered* to n doubleRelay \* TRUE once some node rebroadcast one packet twice vars == <<clock, air, seen, relayed, view, maxRecv, doubleRelay>> Id(m) == [src |-> m.src, ts |-> m.ts] Max(a, b) == IF a > b THEN a ELSE b TypeOK == /\ clock \in [Nodes -> 0..MaxBeacons] /\ air \in SUBSET Packets /\ seen \in [Nodes -> SUBSET PacketIds] /\ relayed \in [Nodes -> SUBSET PacketIds] /\ view \in [Nodes -> [Nodes -> {NoTs} \cup TimeStamps]] /\ maxRecv \in [Nodes -> [Nodes -> {NoTs} \cup TimeStamps]] /\ doubleRelay \in BOOLEAN Init == /\ clock = [n \in Nodes |-> 0] /\ air = {} /\ seen = [n \in Nodes |-> {}] /\ relayed = [n \in Nodes |-> {}] /\ view = [n \in Nodes |-> [p \in Nodes |-> NoTs]] /\ maxRecv = [n \in Nodes |-> [p \in Nodes |-> NoTs]] /\ doubleRelay = FALSE (***************************************************************************) (* Originate a beacon at hops 0. Sending a flood packet also marks it in *) (* the sender's own seen-table, which is what stops the originator from *) (* relaying a copy of its own beacon that floods back to it. *) (***************************************************************************) SendBeacon(p) == /\ p \in Senders /\ clock[p] < MaxBeacons /\ LET t == clock[p] + 1 IN /\ clock' = [clock EXCEPT ![p] = t] /\ air' = air \cup {[src |-> p, ts |-> t, hops |-> 0]} /\ seen' = [seen EXCEPT ![p] = @ \cup {[src |-> p, ts |-> t]}] /\ UNCHANGED <<relayed, view, maxRecv, doubleRelay>> (***************************************************************************) (* Deliver one airborne copy to node n. This mirrors the receive path for *) (* a group-data packet: the seen-table gates BOTH the application callback *) (* and the forwarding decision, so a duplicate is dropped outright and is *) (* never rebroadcast a second time. *) (***************************************************************************) Receive(n, m) == /\ m \in air /\ maxRecv' = IF m.src = n \* own beacon looped back THEN maxRecv ELSE [maxRecv EXCEPT ![n][m.src] = Max(@, m.ts)] /\ IF Id(m) \in seen[n] THEN \* duplicate: not delivered to the application, not forwarded UNCHANGED <<air, seen, relayed, view, doubleRelay>> ELSE /\ seen' = [seen EXCEPT ![n] = @ \cup {Id(m)}] \* --- application layer ------------------------------------------- \* Accept the position only if this beacon is strictly newer than \* the one already held for that peer; ignore our own id entirely. /\ view' = IF m.src # n /\ m.ts > view[n][m.src] THEN [view EXCEPT ![n][m.src] = m.ts] ELSE view \* --- mesh layer: forward once, inside the hop budget -------------- /\ IF m.hops < MaxHops THEN /\ air' = air \cup {[src |-> m.src, ts |-> m.ts, hops |-> m.hops + 1]} /\ relayed' = [relayed EXCEPT ![n] = @ \cup {Id(m)}] /\ doubleRelay' = doubleRelay \/ (Id(m) \in relayed[n]) ELSE UNCHANGED <<air, relayed, doubleRelay>> /\ UNCHANGED clock Next == \/ \E p \in Nodes : SendBeacon(p) \/ \E n \in Nodes, m \in air : Receive(n, m) \* Terminal states exist (every beacon sent, every airborne copy delivered \* everywhere), so the model is checked with CHECK_DEADLOCK FALSE. (***************************************************************************) (* PROPERTIES CHECKED *) (***************************************************************************) \* 1. Monotonic: a node's timestamp for a peer never goes backwards. This is \* a two-state property, so it is checked as an action property rather \* than an invariant. MonotonicStep == \A n, p \in Nodes : view'[n][p] >= view[n][p] Monotonic == [][MonotonicStep]_vars \* 2. Sound: no fabricated positions. Anything stored for a peer is a ts \* that peer really originated, and that this node really received; the \* node never invents a position for itself either. Sound == \A n, p \in Nodes : /\ view[n][p] <= clock[p] \* p really sent this ts /\ view[n][p] <= maxRecv[n][p] \* n really received it /\ (n = p) => view[n][p] = NoTs \* 3. Freshest-wins: for every beacon a node has ever been handed, its view \* of that peer is at least that fresh. Together with Sound this pins \* view[n][p] to exactly the newest beacon of p that ever reached n. \* This is the property flood reordering threatens. Freshest == \A n, p \in Nodes : (n # p) => view[n][p] >= maxRecv[n][p] \* 4. Bounded relay: nothing is airborne beyond the hop budget, a node only \* rebroadcasts packets it actually processed, and no node ever \* rebroadcasts the same packet twice (the seen-table is load-bearing). BoundedRelay == /\ \A m \in air : m.hops <= MaxHops /\ \A n \in Nodes : relayed[n] \subseteq seen[n] /\ ~doubleRelay =============================================================================

\* 3 crew nodes, a 2-hop relay budget, 2 beacons each. Small enough to \* enumerate, large enough for a twice-relayed copy of beacon 1 to land at a \* node that already accepted beacon 2 -- the reordering the guard exists for. CONSTANTS Nodes = {n1, n2, n3} Senders = {n1, n2, n3} MaxHops = 2 MaxBeacons = 2 INIT Init NEXT Next INVARIANTS TypeOK Sound Freshest BoundedRelay PROPERTIES Monotonic CHECK_DEADLOCK FALSE