Library rt.restructuring.behavior.schedule
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From rt.restructuring.behavior Require Export arrival_sequence.
(* We define the notion of a generic processor state. The processor state type
determines aspects of the execution environment are modeled (e.g., overheads, spinning).
In the most simple case (i.e., Ideal.processor_state), at any time,
either a particular job is either scheduled or it is idle. *)
Class ProcessorState (Job : JobType) (State : Type) :=
{
(* For a given processor state, the [scheduled_in] predicate checks whether a given
job is running in that state. *)
scheduled_in: Job → State → bool;
(* For a given processor state, the [service_in] function determines how much
service a given job receives in that state. *)
service_in: Job → State → nat;
(* For a given processor state, a job does not receive service if it is not scheduled
in that state *)
service_implies_scheduled :
∀ j s, scheduled_in j s = false → service_in j s = 0
}.
(* A schedule maps an instant to a processor state *)
Definition schedule (PState : Type) := instant → PState.
Section Schedule.
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
Variable sched : schedule PState.
(* First, we define whether a job j is scheduled at time t, ... *)
Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
(* ... and the instantaneous service received by
job j at time t. *)
Definition service_at (j : Job) (t : instant) := service_in j (sched t).
(* Based on the notion of instantaneous service, we define the
cumulative service received by job j during any interval [t1, t2). *)
Definition service_during (j : Job) (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) service_at j t.
(* Using the previous definition, we define the cumulative service
received by job j up to time t, i.e., during interval [0, t). *)
Definition service (j : Job) (t : instant) := service_during j 0 t.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Context `{JobArrival Job}.
(* Next, we say that job j has completed by time t if it received enough
service in the interval [0, t). *)
Definition completed_by (j : Job) (t : instant) := service j t ≥ job_cost j.
(* We say that job j completes at time t if it has completed by time t but
not by time t - 1 *)
Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
(* We say that R is a response time bound of a job j if j has completed
by R units after its arrival *)
Definition job_response_time_bound (j : Job) (R : duration) :=
completed_by j (job_arrival j + R).
(* We say that a job meets its deadline if it completes by its absolute deadline *)
Definition job_meets_deadline (j : Job) :=
completed_by j (job_deadline j).
(* Job j is pending at time t iff it has arrived but has not yet completed. *)
Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
(* Job j is pending earlier and at time t iff it has arrived before time t
and has not been completed yet. *)
Definition pending_earlier_and_at (j : Job) (t : instant) :=
arrived_before j t && ~~ completed_by j t.
(* Job j is backlogged at time t iff it is pending and not scheduled. *)
Definition backlogged (j : Job) (t : instant) := pending j t && ~~ scheduled_at j t.
(* Let's define the remaining cost of job j as the amount of service
that has to be received for its completion. *)
Definition remaining_cost j t :=
job_cost j - service j t.
(* In this section, we define valid schedules. *)
Section ValidSchedule.
(* We define whether jobs come from some arrival sequence... *)
Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
∀ j t, scheduled_at j t → arrives_in arr_seq j.
(* ..., whether a job can only be scheduled if it has arrived ... *)
Definition jobs_must_arrive_to_execute :=
∀ j t, scheduled_at j t → has_arrived j t.
(* ... and whether a job cannot be scheduled after it completes. *)
Definition completed_jobs_dont_execute :=
∀ j t, service j t ≤ job_cost j.
(* We say that the schedule is valid iff
- jobs come from some arrival sequence
- a job can only be scheduled if it has arrived and is not completed yet *)
Definition valid_schedule (arr_seq : arrival_sequence Job) :=
jobs_come_from_arrival_sequence arr_seq ∧
jobs_must_arrive_to_execute ∧
completed_jobs_dont_execute.
End ValidSchedule.
End Schedule.
From rt.restructuring.behavior Require Export arrival_sequence.
(* We define the notion of a generic processor state. The processor state type
determines aspects of the execution environment are modeled (e.g., overheads, spinning).
In the most simple case (i.e., Ideal.processor_state), at any time,
either a particular job is either scheduled or it is idle. *)
Class ProcessorState (Job : JobType) (State : Type) :=
{
(* For a given processor state, the [scheduled_in] predicate checks whether a given
job is running in that state. *)
scheduled_in: Job → State → bool;
(* For a given processor state, the [service_in] function determines how much
service a given job receives in that state. *)
service_in: Job → State → nat;
(* For a given processor state, a job does not receive service if it is not scheduled
in that state *)
service_implies_scheduled :
∀ j s, scheduled_in j s = false → service_in j s = 0
}.
(* A schedule maps an instant to a processor state *)
Definition schedule (PState : Type) := instant → PState.
Section Schedule.
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
Variable sched : schedule PState.
(* First, we define whether a job j is scheduled at time t, ... *)
Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
(* ... and the instantaneous service received by
job j at time t. *)
Definition service_at (j : Job) (t : instant) := service_in j (sched t).
(* Based on the notion of instantaneous service, we define the
cumulative service received by job j during any interval [t1, t2). *)
Definition service_during (j : Job) (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) service_at j t.
(* Using the previous definition, we define the cumulative service
received by job j up to time t, i.e., during interval [0, t). *)
Definition service (j : Job) (t : instant) := service_during j 0 t.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Context `{JobArrival Job}.
(* Next, we say that job j has completed by time t if it received enough
service in the interval [0, t). *)
Definition completed_by (j : Job) (t : instant) := service j t ≥ job_cost j.
(* We say that job j completes at time t if it has completed by time t but
not by time t - 1 *)
Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
(* We say that R is a response time bound of a job j if j has completed
by R units after its arrival *)
Definition job_response_time_bound (j : Job) (R : duration) :=
completed_by j (job_arrival j + R).
(* We say that a job meets its deadline if it completes by its absolute deadline *)
Definition job_meets_deadline (j : Job) :=
completed_by j (job_deadline j).
(* Job j is pending at time t iff it has arrived but has not yet completed. *)
Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
(* Job j is pending earlier and at time t iff it has arrived before time t
and has not been completed yet. *)
Definition pending_earlier_and_at (j : Job) (t : instant) :=
arrived_before j t && ~~ completed_by j t.
(* Job j is backlogged at time t iff it is pending and not scheduled. *)
Definition backlogged (j : Job) (t : instant) := pending j t && ~~ scheduled_at j t.
(* Let's define the remaining cost of job j as the amount of service
that has to be received for its completion. *)
Definition remaining_cost j t :=
job_cost j - service j t.
(* In this section, we define valid schedules. *)
Section ValidSchedule.
(* We define whether jobs come from some arrival sequence... *)
Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
∀ j t, scheduled_at j t → arrives_in arr_seq j.
(* ..., whether a job can only be scheduled if it has arrived ... *)
Definition jobs_must_arrive_to_execute :=
∀ j t, scheduled_at j t → has_arrived j t.
(* ... and whether a job cannot be scheduled after it completes. *)
Definition completed_jobs_dont_execute :=
∀ j t, service j t ≤ job_cost j.
(* We say that the schedule is valid iff
- jobs come from some arrival sequence
- a job can only be scheduled if it has arrived and is not completed yet *)
Definition valid_schedule (arr_seq : arrival_sequence Job) :=
jobs_come_from_arrival_sequence arr_seq ∧
jobs_must_arrive_to_execute ∧
completed_jobs_dont_execute.
End ValidSchedule.
End Schedule.