relay

executable models of message-delivery guarantees

relay is a small Haskell library of message-delivery guarantees. Each guarantee is a little algebra of two complementary halves — a send half and a receive half, with no shared runtime object — kept close to its laws, and then run end-to-end through a real concurrent test harness.

Guarantees

• Ordered delivery — in-order release over a link that reorders but never loses. The sender stamps sequence numbers; the receiver buffers out-of-order arrivals and releases in order. → article/ordered-delivery.md
• Reliable delivery — exactly-once, in-order release over a link that drops frames, via cumulative acks and retransmission. The closed loop the ordered model leaves open. → article/reliable-delivery.md

Modules

Relay.Session          frames, sessions, sequence numbers (shared)
Relay.SenderHalf       ordered: sequence assignment
Relay.ReceiverHalf     ordered: in-order release + reorder buffer
Relay.Buffer           ordered: multi-session receiver

Relay.Reliable.Outbox    reliable: send half (in-flight buffer, cumulative ack)
Relay.Reliable.Inbox     reliable: receive half (frontier + ack)
Relay.Reliable.Response  reliable: the reverse-channel ack type

The reliable layer reuses the ordered vocabulary unchanged — the same Frame, and ReceiverHalf as the delivery frontier.

Approach

Each guarantee is modelled twice over:

• Pure laws — the local invariants of each half, as QuickCheck properties (sequence assignment, cumulative ack, dedup, the frontier invariant, …).
• Concurrent check — the end-to-end guarantee that no half can observe locally, run through live sender/receiver threads over a channel that reorders (ordered) or drops (reliable).

Building

cabal build all
cabal test                                   # the whole suite
cabal test --test-options="--timeout 30s"    # guard the concurrent tests

Articles

• Ordered Delivery — the base model.
• Reliable Delivery — acks, retransmit, and correspondence to Monarch's hyperactor channel/net subsystem.
• Concurrent Haskell, just enough to read relay's tests — a primer on Chan, TVar, and TQueue grounded in both harnesses.