Library rt.restructuring.model.schedule.work_conserving
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Export all.
In this file, we introduce a restrictive definition of work conserving
uniprocessor schedules. The definition is restrictive because it does not
allow for effects such as jitter or self-suspensions that affect whether a
job can be scheduled at a given point in time. A more general notion of work
conservation that is "readiness-aware", as well as a variant that covers
global scheduling, is TBD.
Consider any type of job associated with any type of tasks...
... with arrival times and costs ...
... and any kind of processor state model.
Further, allow for any notion of job readiness.
Given an arrival sequence and a schedule ...
We say that a scheduler is work-conserving iff whenever a job j
is backlogged, the processor is always busy with another job.
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
backlogged sched j t →
∃ j_other, scheduled_at sched j_other t.
End WorkConserving.
∀ j t,
arrives_in arr_seq j →
backlogged sched j t →
∃ j_other, scheduled_at sched j_other t.
End WorkConserving.