Library rt.restructuring.model.readiness.basic
We define the readiness indicator function for the classic Liu & Layland
model without jitter and no self-suspensions, where jobs are always
ready.
Consider any kind of jobs...
... and any kind of processor state.
Supose jobs have an arrival time and a cost.
In the basic Liu & Layland model, a job is ready iff it is pending.
Global Program Instance basic_ready_instance : JobReady Job PState :=
{
job_ready sched j t := pending sched j t
}.
End LiuAndLaylandReadiness.
{
job_ready sched j t := pending sched j t
}.
End LiuAndLaylandReadiness.