Library prosa.classic.model.schedule.uni.jitter.platform
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(* In this file, we define properties about the platform in jitter-aware schedules. *)
Module Platform.
Import Job SporadicTaskset UniprocessorScheduleWithJitter Priority.
Section Properties.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → sporadic_task.
(* Consider any jitter-aware uniprocessor schedule. *)
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
(* First, we define properties related to execution. *)
Section Execution.
(* We say that a scheduler is work-conserving iff whenever a job j
is backlogged, the processor is always busy with another job.
(Note that the definition of backlogged depends on the jitter.) *)
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
∃ j_other, scheduled_at sched j_other t.
End Execution.
(* Next, we define properties related to FP scheduling. *)
Section FP.
(* We say that an FP policy...*)
Variable higher_eq_priority: FP_policy sporadic_task.
(* ...is respected by the schedule iff a scheduled task has
higher (or same) priority than (as) any backlogged task.
(Note that the definition of backlogged depends on the jitter.) *)
Definition respects_FP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
scheduled_at sched j_hp t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
(* Next, we define properties related to JLFP policies. *)
Section JLFP.
(* We say that a JLFP policy ...*)
Variable higher_eq_priority: JLFP_policy Job.
(* ... is respected by the scheduler iff a scheduled job has
higher (or same) priority than (as) any backlogged job.
(Note that the definition of backlogged depends on the jitter.) *)
Definition respects_JLFP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
scheduled_at sched j_hp t →
higher_eq_priority j_hp j.
End JLFP.
(* Next, we define properties related to JLDP policies. *)
Section JLDP.
(* We say that a JLFP/JLDP policy ...*)
Variable higher_eq_priority: JLDP_policy Job.
(* ... is respected by the scheduler iff at any time t, a scheduled job
has higher (or same) priority than (as) any backlogged job.
(Note that the definition of backlogged depends on the jitter.) *)
Definition respects_JLDP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
scheduled_at sched j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
End Properties.
End Platform.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(* In this file, we define properties about the platform in jitter-aware schedules. *)
Module Platform.
Import Job SporadicTaskset UniprocessorScheduleWithJitter Priority.
Section Properties.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → sporadic_task.
(* Consider any jitter-aware uniprocessor schedule. *)
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
(* First, we define properties related to execution. *)
Section Execution.
(* We say that a scheduler is work-conserving iff whenever a job j
is backlogged, the processor is always busy with another job.
(Note that the definition of backlogged depends on the jitter.) *)
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
∃ j_other, scheduled_at sched j_other t.
End Execution.
(* Next, we define properties related to FP scheduling. *)
Section FP.
(* We say that an FP policy...*)
Variable higher_eq_priority: FP_policy sporadic_task.
(* ...is respected by the schedule iff a scheduled task has
higher (or same) priority than (as) any backlogged task.
(Note that the definition of backlogged depends on the jitter.) *)
Definition respects_FP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
scheduled_at sched j_hp t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
(* Next, we define properties related to JLFP policies. *)
Section JLFP.
(* We say that a JLFP policy ...*)
Variable higher_eq_priority: JLFP_policy Job.
(* ... is respected by the scheduler iff a scheduled job has
higher (or same) priority than (as) any backlogged job.
(Note that the definition of backlogged depends on the jitter.) *)
Definition respects_JLFP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
scheduled_at sched j_hp t →
higher_eq_priority j_hp j.
End JLFP.
(* Next, we define properties related to JLDP policies. *)
Section JLDP.
(* We say that a JLFP/JLDP policy ...*)
Variable higher_eq_priority: JLDP_policy Job.
(* ... is respected by the scheduler iff at any time t, a scheduled job
has higher (or same) priority than (as) any backlogged job.
(Note that the definition of backlogged depends on the jitter.) *)
Definition respects_JLDP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
scheduled_at sched j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
End Properties.
End Platform.