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
Require Import
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 \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 \in ts schedulable tsk.

    End Schedulability.

  End PartitionedAsUniprocessor.

End PartitionSchedulability.