recon_protocols/

stubborn_link.rs

//! Stubborn point-to-point links.
//!
//! Cachin, Guerraoui & Rodrigues, Module 2.2 and Algorithm 2.1 ("Retransmit Forever").
//!
//! **Status: academic. Space: unbounded — and unboundable.** This is how a perfect link is built
//! when the only thing underneath is a lossy datagram service — the simulator's situation, and not
//! a deployment's, where TCP and QUIC retransmit already. It stays because everything above needs a
//! perfect link and the simulator offers only fair-loss.
//!
//! `sent` grows with every transmission, and that is not a defect to be fixed: **it is `SL1`.** The
//! property below is that a message sent once is delivered *an infinite number of times*, so a link
//! that let go would not be a bounded stubborn link — it would not be a stubborn link. There is no
//! bounded form of this abstraction, and the answer to wanting one is [`crate::session_link`], not
//! a smaller `sent`. See `docs/bounded-space.md`.
//!
//! What is true is that nothing retires an entry unless the layer above stops it, and nothing in
//! this repository does — the perfect link never does, because Algorithm 2.2 never does. Every
//! entry is therefore re-sent on every tick, and the cost grows with everything ever sent.
//!
//! Turns a fair-loss network into one where a message sent between correct processes is
//! eventually delivered, by retransmitting it at a fixed interval. The cost is unbounded
//! duplication: the recipient delivers the message infinitely often. Suppressing that is the
//! perfect link's job, not this one's.
//!
//! ```text
//! upon event ⟨ sl, Init ⟩ do
//!     sent := ∅;
//!     starttimer(Δ);
//!
//! upon event ⟨ sl, Send | q, m ⟩ do
//!     trigger ⟨ fll, Send | q, m ⟩;
//!     sent := sent ∪ {(q, m)};
//!
//! upon event ⟨ Timeout ⟩ do
//!     forall (q, m) ∈ sent do trigger ⟨ fll, Send | q, m ⟩;
//!     starttimer(Δ);
//!
//! upon event ⟨ fll, Deliver | p, m ⟩ do
//!     trigger ⟨ sl, Deliver | p, m ⟩;
//! ```
//!
//! # Departures from the page
//!
//! - The book's `⟨ Init ⟩` starts the timer unconditionally and runs it for ever. This arms it
//!   lazily instead, when there is something to retransmit; see `arm`. Behaviourally equivalent,
//!   and it lets a run reach quiescence rather than tick indefinitely.
//! - Each transmission is named by a [`SendId`] so the layer above can retire it with
//!   [`Cmd::Stop`]. The book has no such request and never lets go. See [`Cmd::Send`] for the
//!   precondition that naming brings with it.
//!
//!   Conservative, and worth saying why: `SL1` is conditioned on a sender that sends `m` *once*,
//!   and says nothing about one that retracts. So with no caller the behaviour is exactly the
//!   book's, and a layer that genuinely knows a transmission is finished may stop it without
//!   costing a property. Nothing in this repository calls it yet; only this module's own suite does.

use core::time::Duration;
use recon_core::{NodeId, ProtoCx, Protocol, TimerId};
use std::collections::BTreeMap;

/// Identifies one stubborn transmission, so it can later be stopped.
///
/// The book retransmits forever and never stops, which is `SL1` rather than an oversight. A caller
/// that knows a transmission is finished may nonetheless let go of it, so each one is named. That
/// is a retraction, which the property does not speak about — not a bound on the property.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct SendId(pub u64);

/// Requests from the layer above.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Cmd<M> {
    /// Transmit `msg` to `to`, and keep transmitting it until stopped.
    ///
    /// **`id` must not name a transmission that is still live.** Reusing one replaces the earlier
    /// transmission outright: it stops being retransmitted, and SL1 lapses for it silently —
    /// there is no indication, and nothing above is told a promise was withdrawn. The identifier
    /// is the caller's to allocate, so the uniqueness is the caller's to hold; `debug_assert`
    /// checks it in debug builds.
    Send { id: SendId, to: NodeId, msg: M },
    /// Stop retransmitting the transmission named `id`.
    Stop { id: SendId },
}

/// Indications to the layer above.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Ind<M> {
    /// A message arrived. May be raised many times for one transmission.
    Deliver { from: NodeId, msg: M },
}

/// Retransmits until told to stop.
///
/// Adds nothing to the wire: what it transmits is exactly the payload it was given. That is why
/// a three-layer stack built on it carries only one header.
#[derive(Debug)]
pub struct StubbornLink<M> {
    interval: Duration,
    sent: BTreeMap<SendId, (NodeId, M)>,
    /// The retransmission timer outstanding, if any. A handle rather than a flag: an expiry this
    /// link is no longer waiting on is then recognisable, where `true` said only that something
    /// was pending.
    tick: Option<TimerId>,
}

impl<M> StubbornLink<M> {
    /// Retransmit everything outstanding every `interval`.
    pub fn new(interval: Duration) -> Self {
        StubbornLink { interval, sent: BTreeMap::new(), tick: None }
    }

    /// How many transmissions are still being retried.
    pub fn outstanding(&self) -> usize {
        self.sent.len()
    }

    /// The retransmission interval.
    pub fn interval(&self) -> Duration {
        self.interval
    }
}

impl<M: Clone> StubbornLink<M> {
    /// Arm the retransmission timer if there is anything to retransmit.
    ///
    /// The book starts a timer at initialisation and runs it forever. Arming lazily is
    /// equivalent in behaviour and leaves no timer running when nothing is outstanding — which
    /// also means a run reaches quiescence instead of ticking indefinitely.
    fn arm(&mut self, cx: &mut ProtoCx<'_, Self>) {
        if self.tick.is_none() && !self.sent.is_empty() {
            self.tick = Some(cx.set_timer(self.interval));
        }
    }
}

impl<M: Clone> Protocol for StubbornLink<M> {
    type Cmd = Cmd<M>;
    type Ind = Ind<M>;
    type Msg = M;
    /// No scope conditions: this protocol's guarantees do not lapse.
    type Scope = core::convert::Infallible;
    type Note = crate::Note;
    /// Keeps nothing durably: a crash loses everything this protocol knows.
    type Meta = core::convert::Infallible;
    type Entry = core::convert::Infallible;

    fn on_cmd(&mut self, cmd: Cmd<M>, cx: &mut ProtoCx<'_, Self>) {
        match cmd {
            Cmd::Send { id, to, msg } => {
                // Reuse would retire the earlier transmission with no indication that its SL1 had
                // lapsed. See the precondition on `Cmd::Send`.
                debug_assert!(!self.sent.contains_key(&id), "SendId {id:?} is still live");
                cx.send(to, msg.clone());
                self.sent.insert(id, (to, msg));
                self.arm(cx);
            }
            Cmd::Stop { id } => {
                self.sent.remove(&id);
            }
        }
    }

    fn on_msg(&mut self, from: NodeId, msg: M, cx: &mut ProtoCx<'_, Self>) {
        // No creation: what is delivered upward is exactly what arrived, attributed to whoever
        // the network says sent it.
        cx.indicate(Ind::Deliver { from, msg });
    }

    fn on_timer(&mut self, id: TimerId, cx: &mut ProtoCx<'_, Self>) {
        // Every layer above hands every expiry down, so most of what arrives here was registered
        // by somebody else. Only the one this link is waiting on does anything — which also makes
        // an expiry this link has superseded recognisable rather than merely indistinguishable.
        if self.tick != Some(id) {
            return;
        }
        for (to, msg) in self.sent.values() {
            cx.send(*to, msg.clone());
        }
        self.tick = None;
        self.arm(cx);
    }
}