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.

    Variable arr_seq: arrival_sequence Job.
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    Variable ts: list Task.
    Hypothesis H_all_jobs_from_ts:
      ∀ j, arrives_in arr_seq j → job_task j \in ts.

    Variable assigned_cpu: Task → processor num_cpus.

    Hypothesis H_partitioned: partitioned_schedule job_task sched ts assigned_cpu.

    Section SameService.

      Let partition_of j := assigned_cpu (job_task j).

      Variable j: Job.
      Hypothesis H_j_arrives: arrives_in arr_seq j.

      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.

      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.

      Hypothesis H_locally_schedulable:
        ∀ tsk,
          tsk \in ts → schedulable_on tsk (assigned_cpu tsk).

      Lemma schedulable_at_system_level:
        ∀ tsk,
          tsk \in ts → schedulable tsk.

    End Schedulability.

  End PartitionedAsUniprocessor.

End PartitionSchedulability.