Library rt.restructuring.behavior.ready
From rt.restructuring.behavior Require Export schedule.
(* Definition of a general notion of readiness of a job: a job can be scheduled
only when it is ready. This notion of readiness is a general concept that is
used to model jitter, self-suspensions, etc. *)
Class JobReady (PState : Type) (J : JobType) := job_ready : schedule PState → J → instant → bool.
Section Backlogged.
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
Variable sched : schedule PState.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Context `{JobArrival Job}.
Context `{JobReady PState Job}.
(* Job j is backlogged at time t iff it is ready and not scheduled. *)
Definition backlogged (j : Job) (t : instant) := job_ready sched j t && ~~ scheduled_at sched j t.
(* ..., whether a job can only be scheduled if it is ready ... *)
Definition jobs_must_be_ready_to_execute :=
∀ j t, scheduled_at sched j t → job_ready sched j t.
End Backlogged.
(* Definition of a general notion of readiness of a job: a job can be scheduled
only when it is ready. This notion of readiness is a general concept that is
used to model jitter, self-suspensions, etc. *)
Class JobReady (PState : Type) (J : JobType) := job_ready : schedule PState → J → instant → bool.
Section Backlogged.
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
Variable sched : schedule PState.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Context `{JobArrival Job}.
Context `{JobReady PState Job}.
(* Job j is backlogged at time t iff it is ready and not scheduled. *)
Definition backlogged (j : Job) (t : instant) := job_ready sched j t && ~~ scheduled_at sched j t.
(* ..., whether a job can only be scheduled if it is ready ... *)
Definition jobs_must_be_ready_to_execute :=
∀ j t, scheduled_at sched j t → job_ready sched j t.
End Backlogged.