Library prosa.classic.model.schedule.partitioned.schedulability
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.partitioned.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require prosa.classic.model.schedule.uni.schedule.
Module PartitionSchedulability.
Module uni_sched := prosa.classic.model.schedule.uni.schedulability.Schedulability.
Import ArrivalSequence Partitioned Schedule Schedulability.
Section PartitionedAsUniprocessor.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → Task.
(* Consider any job arrival sequence that is to be scheduled. *)
Variable arr_seq: arrival_sequence Job.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
(* Assume that all jobs in the arrival sequence come from a task set ts. *)
Variable ts: list Task.
Hypothesis H_all_jobs_from_ts:
∀ j, arrives_in arr_seq j → job_task j \in ts.
(* Also assume that every task is assigned to a processor, ... *)
Variable assigned_cpu: Task → processor num_cpus.
(* ...forming a partitioned schedule. *)
Hypothesis H_partitioned: partitioned_schedule job_task sched ts assigned_cpu.
(* Next, we related total service with per-processor service received by each job. *)
Section SameService.
(* Consider the partition where each job is assigned to. *)
Let partition_of j := assigned_cpu (job_task j).
(* Let j be any job. *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
(* We prove that the service received by job j (on the multiprocessor)
is the same as the service received by job j in its partition. *)
Lemma same_per_processor_service :
∀ t1 t2,
service_during sched j t1 t2 =
uni.service_during (sched (partition_of j)) j t1 t2.
End SameService.
Section Schedulability.
(* Recall the definitions of schedulability on a uniprocessor and on
a multiprocessor. *)
Let schedulable_on tsk cpu :=
uni_sched.task_misses_no_deadline job_arrival job_cost job_deadline job_task
arr_seq (sched cpu) tsk.
Let schedulable :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
(* Here we prove that if every task is schedulable in their assigned processors, ...*)
Hypothesis H_locally_schedulable:
∀ tsk,
tsk \in ts → schedulable_on tsk (assigned_cpu tsk).
(* ...then every task is schedulable at the level of the multiprocessor system. *)
Lemma schedulable_at_system_level:
∀ tsk,
tsk \in ts → schedulable tsk.
End Schedulability.
End PartitionedAsUniprocessor.
End PartitionSchedulability.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.partitioned.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require prosa.classic.model.schedule.uni.schedule.
Module PartitionSchedulability.
Module uni_sched := prosa.classic.model.schedule.uni.schedulability.Schedulability.
Import ArrivalSequence Partitioned Schedule Schedulability.
Section PartitionedAsUniprocessor.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → Task.
(* Consider any job arrival sequence that is to be scheduled. *)
Variable arr_seq: arrival_sequence Job.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
(* Assume that all jobs in the arrival sequence come from a task set ts. *)
Variable ts: list Task.
Hypothesis H_all_jobs_from_ts:
∀ j, arrives_in arr_seq j → job_task j \in ts.
(* Also assume that every task is assigned to a processor, ... *)
Variable assigned_cpu: Task → processor num_cpus.
(* ...forming a partitioned schedule. *)
Hypothesis H_partitioned: partitioned_schedule job_task sched ts assigned_cpu.
(* Next, we related total service with per-processor service received by each job. *)
Section SameService.
(* Consider the partition where each job is assigned to. *)
Let partition_of j := assigned_cpu (job_task j).
(* Let j be any job. *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
(* We prove that the service received by job j (on the multiprocessor)
is the same as the service received by job j in its partition. *)
Lemma same_per_processor_service :
∀ t1 t2,
service_during sched j t1 t2 =
uni.service_during (sched (partition_of j)) j t1 t2.
End SameService.
Section Schedulability.
(* Recall the definitions of schedulability on a uniprocessor and on
a multiprocessor. *)
Let schedulable_on tsk cpu :=
uni_sched.task_misses_no_deadline job_arrival job_cost job_deadline job_task
arr_seq (sched cpu) tsk.
Let schedulable :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
(* Here we prove that if every task is schedulable in their assigned processors, ...*)
Hypothesis H_locally_schedulable:
∀ tsk,
tsk \in ts → schedulable_on tsk (assigned_cpu tsk).
(* ...then every task is schedulable at the level of the multiprocessor system. *)
Lemma schedulable_at_system_level:
∀ tsk,
tsk \in ts → schedulable tsk.
End Schedulability.
End PartitionedAsUniprocessor.
End PartitionSchedulability.