Library prosa.classic.model.schedule.partitioned.schedule

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time 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 prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module Partitioned.

  Module uni := prosa.classic.model.schedule.uni.schedule.UniprocessorSchedule.
  Module uni_sched := prosa.classic.model.schedule.uni.schedulability.Schedulability.
  Import SporadicTaskset Schedule Schedulability.
  Export Time.

  Section PartitionedDefs.

    Context {Task: eqType}.
    Context {Job: eqType}.
    Variable job_task: Job → Task.

    Variable arr_seq: arrival_sequence Job.

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


    Section NoJobMigration.


      Variable j: Job.

      Definition never_migrates :=
        
        ∀ t,
          
        ∀ cpu,
          
          scheduled_on sched j cpu t →
          
          ∀ t',
            
            ∀ cpu',
              scheduled_on sched j cpu' t' → cpu' = cpu.

      Variable assigned_cpu : processor num_cpus.
      Definition job_local_to_processor :=
        ∀ t, ∀ cpu,
          scheduled_on sched j cpu t → cpu = assigned_cpu.

    End NoJobMigration.


    Section NoTaskMigration.

      Variable tsk: Task.

      Variable assigned_cpu : processor num_cpus.

      Definition task_local_to_processor :=
        ∀ j,
          job_task j = tsk →
          job_local_to_processor j assigned_cpu.

    End NoTaskMigration.

    Section PartitionedSchedule.

      Variable ts: list Task.

      Variable assigned_cpu: Task → processor num_cpus.

      Definition partitioned_schedule :=
        ∀ tsk,
          tsk \in ts →
          task_local_to_processor tsk (assigned_cpu tsk).

    End PartitionedSchedule.

  End PartitionedDefs.

  Section SimpleProperties.

    Context {Job: eqType}.

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

    Section NoJobMigrationLemmas.

      Variable j: Job.

      Lemma local_jobs_dont_migrate:
        ∀ cpu,
          job_local_to_processor sched j cpu → never_migrates sched j.
      Proof.
        rewrite /job_local_to_processor /never_migrates
             ⇒ cpu H_is_local t cpu' H_sched_at_t t' cpu'' H_sched_at_t'.
        apply H_is_local in H_sched_at_t.
        apply H_is_local in H_sched_at_t'.
        by rewrite H_sched_at_t H_sched_at_t'.
      Qed.

    End NoJobMigrationLemmas.

  End SimpleProperties.

End Partitioned.