Library prosa.classic.model.schedule.global.jitter.platform
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule
prosa.classic.model.schedule.global.jitter.interference.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module Platform.
Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset TaskArrival Interference 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_task: Job → sporadic_task.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Let job_is_backlogged := backlogged job_arrival job_cost job_jitter sched.
Section Execution.
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
job_is_backlogged j t →
∀ cpu, ∃ j_other,
scheduled_on sched j_other cpu t.
Definition work_conserving_count :=
∀ j t,
arrives_in arr_seq j →
job_is_backlogged j t →
size (jobs_scheduled_at sched t) = num_cpus.
End Execution.
Section FP.
Variable higher_eq_priority: FP_policy sporadic_task.
Definition respects_FP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_is_backlogged j t →
scheduled sched j_hp t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
Section JLFP.
Variable higher_eq_priority: JLFP_policy Job.
Definition respects_JLFP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_is_backlogged j t →
scheduled sched j_hp t →
higher_eq_priority j_hp j.
End JLFP.
Section JLDP.
Variable higher_eq_priority: JLDP_policy Job.
Definition respects_JLDP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_is_backlogged j t →
scheduled sched j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
Section Lemmas.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Section EquivalentDefinitions.
Lemma work_conserving_eq_work_conserving_count :
work_conserving ↔ work_conserving_count.
End EquivalentDefinitions.
End Lemmas.
End Properties.
End Platform.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule
prosa.classic.model.schedule.global.jitter.interference.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module Platform.
Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset TaskArrival Interference 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_task: Job → sporadic_task.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Let job_is_backlogged := backlogged job_arrival job_cost job_jitter sched.
Section Execution.
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
job_is_backlogged j t →
∀ cpu, ∃ j_other,
scheduled_on sched j_other cpu t.
Definition work_conserving_count :=
∀ j t,
arrives_in arr_seq j →
job_is_backlogged j t →
size (jobs_scheduled_at sched t) = num_cpus.
End Execution.
Section FP.
Variable higher_eq_priority: FP_policy sporadic_task.
Definition respects_FP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_is_backlogged j t →
scheduled sched j_hp t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
Section JLFP.
Variable higher_eq_priority: JLFP_policy Job.
Definition respects_JLFP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_is_backlogged j t →
scheduled sched j_hp t →
higher_eq_priority j_hp j.
End JLFP.
Section JLDP.
Variable higher_eq_priority: JLDP_policy Job.
Definition respects_JLDP_policy :=
∀ j j_hp t,
arrives_in arr_seq j →
job_is_backlogged j t →
scheduled sched j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
Section Lemmas.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Section EquivalentDefinitions.
Lemma work_conserving_eq_work_conserving_count :
work_conserving ↔ work_conserving_count.
End EquivalentDefinitions.
End Lemmas.
End Properties.
End Platform.