Skip to main content

Module backpressure

Module backpressure 

Source
Expand description

Admission control: the city-wide shedding posture. One function serves every queue-shaped resource — signal queues and fd headroom alike; capacity semantics belong to the caller. Queues and counters live in storage::queue, never here. The part crates/kernel/spec/Backpressure.lean specifies this module.

Structs§

ItemMeta
What admitting this item would cost: one slot for a Signal, more for a new-Run fd reservation.
QueueStats
A queue’s occupancy snapshot.

Enums§

Admission
Deliberately exhaustive: a new admission outcome must force every caller to decide.
ShedReason

Functions§

admit
Decides whether the queue admits one more item. Pure and total: depth + cost <= capacity admits; checked arithmetic, overflow sheds (fail-closed). Shedding refuses new items only — starving what is already queued is a liveness property and citysim’s to assert.