Library prosa.classic.model.schedule.global.jitter.schedule
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require prosa.classic.model.schedule.global.basic.schedule.
Module ScheduleWithJitter.
Export prosa.classic.model.schedule.global.basic.schedule.
Export ArrivalSequence Schedule.
Section ArrivalDependentProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Section JobProperties.
Variable j: Job.
Definition actual_arrival := job_arrival j + job_jitter j.
Definition jitter_has_passed (t: time) := actual_arrival ≤ t.
Definition actual_arrival_before (t: time) := actual_arrival < t.
Definition pending (t: time) := jitter_has_passed t && ~~ completed job_cost sched j t.
Definition backlogged (t: time) := pending t && ~~ scheduled sched j t.
End JobProperties.
Section ScheduleProperties.
Definition jobs_execute_after_jitter :=
∀ j t,
scheduled sched j t → jitter_has_passed j t.
End ScheduleProperties.
Section BasicLemmas.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter.
Section Pending.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma scheduled_implies_pending:
∀ j t,
scheduled sched j t →
pending j t.
End Pending.
Section Service.
Lemma arrival_before_jitter :
jobs_must_arrive_to_execute job_arrival sched.
Lemma service_before_jitter_zero :
∀ j t,
t < job_arrival j + job_jitter j →
service_at sched j t = 0.
Lemma cumulative_service_before_jitter_zero :
∀ j t1 t2,
t2 ≤ job_arrival j + job_jitter j →
\sum_(t1 ≤ t < t2) service_at sched j t = 0.
End Service.
End BasicLemmas.
End ArrivalDependentProperties.
End ScheduleWithJitter.
Module ScheduleOfSporadicTaskWithJitter.
Import SporadicTask Job.
Export ScheduleWithJitter.
Section ScheduledJobs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable tsk: sporadic_task.
Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
if (sched cpu t) is Some j then
(job_task j == tsk)
else false.
Definition task_is_scheduled (t: time) :=
[∃ cpu, task_scheduled_on cpu t].
Definition jobs_of_task_scheduled_between (t1 t2: time) :=
filter (fun j ⇒ job_task j == tsk)
(jobs_scheduled_between sched t1 t2).
End ScheduledJobs.
Section ScheduleProperties.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Definition jobs_of_same_task_dont_execute_in_parallel :=
∀ j j' t,
job_task j = job_task j' →
scheduled sched j t →
scheduled sched j' t →
j = j'.
End ScheduleProperties.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable arr_seq: arrival_sequence Job.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis jobs_dont_execute_after_completion :
completed_jobs_dont_execute job_cost sched.
Variable tsk: sporadic_task.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_task: job_task j = tsk.
Hypothesis valid_job:
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Lemma cumulative_service_le_task_cost :
∀ t t',
service_during sched j t t' ≤ task_cost tsk.
End BasicLemmas.
End ScheduleOfSporadicTaskWithJitter.
Require Import prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require prosa.classic.model.schedule.global.basic.schedule.
Module ScheduleWithJitter.
Export prosa.classic.model.schedule.global.basic.schedule.
Export ArrivalSequence Schedule.
Section ArrivalDependentProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Section JobProperties.
Variable j: Job.
Definition actual_arrival := job_arrival j + job_jitter j.
Definition jitter_has_passed (t: time) := actual_arrival ≤ t.
Definition actual_arrival_before (t: time) := actual_arrival < t.
Definition pending (t: time) := jitter_has_passed t && ~~ completed job_cost sched j t.
Definition backlogged (t: time) := pending t && ~~ scheduled sched j t.
End JobProperties.
Section ScheduleProperties.
Definition jobs_execute_after_jitter :=
∀ j t,
scheduled sched j t → jitter_has_passed j t.
End ScheduleProperties.
Section BasicLemmas.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter.
Section Pending.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma scheduled_implies_pending:
∀ j t,
scheduled sched j t →
pending j t.
End Pending.
Section Service.
Lemma arrival_before_jitter :
jobs_must_arrive_to_execute job_arrival sched.
Lemma service_before_jitter_zero :
∀ j t,
t < job_arrival j + job_jitter j →
service_at sched j t = 0.
Lemma cumulative_service_before_jitter_zero :
∀ j t1 t2,
t2 ≤ job_arrival j + job_jitter j →
\sum_(t1 ≤ t < t2) service_at sched j t = 0.
End Service.
End BasicLemmas.
End ArrivalDependentProperties.
End ScheduleWithJitter.
Module ScheduleOfSporadicTaskWithJitter.
Import SporadicTask Job.
Export ScheduleWithJitter.
Section ScheduledJobs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable tsk: sporadic_task.
Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
if (sched cpu t) is Some j then
(job_task j == tsk)
else false.
Definition task_is_scheduled (t: time) :=
[∃ cpu, task_scheduled_on cpu t].
Definition jobs_of_task_scheduled_between (t1 t2: time) :=
filter (fun j ⇒ job_task j == tsk)
(jobs_scheduled_between sched t1 t2).
End ScheduledJobs.
Section ScheduleProperties.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Definition jobs_of_same_task_dont_execute_in_parallel :=
∀ j j' t,
job_task j = job_task j' →
scheduled sched j t →
scheduled sched j' t →
j = j'.
End ScheduleProperties.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable arr_seq: arrival_sequence Job.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis jobs_dont_execute_after_completion :
completed_jobs_dont_execute job_cost sched.
Variable tsk: sporadic_task.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_task: job_task j = tsk.
Hypothesis valid_job:
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Lemma cumulative_service_le_task_cost :
∀ t t',
service_during sched j t t' ≤ task_cost tsk.
End BasicLemmas.
End ScheduleOfSporadicTaskWithJitter.