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|.
Proof.
assert (UNIQ: uniq (alpha)). by destruct (alpha).
assert (UNIQ': uniq (alpha')). by destruct (alpha').
move: (UNIQ) (UNIQ') ⇒ /card_uniqP → /card_uniqP →.
by apply uniq_leq_size.
Qed.
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.
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|.
Proof.
assert (UNIQ: uniq (alpha)). by destruct (alpha).
assert (UNIQ': uniq (alpha')). by destruct (alpha').
move: (UNIQ) (UNIQ') ⇒ /card_uniqP → /card_uniqP →.
by apply uniq_leq_size.
Qed.
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.