add proof of equivalence of EDF definitions

This commit connects the two ways with which one can specify that a
schedule is an EDF schedule in PROSA: the `EDF_schedule` predicate
and the `respects_policy_at_preemption_point` with the EDF priority
policy predicate. We connect these two definitions by showing that
they're equivalent. We then restate the optimality proof of EDF
schedules using the proven equivalence.

analysis/facts/behavior/arrivals.v

@@ -93,6 +93,19 @@ Section Arrived.
     now apply ready_implies_arrived.
   Qed.
 
+  (** Similarly, since backlogged jobs are by definition pending, any
+      backlogged job must be incomplete. *)
+  Lemma backlogged_implies_incomplete:
+    forall j t,
+      backlogged sched j t -> ~~ completed_by sched j t.
+  Proof.
+    move=> j t BACK.
+    have suff: pending sched j t.
+    - by move /andP => [_ INCOMP].
+    - apply; move: BACK => /andP [READY _].
+      by apply any_ready_job_is_pending.
+  Qed.
+
 End Arrived.
 
 (** In this section, we establish useful facts about arrival sequence prefixes. *)

analysis/facts/behavior/completion.v

 Require Export prosa.analysis.facts.behavior.service.
 Require Export prosa.analysis.facts.behavior.arrivals.
 Require Export prosa.analysis.definitions.schedule_prefix.
+Require Export prosa.analysis.definitions.job_properties.
 
 (** * Completion *)
 
 (** In this file, we establish basic facts about job completions. *)
 Section CompletionFacts.
-  
+
   (** Consider any job type,...*)
   Context {Job: JobType}.
   Context `{JobCost Job}.
@@ -18,10 +19,10 @@ Section CompletionFacts.
   (** ...and a given schedule. *)
   Variable sched: schedule PState.
 
-  (** Let j be any job that is to be scheduled. *)
+  (** Let [j] be any job that is to be scheduled. *)
   Variable j: Job.
 
-  (** We prove that after job j completes, it remains completed. *)
+  (** We prove that after job [j] completes, it remains completed. *)
   Lemma completion_monotonic:
     forall t t',
       t <= t' ->
@@ -33,6 +34,19 @@ Section CompletionFacts.
       by apply service_monotonic.
   Qed.
 
+  (** We prove that if [j] is not completed by [t'], then it's also not
+      completed by any earlier instant. *)
+  Lemma incompletion_monotonic:
+    forall t t',
+      t <= t' ->
+      ~~ completed_by sched j t' ->
+      ~~ completed_by sched j t.
+  Proof.
+    move => t t' LE.
+    apply contra.
+    by apply completion_monotonic.
+  Qed.
+
   (** We observe that being incomplete is the same as not having received
      sufficient service yet... *)
   Lemma less_service_than_cost_is_incomplete:
@@ -52,6 +66,19 @@ Section CompletionFacts.
     move=> t. by split; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //.
   Qed.
 
+  (** Trivially, it follows that an incomplete job has a positive cost. *)
+  Corollary incomplete_implies_positive_cost:
+    forall t,
+      ~~ completed_by sched j t ->
+      job_cost_positive j.
+  Proof.
+    move=> t INCOMP.
+    apply: (ltn_leq_trans _);
+      last by apply leq_subr.
+    apply incomplete_is_positive_remaining_cost.
+    exact INCOMP.
+  Qed.
+
   (** Assume that completed jobs do not execute. *)
   Hypothesis H_completed_jobs:
     completed_jobs_dont_execute sched.

analysis/facts/behavior/deadlines.v

@@ -5,7 +5,7 @@ Require Export prosa.analysis.facts.behavior.completion.
 (** In this file, we observe basic properties of the behavioral job
     model w.r.t. deadlines. *)
 Section DeadlineFacts.
-  
+
   (** Consider any given type of jobs with costs and deadlines... *)
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
 
@@ -13,8 +13,51 @@ Section DeadlineFacts.
   Context {PState: eqType}.
   Context `{ProcessorState Job PState}.
 
-  (** We begin with schedules / processor models in which scheduled jobs
-    always receive service. *)
+  (** First, we derive two properties from the fact that a job is incomplete at
+      some point in time. *)
+  Section Incompletion.
+
+    (** Consider any given schedule. *)
+    Variable sched: schedule PState.
+
+    (** Trivially, a job that both meets its deadline and is incomplete at a
+        time [t] must have a deadline later than [t]. *)
+    Lemma incomplete_implies_later_deadline:
+      forall j t,
+        job_meets_deadline sched j ->
+        ~~ completed_by sched j t ->
+        t < job_deadline j.
+    Proof.
+      move=> j t MET INCOMP.
+      apply contraT; rewrite -leqNgt => PAST_DL.
+      have DL_MISS: ~~ completed_by sched j (job_deadline j)
+        by apply incompletion_monotonic with (t' := t) => //.
+      by move: DL_MISS => /negP.
+    Qed.
+
+    (** Furthermore, a job that both meets its deadline and is incomplete at a
+        time [t] must be scheduled at some point between [t] and its
+        deadline. *)
+    Lemma incomplete_implies_scheduled_later:
+      forall j t,
+        job_meets_deadline sched j ->
+        ~~ completed_by sched j t ->
+        exists t', t <= t' < job_deadline j /\ scheduled_at sched j t'.
+    Proof.
+      move=> j t MET INCOMP.
+      apply: cumulative_service_implies_scheduled.
+      rewrite -(ltn_add2l (service sched j t)) addn0.
+      rewrite service_cat;
+        last by (apply ltnW; apply incomplete_implies_later_deadline).
+      apply ltn_leq_trans with (n := job_cost j);
+        first by rewrite less_service_than_cost_is_incomplete.
+      by apply MET.
+    Qed.
+
+  End Incompletion.
+
+  (** Next, we look at schedules / processor models in which scheduled jobs
+      always receive service. *)
   Section IdealProgressSchedules.
 
     (** Consider a given reference schedule... *)
@@ -26,26 +69,19 @@ Section DeadlineFacts.
     (** ...and scheduled jobs always receive service. *)
     Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
 
-    (** We observe that, if a job is known to meet its deadline, then
-       its deadline must be later than any point at which it is
-       scheduled. That is, if a job that meets its deadline is
-       scheduled at time t, we may conclude that its deadline is at a
-       time later than t. *)
+    (** We observe that if a job meets its deadline and is scheduled at time
+        [t], then then its deadline is at a time later than t. *)
     Lemma scheduled_at_implies_later_deadline:
       forall j t,
         job_meets_deadline sched j ->
         scheduled_at sched j t ->
         t < job_deadline j.
     Proof.
-      move=> j t.
-      rewrite /job_meets_deadline => COMP SCHED.
-      case: (boolP (t < job_deadline j)) => //.
-      rewrite -leqNgt => AFTER_DL.
-      apply completion_monotonic with (t' := t) in COMP => //.
-      apply scheduled_implies_not_completed in SCHED => //.
-      move/negP in SCHED. contradiction.
+      move=> j t MET SCHED_AT.
+      apply (incomplete_implies_later_deadline sched) => //.
+      by apply scheduled_implies_not_completed.
     Qed.
-    
+
   End IdealProgressSchedules.
 
   (** In the following section, we observe that it is sufficient to

analysis/facts/edf_definitions.v

+Require Export prosa.analysis.facts.model.ideal_schedule.
+Require Export prosa.analysis.facts.behavior.deadlines.
+Require Export prosa.analysis.definitions.schedulability.
+Require Export prosa.model.priority.edf.
+Require Export prosa.model.schedule.edf.
+Require Export prosa.model.schedule.priority_driven.
+
+(** * Equivalence of EDF Definitions *)
+
+(** Recall that we have defined "EDF schedules" in two ways.
+
+    The generic way to define an EDF schedule is by using the EDF priority
+    policy defined in [model.priority.edf] and the general notion of
+    priority-compliant schedules defined in [model.schedule.priority_driven].
+
+    Another, more straight-forward way to define an EDF schedule is the standalone
+    definition given in [model.schedule.edf], which is less general but simpler
+    and used in the EDF optimality proof.
+
+    In this file, we show that both definitions are equivalent assuming:
+
+    (1) ideal uniprocessor schedules, ... *)
+Require Import prosa.model.processor.ideal.
+
+(** ... (2) the classic Liu & Layland model of readiness without jitter and
+    without self-suspensions, where pending jobs are always ready, and ... *)
+Require Import prosa.model.readiness.basic.
+
+(** ... (3) that jobs are fully preemptive. *)
+Require Import prosa.model.preemption.fully_preemptive.
+
+Section Equivalence.
+
+  (** For any given type of jobs, each characterized by an arrival time,
+      an execution cost, and an absolute deadline, ... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (** ...consider a given valid job arrival sequence ... *)
+  Variable arr_seq: arrival_sequence Job.
+  Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
+
+  (** ...and a corresponding schedule. *)
+  Variable sched : schedule (ideal.processor_state Job).
+
+  (** Suppose jobs don't execute after their completion, ... *)
+  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
+
+  (** ...all jobs come from the arrival sequence [arr_seq], ...*)
+  Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ...and jobs from [arr_seq] don't miss their deadlines. *)
+  Hypothesis H_no_deadline_misses: all_deadlines_of_arrivals_met arr_seq sched.
+
+  (** We first show that a schedule that satisfies the standalone
+      [EDF_schedule] predicate is also compliant with the generic notion of EDF
+      policy defined in Prosa, namely the [respects_policy_at_preemption_point]
+      predicate. *)
+  Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
+    EDF_schedule sched ->
+    respects_policy_at_preemption_point arr_seq sched.
+  Proof.
+    move=> EDF j' j t ARR PREEMPTION BL SCHED.
+    have suff: exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t'.
+    { move=> [t' [/andP [LE _] SCHED']].
+      apply: (EDF t); [done | exact LE | exact SCHED' |].
+      by apply: (backlogged_implies_arrived sched j' t). }
+    apply; apply: incomplete_implies_scheduled_later;
+      first by apply: H_no_deadline_misses => //.
+    by apply: (backlogged_implies_incomplete sched j' t).
+  Qed.
+
+  (** Conversely, the reverse direction also holds: a schedule that satisfies
+      the [respects_policy_at_preemption_point] predicate is also an EDF
+      schedule in the sense of [EDF_schedule]. *)
+  Lemma respects_policy_at_preemption_point_implies_EDF_schedule :
+    respects_policy_at_preemption_point arr_seq sched ->
+    EDF_schedule sched.
+  Proof.
+    move=> H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.
+    case (boolP (j == j_hp)); first by move /eqP => EQ; subst.
+    move /neqP => NEQ.
+    exploit (H_priority_driven j j_hp t) => //.
+    { by apply (H_from_arr_seq _ _ SCHED'). }
+    { by rewrite /preemption_time; destruct (sched t). }
+    { apply /andP; split => //.
+      - apply /andP; split => //.
+        apply (incompletion_monotonic _ j _ _ LEQ).
+        apply scheduled_implies_not_completed => //.
+        by apply ideal_proc_model_ensures_ideal_progress.
+      - apply /negP; move => SCHED''.
+        by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }
+  Qed.
+
+  (** From the two preceding lemmas, it follows immediately that the two EDF
+      definitions are indeed equivalent, which we note with the following
+      corollary. *)
+  Corollary EDF_schedule_equiv:
+    EDF_schedule sched <-> respects_policy_at_preemption_point arr_seq sched.
+  Proof.
+    split.
+    - by apply EDF_schedule_implies_respects_policy_at_preemption_point.
+    - by apply respects_policy_at_preemption_point_implies_EDF_schedule.
+  Qed.
+
+End Equivalence.

results/edf/optimality.v

 Require Export prosa.analysis.facts.transform.edf_opt.
 Require Export prosa.analysis.facts.transform.edf_wc.
+Require Export prosa.analysis.facts.edf_definitions.
 
 (** * Optimality of EDF on Ideal Uniprocessors *)
 
@@ -8,11 +9,15 @@ Require Export prosa.analysis.facts.transform.edf_wc.
     schedule), then there is also an (ideal) EDF schedule in which all
     deadlines are met. *)
 
-(** The following results assume ideal uniprocessor schedules... *)
+(** The following results assume ideal uniprocessor schedules,... *)
 Require prosa.model.processor.ideal.
-(** ... and the basic (i.e., Liu & Layland) readiness model under which any
-    pending job is always ready. *)
+(** ... the basic (i.e., Liu & Layland) readiness model under which any
+    pending job is always ready, ... *)
 Require prosa.model.readiness.basic.
+(** ... the EDF priority policy, ... *)
+Require prosa.model.priority.edf.
+(** ...and a fully preemptive job model. *)
+Require prosa.model.preemption.fully_preemptive.
 
 (** ** Optimality Theorem *)
 
@@ -26,7 +31,7 @@ Section Optimality.
   Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
 
   (** We observe that EDF is optimal in the sense that, if there exists
-     any schedule in which all jobs of arr_seq meet their deadline,
+     any schedule in which all jobs of [arr_seq] meet their deadline,
      then there also exists an EDF schedule in which all deadlines are
      met. *)
   Theorem EDF_optimality:
@@ -87,6 +92,33 @@ Section Optimality.
       [EDF_WC_optimality]. We nonetheless have two separate proofs for historic
       reasons as [EDF_optimality] predates [EDF_WC_optimality] (in Prosa). *)
 
+  (** Finally, we state the optimality theorem also in terms of a
+      policy-compliant schedule, which a more generic notion used in Prosa for
+      scheduling policies (rather than the simpler, but ad-hoc
+      [EDF_schedule] predicate used above).
+
+      Given that we're considering the EDF priority policy and a fully
+      preemptive job model, satisfying the [EDF_schedule] predicate is
+      equivalent to satisfying the [respects_policy_at_preemption_point]
+      w.r.t. to the EDF policy predicate. The optimality of priority-compliant
+      schedules that are work-conserving follows hence directly from the above
+      [EDF_WC_optimality] theorem. *)
+  Corollary EDF_priority_compliant_WC_optimality:
+    (exists any_sched : schedule (ideal.processor_state Job),
+        valid_schedule any_sched arr_seq /\
+        all_deadlines_of_arrivals_met arr_seq any_sched) ->
+    exists priority_compliant_sched : schedule (ideal.processor_state Job),
+        valid_schedule priority_compliant_sched arr_seq /\
+        all_deadlines_of_arrivals_met arr_seq priority_compliant_sched /\
+        work_conserving arr_seq priority_compliant_sched /\
+        respects_policy_at_preemption_point arr_seq priority_compliant_sched.
+  Proof.
+    move /EDF_WC_optimality => [edf_sched [[ARR READY] [DL_MET [WC EDF]]]].
+    exists edf_sched.
+    apply (EDF_schedule_equiv arr_seq _) in EDF => //.
+    now apply (completed_jobs_are_not_ready edf_sched READY).
+  Qed.
+
 End Optimality.
 
 (** ** Weak Optimality Theorem *)

scripts/wordlist.pws

@@ -60,4 +60,7 @@ RTCT
 superadditivity
 superadditive
 subadditivity
-subadditive
\ No newline at end of file
+subadditive
+ad
+hoc
+