Cairn.Runtime.InFlight
lean/Cairn/Runtime/InFlight.lean
Requests in flight (docs/effects.md, "Requests in flight"): what the runtime guarantees about the cap, the queue and cancelled requests.
- The cap is never exceeded: the capped requests with the host (sent and not answered, or
cancelled and not yet answered) never number more than
App.maxInFlight, and the cap never changes (step_cap,steps_cap). - Nothing waits that could go: after every event, every queued request is held either by
the cap or by its id's cancelled request still being with the host (
step_settled,queued_blocked). - Every queued request is eventually sent or cancelled: a queued request always has a
blocker, a request with the host, and the host's reply to a blocker either takes the request
out of the queue or shrinks a count of what is ahead of it (
step_drains). Nothing else ever grows that count (step_wait_le), so after finitely many replies the request has left the queue: sent (promote) or cancelled (World.cancel). - A cancelled id never delivers: the host's reply to a request cancelled after it was sent
reaches no app, and frees its slot (
step_reply_cancelled); on the book's side, no reply to a cancelled id is admitted until it is requested again (Book.cancel_blocks, read withsteps_book).
The statements are about a world that is Fine (step_fine, from start_fine).
Imports Cairn.Runtime.WorldProofs
Structures 3
Through (I : World → Prop) (R : World → World → Prop) : Prop
I is kept and R holds across absorbing an effect and updates that leave the tables
alone.
trans : R a c
reqs : I w' ∧ R w w'
absorb1 : I (w.absorb1 e).fst ∧ R w (w.absorb1 e).fst
Carries (I : World → Prop) (R : World → World → Prop) : Prop
…and across taking a reply, or a cancelled request's reply, then sending from the queue.
toThrough : Through I R
reply : I w'.promote.fst ∧ R w w'.promote.fst
stop : I w'.promote.fst ∧ R w w'.promote.fst
Fine (w : World) : Prop
The request tables are well formed: no id is pending or queued twice (Keys), no pending
id is also stopping, the cap holds and is at least one, and the queue is in ticket order with
every ticket issued.
keys : w.Keys
apart : w.isStopping p.fst = falsecap : w.inFlight ≤ w.cap
pos : 0 < w.cap
sorted : List.Pairwise (fun a b => a.fst < b.fst) w.queued
fresh : q.fst < w.nextTicket
Definitions 11
Reqs (w w' : World) : Prop
The request tables, the cap and the next ticket are the same.
Settled (w : World) : Prop
Nothing waits that could go: no queued request could be sent now.
bookOf (w : World) : Book
The canonical book of a world: its timers and its live requests.
stopOne (w : World) (id : Nat) (k : Request.Kind) : World
id's pending request, of kind k, moved to stopping.
capAhead (w : World) (t : Nat) : Nat
stopAhead (w : World) (t : Nat) : Nat
ahead (w : World) (t : Nat) : Nat
What holds up the queued requests with tickets up to t.
Drains (t : Nat) (w w' : World) : Prop
From w to w', nothing ahead grew and no queued request up to t appeared, or saw its id
start stopping.
capIn (t : Nat) (l : List (Nat × Nat × Request)) : Nat
The capped requests with tickets up to t in a list.
Blocks (w : World) (q : Nat × Nat × Request) (x : Nat) : Prop
What q waits for, by id: the host's reply to its id's cancelled request, or (for a capped
request whose id is free) the reply to any capped request with the host.
Track (x : Nat) (k : Request.Kind) (w w' : World) : Prop
How a request with the host fares: still pending with its kind, or moved to stopping.
Theorems 79
refl (w : World) : w.Reqs w
refl {I : World → Prop} {R : World → World → Prop} (K : Through I R)
{w : World} (h : I w) : I w ∧ R w w
next {I : World → Prop} {R : World → World → Prop} (K : Through I R)
{a b c : World} (h1 : I b ∧ R a b) (h2 : I b → I c ∧ R b c) : I c ∧ R a c
absorb {I : World → Prop} {R : World → World → Prop} (K : Through I R)
(es : List Effect) (w : World) : I w → I (w.absorb es).fst ∧ R w (w.absorb es).fst
give {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Through I R) (app : App S) (c : Ctx S) (m : Msg) (h : I c.world) :
I (Runtime.give app c m).world ∧ R c.world (Runtime.give app c m).world
hear {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Through I R) (app : App S) (c : Ctx S) (h : I c.world) :
I (Runtime.hear app c).world ∧ R c.world (Runtime.hear app c).world
fire {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Through I R) (app : App S) (c : Ctx S) (n : String) (h : I c.world) :
I (Runtime.fire app c n).world ∧ R c.world (Runtime.fire app c n).world
foldl_fire {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Through I R) (app : App S) (ns : List String) (c : Ctx S) :
I c.world →
I (List.foldl (Runtime.fire app) c ns).world ∧
R c.world (List.foldl (Runtime.fire app) c ns).world
boot {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Through I R) (app : App S) (c : Ctx S) (h : I c.world) :
I (Runtime.boot app c).world ∧ R c.world (Runtime.boot app c).world
act {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Through I R) (app : App S) (c : Ctx S) (acts : List Action) (h : I c.world) :
I (Runtime.act app c acts).world ∧ R c.world (Runtime.act app c acts).world
ack {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Carries I R) (c : Ctx S) (id : Nat) (h : I c.world) :
I (Runtime.ack c id).world ∧ R c.world (Runtime.ack c id).world
admit {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Carries I R) (app : App S) (s : State S) (e : Event) (h : I s.world) :
I (Runtime.admit app s e).world ∧ R s.world (Runtime.admit app s e).world
step {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Carries I R) (app : App S) (cfg : Config) (s : State S) (e : Event) (h : I s.world) :
I (Runtime.step app cfg s e).fst.world ∧ R s.world (Runtime.step app cfg s e).fst.worldA kept property is kept by a step.
steps {S : Type} {I : World → Prop} {R : World → World → Prop}
(K : Carries I R) (app : App S) (cfg : Config) (s : State S) (es : List Event)
(h : I s.world) :
I (Runtime.steps app cfg s es).fst.world ∧
R s.world (Runtime.steps app cfg s es).fst.world…and by a batch of steps.
countP_filter_le {α : Type} (p q : α → Bool) (l : List α) :
List.countP p (List.filter q l) ≤ List.countP p l
countP_filter_ne {β : Type} (p : Nat × β → Bool) {x : Nat} {v : β}
(l : List (Nat × β)) :
(x, v) ∈ l →
(List.countP p (List.filter (fun x_1 => x_1.fst != x) l) +
if p (x, v) = true then 1 else 0) ≤
List.countP p l
send_inFlight (w : World) (id : Nat) (k : Request.Kind) : (w.send id k).inFlight = w.inFlight + if k.capped = true then 1 else 0
canSend_capped {w : World} {id : Nat} {k : Request.Kind}
(h : w.canSend id k = true) (hk : k.capped = true) : w.inFlight < w.cap
canSend_stop {w : World} {id : Nat} {k : Request.Kind}
(h : w.canSend id k = true) : w.isStopping id = false
send_cap {w : World} {id : Nat} {k : Request.Kind}
(hc : w.inFlight ≤ w.cap) (h : w.canSend id k = true) :
(w.send id k).inFlight ≤ (w.send id k).capSending under canSend keeps the cap.
cancel_inFlight (w : World) (id : Nat) : (w.cancel id).fst.inFlight ≤ w.inFlight
absorb1_cap (w : World) (e : Effect) (h : w.inFlight ≤ w.cap) : (w.absorb1 e).fst.inFlight ≤ (w.absorb1 e).fst.cap
promoteGo_cap (rest : List (Nat × Nat × Request)) (w : World) : w.inFlight ≤ w.cap → (w.promoteGo rest).fst.inFlight ≤ (w.promoteGo rest).fst.cap
promote_cap (w : World) (h : w.inFlight ≤ w.cap) : w.promote.fst.inFlight ≤ w.promote.fst.cap
takeReply_inFlight {w w' : World} {id : Nat} {r : Reply}
(h : w.takeReply id r = some w') : w'.inFlight ≤ w.inFlight ∧ w'.cap = w.cap
takeStop_inFlight {w w' : World} {id : Nat}
(h : w.takeStop id = some w') : w'.inFlight ≤ w.inFlight ∧ w'.cap = w.cap
carries_cap : Carries (fun w => w.inFlight ≤ w.cap) fun w w' => w'.cap = w.cap
The cap holds, and the cap itself never changes.
step_cap {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event)
(h : s.world.inFlight ≤ s.world.cap) :
(step app cfg s e).fst.world.inFlight ≤ (step app cfg s e).fst.world.cap ∧
(step app cfg s e).fst.world.cap = s.world.capThe cap is never exceeded. After any event, the capped requests with the host (sent and not answered, or cancelled and not yet answered) number at most the cap, and the cap is unchanged.
start_cap {S : Type} (app : App S) (cfg : Config) (size : Size)
(scale : Nat) :
(start app cfg size scale).world.inFlight = 0 ∧
(start app cfg size scale).world.cap = max 1 app.maxInFlight
steps_cap {S : Type} (app : App S) (cfg : Config) (size : Size) (scale : Nat)
(es : List Event) :
have w := (steps app cfg (start app cfg size scale) es).fst.world;
w.inFlight ≤ w.cap ∧ w.cap = max 1 app.maxInFlightFrom launch, the cap is App.maxInFlight (at least one) and never exceeded.
canSend_false {w : World} {id : Nat} {k : Request.Kind} :
w.canSend id k = false ↔ w.isStopping id = true ∨ k.capped = true ∧ w.cap ≤ w.inFlight
mono {w w' : World} (h : w.Settled)
(hq : ∀ (q : Nat × Nat × Request), q ∈ w'.queued → q ∈ w.queued)
(hs : ∀ (id : Nat), w.isStopping id = true → w'.isStopping id = true)
(hi : w.inFlight ≤ w'.inFlight) (hc : w'.cap = w.cap) : w'.SettledA queued request that can't go stays unable to while nothing is freed: no fewer requests in flight, no fewer ids stopping, the same cap.
agrees_bookOf {w : World} (h : w.Keys) : Agrees w w.bookOf
isStopping_iff (w : World) (id : Nat) : w.isStopping id = true ↔ ∃ k, (id, k) ∈ w.stopping
countP_filter_one {β : Type} (p : Nat × β → Bool) {x : Nat} {v : β}
(l : List (Nat × β)) :
(List.map (fun x => x.fst) l).Nodup →
(x, v) ∈ l →
(List.countP p (List.filter (fun x_1 => x_1.fst != x) l) +
if p (x, v) = true then 1 else 0) =
List.countP p lWith no id twice, filter takes out exactly one entry.
pending_nodup {w : World} (h : w.Keys) :
(List.map (fun x => x.fst) w.pending).Nodup
absorb1_cases (w : World) (e : Effect) : w.Reqs (w.absorb1 e).fst ∨ (∃ id k, w.canSend id k = true ∧ (w.absorb1 e).fst = have __src := w.send id k; { clock := __src.clock, heard := __src.heard, booted := __src.booted, timers := (w.absorb1 e).fst.timers, pending := __src.pending, queued := __src.queued, stopping := __src.stopping, cap := __src.cap, nextTicket := __src.nextTicket, subs := __src.subs, nextSub := __src.nextSub }) ∨ (∃ id r, w.canSend id r.kind = false ∧ (w.absorb1 e).fst = have __src := w.enqueue id r; { clock := __src.clock, heard := __src.heard, booted := __src.booted, timers := (w.absorb1 e).fst.timers, pending := __src.pending, queued := __src.queued, stopping := __src.stopping, cap := __src.cap, nextTicket := __src.nextTicket, subs := __src.subs, nextSub := __src.nextSub }) ∨ ∃ id, (w.absorb1 e).fst = (w.cancel id).fst
What absorb1 does to the request tables.
cancel_cases (w : World) (id : Nat) : (w.cancel id).fst = { clock := w.clock, heard := w.heard, booted := w.booted, timers := w.timers, pending := w.pending, queued := List.filter (fun x => x.snd.fst != id) w.queued, stopping := w.stopping, cap := w.cap, nextTicket := w.nextTicket, subs := w.subs, nextSub := w.nextSub } ∨ (∃ k, List.lookup id w.pending = some k ∧ (w.cancel id).fst = w.stopOne id k) ∨ (w.cancel id).fst = w
fine_reqs {w w' : World} (hr : w.Reqs w') (h : w.Fine) : w'.Fine
settled_reqs {w w' : World} (hr : w.Reqs w') (h : w.Settled) :
w'.Settled
cancel_fine {w : World} (h : w.Fine) (id : Nat) :
(w.cancel id).fst.Fine ∧ (w.Settled → (w.cancel id).fst.Settled)
absorb1_fine {w : World} (h : w.Fine) (e : Effect) :
(w.absorb1 e).fst.Fine ∧ (w.Settled → (w.absorb1 e).fst.Settled)
promoteGo_parts (rest : List (Nat × Nat × Request)) (w : World) : ∃ sent l, (w.promoteGo rest).fst = { clock := w.clock, heard := w.heard, booted := w.booted, timers := w.timers, pending := w.pending ++ sent, queued := w.queued ++ l, stopping := w.stopping, cap := w.cap, nextTicket := w.nextTicket, subs := w.subs, nextSub := w.nextSub } ∧ l.Sublist rest ∧ ∀ (p : Nat × Request.Kind), p ∈ sent → w.isStopping p.fst = false
How promoteGo leaves the tables: some of the requests it was given sent, the rest
appended to the queue in order.
promoteGo_settled (rest : List (Nat × Nat × Request)) (w : World) : w.Settled → (w.promoteGo rest).fst.Settled
promote_settled (w : World) : w.promote.fst.Settled
After promote, nothing waits that could go.
promote_fine {w : World} (h : w.Fine) : w.promote.fst.Fine
takeReply_fine {w w' : World} {id : Nat} {r : Reply} (h : w.Fine)
(hw : w.takeReply id r = some w') : w'.Fine
takeStop_fine {w w' : World} {id : Nat} (h : w.Fine)
(hw : w.takeStop id = some w') : w'.Fine
carries_fine : Carries (fun w => w.Fine ∧ w.Settled) fun x x_1 => TrueFine and settled worlds stay fine and settled.
step_settled {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event)
(h : s.world.Fine ∧ s.world.Settled) :
(step app cfg s e).fst.world.Fine ∧ (step app cfg s e).fst.world.SettledEvery step keeps the tables fine and settled: after any event, nothing waits in the queue that could be sent.
start_fine {S : Type} (app : App S) (cfg : Config) (size : Size)
(scale : Nat) :
(start app cfg size scale).world.Fine ∧ (start app cfg size scale).world.Settled
steps_fine {S : Type} (app : App S) (cfg : Config) (size : Size) (scale : Nat)
(es : List Event) :
(steps app cfg (start app cfg size scale) es).fst.world.Fine ∧
(steps app cfg (start app cfg size scale) es).fst.world.Settled
stopping_not_pending {w : World} (h : w.Fine) {id : Nat}
(hs : w.isStopping id = true) : List.lookup id w.pending = none
takeReply_stopping {w : World} (h : w.Fine) {id : Nat}
(hs : w.isStopping id = true) (r : Reply) : w.takeReply id r = none
promote_stopping (w : World) : w.promote.fst.stopping = w.stopping
step_reply_cancelled {S : Type} (app : App S) (cfg : Config) (s : State S)
{id : Nat} (r : Reply) (h : s.world.Fine) (hs : s.world.isStopping id = true) :
(step app cfg s (Event.reply id r)).fst.app = s.app ∧
(step app cfg s (Event.reply id r)).fst.world.stopping =
List.filter (fun x => x.fst != id) s.world.stoppingA cancelled id never delivers. The host's one reply to a request cancelled after it was sent reaches no app, whatever it says, and the id stops being held: its slot is free and a request under it can be sent.
trans {t : Nat} {a b c : World} (h1 : Drains t a b)
(h2 : Drains t b c) : Drains t a c
drains_same {t : Nat} {w w' : World} (hq : w'.queued = w.queued)
(hs : w'.stopping = w.stopping) : Drains t w w'
drains_sub {t : Nat} {w w' : World} (hq : w'.queued.Sublist w.queued)
(hs : ∀ (id : Nat), w'.isStopping id = true → w.isStopping id = true) : Drains t w w'
live_apart {w : World} (h : w.Keys) {id : Nat} {k : Request.Kind}
(hl : List.lookup id w.pending = some k) (q : Nat × Nat × Request) :
q ∈ w.queued → q.snd.fst ≠ id
stopOne_drains {t : Nat} {w : World} (h : w.Keys) {id : Nat}
{k : Request.Kind} (hl : List.lookup id w.pending = some k) : Drains t w (w.stopOne id k)
absorb1_drains {t : Nat} {w : World} (h : w.Fine)
(ht : t < w.nextTicket) (e : Effect) :
t < (w.absorb1 e).fst.nextTicket ∧ Drains t w (w.absorb1 e).fst
takeStop_isStopping {w w' : World} {id : Nat}
(hw : w.takeStop id = some w') (x : Nat) : w'.isStopping x = true → w.isStopping x = true
promote_queued (w : World) : w.promote.fst.queued.Sublist w.queued ∧ w.promote.fst.stopping = w.stopping ∧ w.promote.fst.nextTicket = w.nextTicket
promote_drains' {t : Nat} (w : World) : Drains t w w.promote.fst
carries_drains (t : Nat) :
Carries (fun w => w.Fine ∧ t < w.nextTicket) (World.Drains t)Fine worlds stay fine, the ticket bound holds, and nothing ahead of a ticket grows.
step_wait_le {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event)
{t : Nat} (h : s.world.Fine) (ht : t < s.world.nextTicket) :
World.Drains t s.world (step app cfg s e).fst.worldNothing ahead grows. Over any event, the count of what holds up the queued requests with
tickets up to t does not grow, and no request up to t joins the queue (every ticket issued is
below nextTicket).
countP_lt {α : Type} {p p' : α → Bool} {a : α} (l : List α) :
(∀ (y : α), y ∈ l → p' y = true → p y = true) →
a ∈ l → p a = true → p' a = false → List.countP p' l < List.countP p l
promoteGo_strict {t : Nat} {q : Nat × Nat × Request} (hq1 : q.fst ≤ t)
(hqc : q.snd.snd.kind.capped = true) (post pre : List (Nat × Nat × Request)) (w : World) :
(∀ (p : Nat × Nat × Request), p ∈ pre → p.fst ≤ t) →
w.isStopping q.snd.fst = false →
w.inFlight < w.cap →
∃ l,
(w.promoteGo (pre ++ q :: post)).fst.queued = w.queued ++ l ∧
l.Sublist (pre ++ q :: post) ∧ capIn t l < capIn t (pre ++ q :: post)With a slot free, promoteGo reaching a capped request q whose id is not stopping sends a
capped request with ticket up to t: q, or one before it.
promote_strict {w : World} (h : w.Fine) {q : Nat × Nat × Request}
(hq : q ∈ w.queued) (hqc : q.snd.snd.kind.capped = true)
(hs : w.isStopping q.snd.fst = false) (hc : w.inFlight < w.cap) :
w.promote.fst.ahead q.fst < w.ahead q.fstWith a slot free and a capped queued request whose id is not stopping, promote makes the
count ahead of it shrink.
queued_blocked {w : World} (h : w.Fine) (hs : w.Settled)
{q : Nat × Nat × Request} (hq : q ∈ w.queued) : ∃ x, w.Blocks q xEvery queued request has a blocker: in a fine, settled world a queued request waits for a request that is with the host.
freed_strict {w w2 : World} (h2 : w2.Fine) {q : Nat × Nat × Request}
(hq : q ∈ w2.queued) (hqc : q.snd.snd.kind.capped = true)
(hs : w2.isStopping q.snd.fst = false) (hc : w2.inFlight < w2.cap)
(hd : w2.ahead q.fst ≤ w.ahead q.fst) : w2.promote.fst.ahead q.fst < w.ahead q.fstTaking a capped request out of the tables frees a slot; then promote shrinks the count
ahead of a capped queued request whose id is free.
takeReply_frees {w w2 : World} (h : w.Fine) {x : Nat} {k : Request.Kind}
{r : Reply} (hm : (x, k) ∈ w.pending) (hk : k.capped = true)
(hw : w.takeReply x r = some w2) : w2.inFlight < w2.cap
takeStop_frees {w w2 : World} (h : w.Fine) {x : Nat} {k : Request.Kind}
(hm : (x, k) ∈ w.stopping) (hk : k.capped = true) (hw : w.takeStop x = some w2) :
w2.inFlight < w2.cap
takeStop_some_of {w : World} {x : Nat} {k : Request.Kind}
(hm : (x, k) ∈ w.stopping) : ∃ w2, w.takeStop x = some w2
trans {x : Nat} {k : Request.Kind} {a b c : World}
(h1 : Track x k a b) (h2 : Track x k b c) : Track x k a c
absorb1_track {w : World} (h : w.Fine) (e : Effect) (x : Nat)
(k : Request.Kind) : Track x k w (w.absorb1 e).fst
through_track (t x : Nat) (k : Request.Kind) : Through (fun w => w.Fine ∧ t < w.nextTicket) fun w w' => World.Drains t w w' ∧ World.Track x k w w'
Absorbing effects keeps the drain and tracks a request with the host.
step_drains {S : Type} (app : App S) (cfg : Config) (s : State S)
{q : Nat × Nat × Request} {x : Nat} {r : Reply} (h : s.world.Fine)
(hq : q ∈ s.world.queued) (hb : s.world.Blocks q x)
(hr :
∀ (k : Request.Kind),
List.lookup x s.world.pending = some k → Reply.answers k r = true) :
¬q ∈ (step app cfg s (Event.reply x r)).fst.world.queued ∨
(step app cfg s (Event.reply x r)).fst.world.ahead q.fst < s.world.ahead q.fstThe reply to a blocker drains the queue. If x blocks a queued request q and the host
answers x (in the shape that answers its kind, if it is pending), then afterwards q has left
the queue (sent or cancelled), or the count ahead of it is smaller. With step_wait_le and
queued_blocked, q leaves the queue after at most ahead q.1 replies to its blockers.
Keeping a property through a step
The runtime changes the request tables in five ways only: absorbing an effect, taking a reply
or a cancelled request's reply (each followed by promote), and updates that leave the tables
alone (the clock, timers, subscriptions). A property of worlds I, with a relation R between
a world and a later one, that each of these keeps is kept by a whole step.
The cap
Fine worlds: the tables' own invariants
A cancelled request's reply
Every queued request is eventually sent or cancelled
Fix a queued request q with ticket t. ahead w t counts what holds the requests up to t:
the capped ones among them (each needs a slot) and those whose id is still stopping (each needs
that reply). Nothing the runtime does makes it grow (step_wait_le), and the reply to whatever
blocks q either takes q out of the queue or makes it shrink (step_drains).