Library prosa.classic.model.schedule.apa.affinity

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module Affinity.

  Import ArrivalSequence ScheduleOfSporadicTask.

  Section AffinityDefs.

    Variable sporadic_task: eqType.

    Variable num_cpus: nat.

    Definition affinity := {set (processor num_cpus)}.

    Definition task_affinity := sporadic_task → affinity.

  End AffinityDefs.

  Section Properties.

    Context {sporadic_task: eqType}.
    Context {num_cpus: nat}.

    Section JobProperties.

      Variable alpha: task_affinity sporadic_task num_cpus.

      Variable tsk: sporadic_task.

      Variable cpu: processor num_cpus.

      Definition can_execute_on := cpu \in alpha tsk.

    End JobProperties.

    Section ScheduleProperties.

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

      Variable sched: schedule Job num_cpus.

      Variable alpha: affinity num_cpus.

      Definition task_scheduled_on_affinity (tsk: sporadic_task) (t: time) :=
        [∃ cpu, (cpu \in alpha) && task_scheduled_on job_task sched tsk cpu t].

    End ScheduleProperties.

    Section Subset.

      Variable alpha' alpha: affinity num_cpus.

      Definition is_subaffinity := {subset alpha' ≤ alpha}.

      Section Lemmas.

        Hypothesis H_subaffinity: is_subaffinity.

        Lemma leq_subaffinity : #|alpha'| ≤ #|alpha|.

      End Lemmas.

    End Subset.

    Section IntersectingAffinities.

      Definition affinity_intersects (alpha alpha': affinity num_cpus) :=
        [∃ cpu, (cpu \in alpha) && (cpu \in alpha')].

    End IntersectingAffinities.

  End Properties.

End Affinity.