bend-kit-scheduler
Releases (5)
Definitions (126)
queue.bend
- type Ticket
- type State
- def id
- def deadline
- def payload
- def le.same
- def le
- def new
- def enqueue
- def select.due
- def select
- def remove.list.keepponytail: eager O(n) cancellation; indexed deletion if cancellation dominates.
- def remove.list
- def remove.heap.keep
- def remove.heap
- def cancel
- def find.list.chooseReference observation for laws; completion uses the single-pass take below.
- def find.list
- type Taken
- def take.keepRemove all matching entries and return the first token in one traversal.
- def take.list
- def complete.taken
- def complete
- def requeue.found
- def requeue.completed
- def requeue
- def next_idNon-consuming observations used by adapters and laws.
- def pending
- def running
queue_laws.bend
- type BothOrdinary & pairs are affine even when their fields are Data.
- def state
- def selected
- def requeued
- def enqueued
- def assigned
- def complete.referenceReference semantics are deliberately simple; the live transition takes one pass and its equivalence is proved universally, including duplicate IDs.
- def requeue.reference
- law take_equivalent
- law complete_equivalent
- law requeue_equivalent
- def absent.list
- def all.heap
- def absent.ticket
- def bound.ticket
- def absent.heap
- def below
- def orderedThe root must bound both subtrees recursively, not just its direct children.
- def due
- def minimum
- law new_ordered
- law select_due
- law select_minimum
- law equal_deadline_fifo
- law enqueue_id
- law cancel_pending_absent
- law cancel_running_absent
- law absent_find
- law complete_one_shot
- law cancel_complete
- law cancel_requeue
- law complete_requeue
- law select_absentAn absent ID stays absent on every selection, in both registries.
- law absent_selected
- law enqueue_ordered
- law select_ordered
- law cancel_ordered
- def requeue.state
- law requeue_ordered
- law complete_ordered
- law enqueue_assigned_id
- law cancel_keeps_counter
- law complete_keeps_counter
- law select_keeps_counter
- law requeue_keeps_counter
- law requeue_tokenThe running token, not a newly assigned ID, is moved back to pending.
- law complete_token
queue_proof.bend
- def split
- def take_equivalent.step
- def key_refl
- def key_succ
- def key_succ.premise
- def key_succ.conclusion
- def key_flip
- def key_trans
- def le_refl
- def le_flip
- def le_trans
- def merge_allMerging cannot introduce an element that violates any predicate P.
- def merge_all.full
- def below_trans
- def merge_ordered
- def merge_ordered.full
- def remove_all
- def remove_ordered
- def remove_absent.heap
- def remove_absent.list
- def requeue_absent
- def selected_absent
- def select_selected_absent
- def push_ordered