From ec51a2dc23adc013fc68d5fab2bfd90eea5eb97c Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Fri, 25 Sep 2020 13:08:21 +0200
Subject: [PATCH] note basic `task_schedule` properties
---
analysis/facts/model/task_schedule.v | 50 ++++++++++++++++++++++++++++
1 file changed, 50 insertions(+)
create mode 100644 analysis/facts/model/task_schedule.v
diff --git a/analysis/facts/model/task_schedule.v b/analysis/facts/model/task_schedule.v
new file mode 100644
index 000000000..1f7641992
--- /dev/null
+++ b/analysis/facts/model/task_schedule.v
@@ -0,0 +1,50 @@
+Require Export prosa.model.task.concept.
+Require Export prosa.analysis.definitions.task_schedule.
+Require Export prosa.analysis.facts.model.ideal_schedule.
+
+(** In this file we provide basic properties related to schedule of a task. *)
+Section TaskSchedule.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** Let [sched] be any ideal uni-processor schedule. *)
+ Variable sched : schedule (ideal.processor_state Job).
+
+ (** Let [tsk] be any task. *)
+ Variable tsk : Task.
+
+ (** We show that if a job of task [tsk] is scheduled at time [t],
+ then task [tsk] is scheduled at time [t]. *)
+ Lemma job_of_task_scheduled_implies_task_scheduled :
+ forall j t,
+ job_of_task tsk j ->
+ scheduled_at sched j t ->
+ task_scheduled_at sched tsk t.
+ Proof.
+ intros ? ? TSK SCHED.
+ unfold task_scheduled_at.
+ by move: SCHED; rewrite scheduled_at_def => /eqP ->.
+ Qed.
+
+ (** And vice versa, if no job of task [tsk] is scheduled at time
+ [t], then task [tsk] is not scheduled at time [t]. *)
+ Lemma job_of_task_scheduled_implies_task_scheduled':
+ forall j t,
+ ~~ job_of_task tsk j ->
+ scheduled_at sched j t ->
+ ~~ task_scheduled_at sched tsk t.
+ Proof.
+ move => j t /negP TSK SCHED; apply /negP => TSCHED; apply: TSK.
+ move: SCHED; rewrite scheduled_at_def => /eqP SCHED.
+ by move: TSCHED; rewrite /task_scheduled_at SCHED.
+ Qed.
+
+End TaskSchedule.
--
GitLab