Library prosa.classic.model.schedule.uni.basic.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.schedule.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module Platform.
Import Job SporadicTaskset UniprocessorSchedule 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 arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Section Execution.
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
∃ j_other, scheduled_at sched j_other t.
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 →
backlogged job_arrival job_cost sched j t →
scheduled_at 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 →
backlogged job_arrival job_cost sched j t →
scheduled_at 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 →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
End Properties.
Section Lemmas.
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 arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Let job_backlogged_at := backlogged job_arrival job_cost sched.
Let job_pending_at := pending job_arrival job_cost sched.
Let job_completed_by := completed_by job_cost sched.
Section JobNeverBacklogged.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Variable j: Job.
Hypothesis H_j_is_never_backlogged:
∀ t,
job_arrival j ≤ t < job_arrival j + job_cost j →
¬ job_backlogged_at j t.
Lemma job_never_backlogged_response_time_holds:
∀ R,
R ≥ job_cost j →
job_completed_by j (job_arrival j + R).
End JobNeverBacklogged.
End Lemmas.
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.schedule.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module Platform.
Import Job SporadicTaskset UniprocessorSchedule 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 arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Section Execution.
Definition work_conserving :=
∀ j t,
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
∃ j_other, scheduled_at sched j_other t.
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 →
backlogged job_arrival job_cost sched j t →
scheduled_at 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 →
backlogged job_arrival job_cost sched j t →
scheduled_at 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 →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
End Properties.
Section Lemmas.
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 arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Let job_backlogged_at := backlogged job_arrival job_cost sched.
Let job_pending_at := pending job_arrival job_cost sched.
Let job_completed_by := completed_by job_cost sched.
Section JobNeverBacklogged.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Variable j: Job.
Hypothesis H_j_is_never_backlogged:
∀ t,
job_arrival j ≤ t < job_arrival j + job_cost j →
¬ job_backlogged_at j t.
Lemma job_never_backlogged_response_time_holds:
∀ R,
R ≥ job_cost j →
job_completed_by j (job_arrival j + R).
End JobNeverBacklogged.
End Lemmas.
End Platform.