# Library prosa.model.schedule.work_conserving

# Definition of Work Conservation

Consider any type of jobs...

... with arrival times and costs ...

... and any kind of processor 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 executing another job j_other. Note that this definition is intentionally silent on matters of priority.
Definition work_conserving :=

∀ j t,

arrives_in arr_seq j →

backlogged sched j t →

∃ j_other, scheduled_at sched j_other t.

∀ j t,

arrives_in arr_seq j →

backlogged sched j t →

∃ j_other, scheduled_at sched j_other t.

Related to this, we define the set of all jobs that are backlogged at a
given time t, i.e., the set of jobs that could be scheduled, and which
a work-conserving scheduler must hence consider.

Definition jobs_backlogged_at (t : instant): seq Job :=

[seq j <- arrivals_up_to arr_seq t | backlogged sched j t].

End WorkConserving.

[seq j <- arrivals_up_to arr_seq t | backlogged sched j t].

End WorkConserving.