Library rt.model.basic.schedule
Require Import
rt.util.all
rt.model.basic.job rt.model.basic.task rt.model.basic.arrival_sequence.
(* Definition, properties and lemmas about schedules. *)
Module Schedule.
Export ArrivalSequence.
(* A processor is defined as a bounded natural number: 0, num_cpus). *)
Definition processor (num_cpus: nat) := 'I_num_cpus.
Section ScheduleDef.
Context {Job: eqType}.
(* Given the number of processors and an arrival sequence, ...*)
Variable num_cpus: nat.
Variable arr_seq: arrival_sequence Job.
(* ... we define a schedule as a mapping such that each processor
at each time contains either a job from the sequence or none. *)
Definition schedule :=
processor num_cpus → time → option (JobIn arr_seq).
End ScheduleDef.
(* Next, we define properties of jobs in a schedule. *)
Section ScheduledJobs.
Context {Job: eqType}.
(* Given an arrival sequence, ... *)
Context {arr_seq: arrival_sequence Job}.
Variable job_cost: Job → time. (* ... a job cost function, ... *)
(* ... and the number of processors, ...*)
Context {num_cpus: nat}.
(* ... we define the following properties for job j in schedule sched. *)
Variable sched: schedule num_cpus arr_seq.
Variable j: JobIn arr_seq.
(* A job j is scheduled on processor cpu at time t iff such a mapping exists. *)
Definition scheduled_on (cpu: processor num_cpus) (t: time) :=
sched cpu t == Some j.
(* A job j is scheduled at time t iff there exists a cpu where it is mapped.*)
Definition scheduled (t: time) :=
[∃ cpu, scheduled_on cpu t].
(* A processor cpu is idle at time t if it doesn't contain any jobs. *)
Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
sched cpu t = None.
(* The instantaneous service of job j at time t is the number of cpus
where it is scheduled on. Note that we use a sum to account for
parallelism if required. *)
Definition service_at (t: time) :=
\sum_(cpu < num_cpus | scheduled_on cpu t) 1.
(* The cumulative service received by job j during 0, t'). *)
Definition service (t': time) := \sum_(0 ≤ t < t') service_at t.
(* The cumulative service received by job j during t1, t2). *)
Definition service_during (t1 t2: time) := \sum_(t1 ≤ t < t2) service_at t.
(* Job j has completed at time t if it received enough service. *)
Definition completed (t: time) := service t == job_cost j.
(* Job j is pending at time t iff it has arrived but has not completed. *)
Definition pending (t: time) := has_arrived j t && ~~completed t.
(* Job j is backlogged at time t iff it is pending and not scheduled. *)
Definition backlogged (t: time) := pending t && ~~scheduled t.
(* Job j is carry-in in interval t1, t2) iff it arrives before t1 and is not complete at time t1 *)
Definition carried_in (t1: time) := arrived_before j t1 && ~~ completed t1.
(* Job j is carry-out in interval t1, t2) iff it arrives after t1 and is not complete at time t2 *)
Definition carried_out (t1 t2: time) := arrived_before j t2 && ~~ completed t2.
(* The list of scheduled jobs at time t is the concatenation of the jobs
scheduled on each processor. *)
Definition jobs_scheduled_at (t: time) :=
\cat_(cpu < num_cpus) make_sequence (sched cpu t).
(* The list of jobs scheduled during the interval t1, t2) is the the duplicate-free concatenation of the jobs scheduled at instant. *)
Definition jobs_scheduled_between (t1 t2: time) :=
undup (\cat_(t1 ≤ t < t2) jobs_scheduled_at t).
End ScheduledJobs.
(* In this section, we define properties of valid schedules. *)
Section ValidSchedules.
Context {Job: eqType}. (* Assume a job type with decidable equality, ...*)
Context {arr_seq: arrival_sequence Job}. (* ..., an arrival sequence, ...*)
Variable job_cost: Job → time. (* ... a cost function, .... *)
(* ... and a schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Next, we define whether job are sequential, ... *)
Definition sequential_jobs :=
∀ j t cpu1 cpu2,
sched cpu1 t = Some j → sched cpu2 t = Some j → cpu1 = cpu2.
(* ... whether a job can only be scheduled if it has arrived, ... *)
Definition jobs_must_arrive_to_execute :=
∀ j t, scheduled sched j t → has_arrived j t.
(* ... whether a job can be scheduled after it completes. *)
Definition completed_jobs_dont_execute :=
∀ j t, service sched j t ≤ job_cost j.
End ValidSchedules.
(* In this section, we prove some basic lemmas about a job. *)
Section JobLemmas.
(* Consider an arrival sequence, ...*)
Context {Job: eqType}.
Context {arr_seq: arrival_sequence Job}.
(* ... a job cost function, ...*)
Variable job_cost: Job → time.
(* ..., and a particular schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Next, we prove some lemmas about the service received by a job j. *)
Variable j: JobIn arr_seq.
Section Basic.
(* At any time t, job j is not scheduled iff it doesn't get service. *)
Lemma not_scheduled_no_service :
∀ t,
~~ scheduled sched j t = (service_at sched j t == 0).
(* If the cumulative service during a time interval is not zero, there
must be a time t in this interval where the service is not 0, ... *)
Lemma cumulative_service_implies_service :
∀ t1 t2,
service_during sched j t1 t2 != 0 →
∃ t,
t1 ≤ t < t2 ∧
service_at sched j t != 0.
(* ... and vice versa. *)
Lemma service_implies_cumulative_service:
∀ t t1 t2,
t1 ≤ t < t2 →
service_at sched j t != 0 →
service_during sched j t1 t2 != 0.
End Basic.
Section SequentialJobs.
(* If jobs are sequential, then... *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ..., the service received by job j at any time t is at most 1, ... *)
Lemma service_at_most_one :
∀ t, service_at sched j t ≤ 1.
(* ..., which implies that the service receive during a interval
of length delta is at most delta. *)
Lemma cumulative_service_le_delta :
∀ t delta, service_during sched j t (t + delta) ≤ delta.
End SequentialJobs.
Section Completion.
(* Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
(* Then, after job j completes, it remains completed. *)
Lemma completion_monotonic :
∀ t t',
t ≤ t' →
completed job_cost sched j t →
completed job_cost sched j t'.
(* A completed job cannot be scheduled. *)
Lemma completed_implies_not_scheduled :
∀ t,
completed job_cost sched j t →
~~ scheduled sched j t.
(* The service received by job j in any interval is no larger than its cost. *)
Lemma cumulative_service_le_job_cost :
∀ t t',
service_during sched j t t' ≤ job_cost j.
End Completion.
Section Arrival.
(* Assume that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute sched.
(* Then, job j does not receive service at any time t prior to its arrival. *)
Lemma service_before_job_arrival_zero :
∀ t,
t < job_arrival j →
service_at sched j t = 0.
(* The same applies for the cumulative service received by job j. *)
Lemma cumulative_service_before_job_arrival_zero :
∀ t1 t2,
t2 ≤ job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
(* Hence, you can ignore the service received by a job before its arrival time. *)
Lemma service_before_arrival_eq_service_during :
∀ t0 t,
t0 ≤ job_arrival j →
\sum_(t0 ≤ t < job_arrival j + t) service_at sched j t =
\sum_(job_arrival j ≤ t < job_arrival j + t) service_at sched j t.
End Arrival.
Section Pending.
(* Assume that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute sched.
(* Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
(* Then, if job j is scheduled, it must be pending. *)
Lemma scheduled_implies_pending:
∀ t,
scheduled sched j t →
pending job_cost sched j t.
End Pending.
End JobLemmas.
(* In this section, we prove some lemmas about the list of jobs
scheduled at time t. *)
Section ScheduledJobsLemmas.
(* Consider an arrival sequence ...*)
Context {Job: eqType}.
Context {arr_seq: arrival_sequence Job}.
(* ... and some schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
Section Membership.
(* A job is in the list of scheduled jobs iff it is scheduled. *)
Lemma mem_scheduled_jobs_eq_scheduled :
∀ j t,
j \in jobs_scheduled_at sched t = scheduled sched j t.
End Membership.
Section Uniqueness.
(* Suppose that jobs are sequential. *)
Hypothesis H_sequential_jobs : sequential_jobs sched.
(* Then, the list of jobs scheduled at any time t has no duplicates. *)
Lemma scheduled_jobs_uniq :
∀ t,
uniq (jobs_scheduled_at sched t).
End Uniqueness.
Section NumberOfJobs.
(* The number of scheduled jobs is no larger than the number of cpus. *)
Lemma num_scheduled_jobs_le_num_cpus :
∀ t,
size (jobs_scheduled_at sched t) ≤ num_cpus.
End NumberOfJobs.
End ScheduledJobsLemmas.
End Schedule.
(* Specific properties of a schedule of sporadic jobs. *)
Module ScheduleOfSporadicTask.
Import SporadicTask Job.
Export Schedule.
Section ScheduledJobs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → sporadic_task.
(* Consider any schedule. *)
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Given a task tsk, ...*)
Variable tsk: sporadic_task.
(* ..., we we can state that tsk is scheduled on cpu at time t as follows. *)
Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
if (sched cpu t) is Some j then
(job_task j == tsk)
else false.
(* Likewise, we can state that tsk is scheduled on some processor. *)
Definition task_is_scheduled (t: time) :=
[∃ cpu, task_scheduled_on cpu t].
(* We also define the list of jobs scheduled during t1, t2). *)
Definition jobs_of_task_scheduled_between (t1 t2: time) :=
filter (fun (j: JobIn arr_seq) ⇒ 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_task: Job → sporadic_task.
(* Consider any schedule. *)
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Next we define intra-task parallelism, ... *)
Definition jobs_of_same_task_dont_execute_in_parallel :=
∀ (j j': JobIn arr_seq) t,
job_task j = job_task j' →
scheduled sched j t → scheduled sched j' t → j = j'.
(* ... and task precedence constraints. *)
Definition task_precedence_constraints :=
∀ (j j': JobIn arr_seq) t,
job_task j = job_task j' →
job_arrival j < job_arrival j' →
pending job_cost sched j t → ~~ scheduled sched j' t.
End ScheduleProperties.
Section BasicLemmas.
(* Assume the job cost and task are known. *)
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.
(* Then, in a valid schedule of sporadic tasks ...*)
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* ...such that jobs do not execute after completion, ...*)
Hypothesis jobs_dont_execute_after_completion :
completed_jobs_dont_execute job_cost sched.
Variable tsk: sporadic_task.
Variable j: JobIn arr_seq.
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.
(* Remember that for any job of tsk, service <= task_cost tsk *)
Lemma cumulative_service_le_task_cost :
∀ t t',
service_during sched j t t' ≤ task_cost tsk.
End BasicLemmas.
End ScheduleOfSporadicTask.
rt.model.basic.job rt.model.basic.task rt.model.basic.arrival_sequence.
(* Definition, properties and lemmas about schedules. *)
Module Schedule.
Export ArrivalSequence.
(* A processor is defined as a bounded natural number: 0, num_cpus). *)
Definition processor (num_cpus: nat) := 'I_num_cpus.
Section ScheduleDef.
Context {Job: eqType}.
(* Given the number of processors and an arrival sequence, ...*)
Variable num_cpus: nat.
Variable arr_seq: arrival_sequence Job.
(* ... we define a schedule as a mapping such that each processor
at each time contains either a job from the sequence or none. *)
Definition schedule :=
processor num_cpus → time → option (JobIn arr_seq).
End ScheduleDef.
(* Next, we define properties of jobs in a schedule. *)
Section ScheduledJobs.
Context {Job: eqType}.
(* Given an arrival sequence, ... *)
Context {arr_seq: arrival_sequence Job}.
Variable job_cost: Job → time. (* ... a job cost function, ... *)
(* ... and the number of processors, ...*)
Context {num_cpus: nat}.
(* ... we define the following properties for job j in schedule sched. *)
Variable sched: schedule num_cpus arr_seq.
Variable j: JobIn arr_seq.
(* A job j is scheduled on processor cpu at time t iff such a mapping exists. *)
Definition scheduled_on (cpu: processor num_cpus) (t: time) :=
sched cpu t == Some j.
(* A job j is scheduled at time t iff there exists a cpu where it is mapped.*)
Definition scheduled (t: time) :=
[∃ cpu, scheduled_on cpu t].
(* A processor cpu is idle at time t if it doesn't contain any jobs. *)
Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
sched cpu t = None.
(* The instantaneous service of job j at time t is the number of cpus
where it is scheduled on. Note that we use a sum to account for
parallelism if required. *)
Definition service_at (t: time) :=
\sum_(cpu < num_cpus | scheduled_on cpu t) 1.
(* The cumulative service received by job j during 0, t'). *)
Definition service (t': time) := \sum_(0 ≤ t < t') service_at t.
(* The cumulative service received by job j during t1, t2). *)
Definition service_during (t1 t2: time) := \sum_(t1 ≤ t < t2) service_at t.
(* Job j has completed at time t if it received enough service. *)
Definition completed (t: time) := service t == job_cost j.
(* Job j is pending at time t iff it has arrived but has not completed. *)
Definition pending (t: time) := has_arrived j t && ~~completed t.
(* Job j is backlogged at time t iff it is pending and not scheduled. *)
Definition backlogged (t: time) := pending t && ~~scheduled t.
(* Job j is carry-in in interval t1, t2) iff it arrives before t1 and is not complete at time t1 *)
Definition carried_in (t1: time) := arrived_before j t1 && ~~ completed t1.
(* Job j is carry-out in interval t1, t2) iff it arrives after t1 and is not complete at time t2 *)
Definition carried_out (t1 t2: time) := arrived_before j t2 && ~~ completed t2.
(* The list of scheduled jobs at time t is the concatenation of the jobs
scheduled on each processor. *)
Definition jobs_scheduled_at (t: time) :=
\cat_(cpu < num_cpus) make_sequence (sched cpu t).
(* The list of jobs scheduled during the interval t1, t2) is the the duplicate-free concatenation of the jobs scheduled at instant. *)
Definition jobs_scheduled_between (t1 t2: time) :=
undup (\cat_(t1 ≤ t < t2) jobs_scheduled_at t).
End ScheduledJobs.
(* In this section, we define properties of valid schedules. *)
Section ValidSchedules.
Context {Job: eqType}. (* Assume a job type with decidable equality, ...*)
Context {arr_seq: arrival_sequence Job}. (* ..., an arrival sequence, ...*)
Variable job_cost: Job → time. (* ... a cost function, .... *)
(* ... and a schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Next, we define whether job are sequential, ... *)
Definition sequential_jobs :=
∀ j t cpu1 cpu2,
sched cpu1 t = Some j → sched cpu2 t = Some j → cpu1 = cpu2.
(* ... whether a job can only be scheduled if it has arrived, ... *)
Definition jobs_must_arrive_to_execute :=
∀ j t, scheduled sched j t → has_arrived j t.
(* ... whether a job can be scheduled after it completes. *)
Definition completed_jobs_dont_execute :=
∀ j t, service sched j t ≤ job_cost j.
End ValidSchedules.
(* In this section, we prove some basic lemmas about a job. *)
Section JobLemmas.
(* Consider an arrival sequence, ...*)
Context {Job: eqType}.
Context {arr_seq: arrival_sequence Job}.
(* ... a job cost function, ...*)
Variable job_cost: Job → time.
(* ..., and a particular schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Next, we prove some lemmas about the service received by a job j. *)
Variable j: JobIn arr_seq.
Section Basic.
(* At any time t, job j is not scheduled iff it doesn't get service. *)
Lemma not_scheduled_no_service :
∀ t,
~~ scheduled sched j t = (service_at sched j t == 0).
(* If the cumulative service during a time interval is not zero, there
must be a time t in this interval where the service is not 0, ... *)
Lemma cumulative_service_implies_service :
∀ t1 t2,
service_during sched j t1 t2 != 0 →
∃ t,
t1 ≤ t < t2 ∧
service_at sched j t != 0.
(* ... and vice versa. *)
Lemma service_implies_cumulative_service:
∀ t t1 t2,
t1 ≤ t < t2 →
service_at sched j t != 0 →
service_during sched j t1 t2 != 0.
End Basic.
Section SequentialJobs.
(* If jobs are sequential, then... *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ..., the service received by job j at any time t is at most 1, ... *)
Lemma service_at_most_one :
∀ t, service_at sched j t ≤ 1.
(* ..., which implies that the service receive during a interval
of length delta is at most delta. *)
Lemma cumulative_service_le_delta :
∀ t delta, service_during sched j t (t + delta) ≤ delta.
End SequentialJobs.
Section Completion.
(* Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
(* Then, after job j completes, it remains completed. *)
Lemma completion_monotonic :
∀ t t',
t ≤ t' →
completed job_cost sched j t →
completed job_cost sched j t'.
(* A completed job cannot be scheduled. *)
Lemma completed_implies_not_scheduled :
∀ t,
completed job_cost sched j t →
~~ scheduled sched j t.
(* The service received by job j in any interval is no larger than its cost. *)
Lemma cumulative_service_le_job_cost :
∀ t t',
service_during sched j t t' ≤ job_cost j.
End Completion.
Section Arrival.
(* Assume that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute sched.
(* Then, job j does not receive service at any time t prior to its arrival. *)
Lemma service_before_job_arrival_zero :
∀ t,
t < job_arrival j →
service_at sched j t = 0.
(* The same applies for the cumulative service received by job j. *)
Lemma cumulative_service_before_job_arrival_zero :
∀ t1 t2,
t2 ≤ job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
(* Hence, you can ignore the service received by a job before its arrival time. *)
Lemma service_before_arrival_eq_service_during :
∀ t0 t,
t0 ≤ job_arrival j →
\sum_(t0 ≤ t < job_arrival j + t) service_at sched j t =
\sum_(job_arrival j ≤ t < job_arrival j + t) service_at sched j t.
End Arrival.
Section Pending.
(* Assume that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute sched.
(* Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
(* Then, if job j is scheduled, it must be pending. *)
Lemma scheduled_implies_pending:
∀ t,
scheduled sched j t →
pending job_cost sched j t.
End Pending.
End JobLemmas.
(* In this section, we prove some lemmas about the list of jobs
scheduled at time t. *)
Section ScheduledJobsLemmas.
(* Consider an arrival sequence ...*)
Context {Job: eqType}.
Context {arr_seq: arrival_sequence Job}.
(* ... and some schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
Section Membership.
(* A job is in the list of scheduled jobs iff it is scheduled. *)
Lemma mem_scheduled_jobs_eq_scheduled :
∀ j t,
j \in jobs_scheduled_at sched t = scheduled sched j t.
End Membership.
Section Uniqueness.
(* Suppose that jobs are sequential. *)
Hypothesis H_sequential_jobs : sequential_jobs sched.
(* Then, the list of jobs scheduled at any time t has no duplicates. *)
Lemma scheduled_jobs_uniq :
∀ t,
uniq (jobs_scheduled_at sched t).
End Uniqueness.
Section NumberOfJobs.
(* The number of scheduled jobs is no larger than the number of cpus. *)
Lemma num_scheduled_jobs_le_num_cpus :
∀ t,
size (jobs_scheduled_at sched t) ≤ num_cpus.
End NumberOfJobs.
End ScheduledJobsLemmas.
End Schedule.
(* Specific properties of a schedule of sporadic jobs. *)
Module ScheduleOfSporadicTask.
Import SporadicTask Job.
Export Schedule.
Section ScheduledJobs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → sporadic_task.
(* Consider any schedule. *)
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Given a task tsk, ...*)
Variable tsk: sporadic_task.
(* ..., we we can state that tsk is scheduled on cpu at time t as follows. *)
Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
if (sched cpu t) is Some j then
(job_task j == tsk)
else false.
(* Likewise, we can state that tsk is scheduled on some processor. *)
Definition task_is_scheduled (t: time) :=
[∃ cpu, task_scheduled_on cpu t].
(* We also define the list of jobs scheduled during t1, t2). *)
Definition jobs_of_task_scheduled_between (t1 t2: time) :=
filter (fun (j: JobIn arr_seq) ⇒ 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_task: Job → sporadic_task.
(* Consider any schedule. *)
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Next we define intra-task parallelism, ... *)
Definition jobs_of_same_task_dont_execute_in_parallel :=
∀ (j j': JobIn arr_seq) t,
job_task j = job_task j' →
scheduled sched j t → scheduled sched j' t → j = j'.
(* ... and task precedence constraints. *)
Definition task_precedence_constraints :=
∀ (j j': JobIn arr_seq) t,
job_task j = job_task j' →
job_arrival j < job_arrival j' →
pending job_cost sched j t → ~~ scheduled sched j' t.
End ScheduleProperties.
Section BasicLemmas.
(* Assume the job cost and task are known. *)
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.
(* Then, in a valid schedule of sporadic tasks ...*)
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* ...such that jobs do not execute after completion, ...*)
Hypothesis jobs_dont_execute_after_completion :
completed_jobs_dont_execute job_cost sched.
Variable tsk: sporadic_task.
Variable j: JobIn arr_seq.
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.
(* Remember that for any job of tsk, service <= task_cost tsk *)
Lemma cumulative_service_le_task_cost :
∀ t t',
service_during sched j t t' ≤ task_cost tsk.
End BasicLemmas.
End ScheduleOfSporadicTask.