From 3fe76668f6ea50d781041e4bc4c42a1c391b5771 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 18 Jul 2019 15:23:41 +0200
Subject: [PATCH] add two notions of "all deadlines met" independent of tasks

---
 restructuring/analysis/schedulability.v | 60 +++++++++++++++++++++++++
 1 file changed, 60 insertions(+)

diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 92fea8c..5bb6e8b 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -106,3 +106,63 @@ Section Schedulability.
   Qed.
 
 End Schedulability.
+
+
+(** We further define two notions of "all deadlines met" that do not
+    depend on a task abstraction: one w.r.t. all scheduled jobs in a
+    given schedule and one w.r.t. all jobs that arrive in a given
+    arrival sequence. *)
+Section AllDeadlinesMet.
+
+  (* Consider any given type of jobs... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (* ... any given type of processor states. *)
+  Context {PState: eqType}.
+  Context `{ProcessorState Job PState}.
+
+  (* We say that all deadlines are met if every job scheduled at some
+     point in the schedule meets its deadline. Note that this is a
+     relatively weak definition since an "empty" schedule that is idle
+     at all times trivially satisfies it (since the definition does
+     not require any kind of work conservation). *)
+  Definition all_deadlines_met (sched: schedule PState) :=
+    forall j t,
+      scheduled_at sched j t ->
+      job_meets_deadline sched j.
+
+  (* To augment the preceding definition, we also define an alternate
+     notion of "all deadlines met" based on all jobs included in a
+     given arrival sequence.  *)
+  Section DeadlinesOfArrivals.
+
+    (* Given an arbitrary job arrival sequence ... *)
+    Variable arr_seq: arrival_sequence Job.  
+
+    (* ... we say that all arrivals meet their deadline if every job
+       that arrives at some point in time meets its deadline. Note
+       that this definition does not preclude the existence of jobs in
+       a schedule that miss their deadline (e.g., if they stem from
+       another arrival sequence). *)
+    Definition all_deadlines_of_arrivals_met (sched: schedule PState) :=
+      forall j,
+        arrives_in arr_seq j ->
+        job_meets_deadline sched j.
+
+  End DeadlinesOfArrivals.
+
+  (* We observe that the latter definition, assuming a schedule in
+     which all jobs come from the arrival sequence, implies the former
+     definition. *)
+  Lemma all_deadlines_met_in_valid_schedule:
+    forall arr_seq sched,
+      jobs_come_from_arrival_sequence sched arr_seq ->
+      all_deadlines_of_arrivals_met arr_seq sched ->
+      all_deadlines_met sched.
+  Proof.
+    move=> arr_seq sched FROM_ARR DL_ARR_MET j t SCHED.
+    apply DL_ARR_MET.
+    by apply (FROM_ARR _ t).
+  Qed.
+    
+End AllDeadlinesMet.
-- 
2.26.2