Library transfer.transfer_schedulability

Transfer Schedulability for Ideal Uniprocessors

In this development, we define the exact transfer schedulability criterion and prove two sufficient and one necessary conditions.

Transfer schedulability is a concept that allows mimicking the behavior of some reference schedule in an online schedule such that no job finishes later in the online schedule than in the reference schedule.

In this file, we are concerned solely with the condition under which such a schedulability transfer is guaranteed. We do not concern ourselves with any particular mechanism for accomplishing such a transfer at runtime.

The following line imports the SSReflect tactics language that we use to construct proofs.

From mathcomp Require Import all_ssreflect all_algebra.

We build on the open-source Prosa library for mechanized schedulability analysis, from which we reuse central modeling definitions and many auxiliary lemmas.

Require Export prosa.analysis.facts.model.service_of_jobs.
Require Export prosa.analysis.definitions.schedulability.

In particular, we restrict our focus exclusively to ideal uniprocessor schedules in the following.

Require Export prosa.analysis.facts.model.ideal.schedule.

System Model

We are now ready to introduce the system model that we analyze.

Section TransferSchedulability.

We consider jobs characterized by arrival times and deadlines. No assumptions are made on how jobs relate (or whether they do so at all) and on how deadlines relate to arrival times. (We do not consider any "task" concept in this file.)

Context {Job : JobType} `{JobArrival Job} `{JobDeadline Job}.

As already mentioned, we consider ideal uniprocessor schedules. To this end, let us recall Prosa's existing definition of this common assumption. (For convenience and to match Prosa convention, we will refer to the ideal uniprocessor state simply as PState.)

#[local] Existing Instance ideal.processor_state.
Let PState := ideal.processor_state Job.

Next, we introduce the two key elements of the model. First, a reference schedule called ref_sched in the following. This is the schedule that we assume is being emulated.

Variable ref_sched : schedule PState.

Second, assume we are given an online schedule called online_sched, which is the schedule to which schedulability is supposed to be transferred to.

Variable online_sched : schedule PState.

We need to consider two different job costs: the one planned for in the reference schedule, called ref_job_cost, and the one actually exhibited in the online schedule, called online_job_cost.

Variable ref_job_cost online_job_cost : JobCost Job.

When we say that a job is complete in the reference schedule, it is a statement w.r.t. the reference cost job_cost_ref. Conversely, when we say that a job is complete in the online schedule, it is a statement w.r.t. the online cost job_cost_online. For ease of reference, we define respective local abbreviations.

Syntax hint: The "@" notation allows us to explicitly specify parameters that are usually implicitly inferred, such as the job-cost parameter in our case here.

Let ref_completed_by := (@completed_by _ _ ref_sched ref_job_cost).
Let online_completed_by := (@completed_by _ _ online_sched online_job_cost).

Well-Formedness of the Schedules

In order to prove the desired results, we need to place some mild assumptions on the reference and online schedules. The following hypotheses express these commonsense well-formedness requirements.

First of all, we assume that the (possibly infinite) set of jobs to be scheduled is characterized by the arrival sequence, called arr_seq, which is a standard modeling element in Prosa.

Note that arr_seq is a section variable and hence implicitly forall-quantified. The results established in this file thus hold w.r.t. to any arrival sequence (in which each job arrives at most once).

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

Next, we require that the reference schedule indeed contains only jobs that arrive in the system.

Hypothesis H_jobs_arr_ref : jobs_come_from_arrival_sequence ref_sched arr_seq.

Additionally, we require the reference schedule to be well-formed: any job that executes must have arrived and not yet complete.

Hypothesis H_jobs_must_arrive_ref : jobs_must_arrive_to_execute ref_sched.
Hypothesis H_jobs_exec_ref : (@completed_jobs_dont_execute _ _ ref_sched ref_job_cost).

Finally, we also require that completed jobs don't execute past their completion in the online schedule.

Hypothesis H_jobs_exec_on : (@completed_jobs_dont_execute _ _ online_sched online_job_cost).

Definition of "Schedulability Transfer"

By "transfer schedulability", we refer to the property that no job finishes any later in the online schedule than in the reference schedule. That is, if a job j is finished at a given time t in the reference schedule, then the same job is also finished at time t in the online schedule.

  Definition schedulability_transferred :=
    ∀ j t,
      ref_completed_by j t → online_completed_by j t.

As a corollary, we next note that this notion trivially extends to deadlines. As before, we need to be careful to be referring to the appropriate job-cost parameter.

Let ref_job_meets_deadline := (@job_meets_deadline _ _ ref_sched ref_job_cost _).
Let online_job_meets_deadline := (@job_meets_deadline _ _ online_sched online_job_cost _).

We can now re-state the schedulability-transfer property in terms of job deadlines: Assuming that the schedulability_transferred property holds, a job meets its deadline in the online schedule if it meets its deadline in the reference schedule.

  Corollary deadlines_met :
    schedulability_transferred →
    (∀ j, ref_job_meets_deadline j → online_job_meets_deadline j ).
  Proof. move⇒ TRANS j MET; by apply: TRANS. Qed.

Auxiliary Lemmas to be Submitted to Prosa

As part of completing the proofs below, we accumulated some general auxiliary lemmas about basic facts that we found to be currently missing in Prosa. Those are given in the following, but are not specific to transfer schedulability as a concept.

After the paper has been published, we will offer these lemmas to the Prosa maintainers for upstreaming.

The casual reader may safely ignore these lemmas.

An incomplete job that is not scheduled at time t remains incomplete.

  Lemma not_scheduled_remains_incomplete {jc : JobCost Job} :
    ∀ sched j t,
      ~~ completed_by sched j t →
      ~~ scheduled_at sched j t →
      (~~ completed_by sched j t .+1 ).
  Proof.
    move⇒ sched j t + NSCHED.
    rewrite /completed_by/service -service_during_last_plus_before //.
    by rewrite not_scheduled_implies_no_service // addn0.
  Qed.

On a uniprocessor, only one job is scheduled at a time. Hence, if we know one job to be scheduled, we can conclude that any other job isn't scheduled. This lemma makes Prosa's uniprocessor definition slightly more convenient to use.

  Lemma uniproc_only_one_scheduled :
    ∀ {j j' : Job},
      j != j' →
      ∀ sched t,
        scheduled_at sched j t → ~~ (scheduled_at sched j' t ).
  Proof.
    move⇒ j j' NEQ sched t SCHED.
    apply: contra_notN ⇒ [SCHED'|];
      last by apply/eqP; exact: NEQ.
    by apply: ideal_proc_model_is_a_uniprocessor_model.
  Qed.

When considering the service accumulated by bunch of jobs in an interval [t1, t2], the total amount of service can be split into the service received during [t1, t2) and the service received at the last point in time t2.

  Lemma service_of_jobs_cat_last :
    ∀ (sched : schedule PState) P js t1 t2,
      t1 ≤ t2 →
      service_of_jobs sched P js t1 t2 .+1
      = service_of_jobs sched P js t1 t2
        + service_of_jobs_at sched P js t2.
  Proof.
    move⇒ sched P js t1 t2 LEQ.
    rewrite !service_of_jobs_sum_over_time_interval.
    by rewrite big_nat_recr.
  Qed.

On a unitspeed processor (such as an ideal uniprocessor), if we know that a job in a given set is scheduled, then the total service accrued by the set of jobs at this point in time increases by one time unit.

Notation hint: uniq js is MathComp's way of stating that js is indeed a set, i.e., each element in the sequence is unique (= not repeated).

  Lemma service_of_jobs_at_scheduled :
    ∀ (sched : schedule PState) (P : pred Job) js t,
      uniq js →
      (∃ j , (j \in js ) ∧ scheduled_at sched j t ∧ P j ) →
      service_of_jobs_at sched P js t = 1.
  Proof.
    move⇒ sched P js t UNIQ [j [IN [SCHED Pj]]].
    have NSCHED: ∀ j', j' != j → service_at sched j' t = 0.
    { move⇒ j' /[1! eq_sym ] NEQ.
      rewrite -no_service_not_scheduled //.
      by apply: (uniproc_only_one_scheduled NEQ). }
    rewrite /service_of_jobs_at (bigID (fun j' ⇒ j' == j )) /=.
    have /eqP ->: \sum_(i <- js | P i && (i != j)) service_at sched i t == 0.
    { rewrite sum_nat_seq_eq0.
      apply/allP ⇒ j' IN'.
      apply/implyP ⇒ /andP[Pj' NEQ].
      by apply/eqP/NSCHED. }
    rewrite addn0.
    have ->: \sum_(i <- js | P i && (i == j)) service_at sched i t
             = \sum_(i <- [:: j] | P i && (i == j)) service_at sched i t.
    { rewrite -[LHS]big_filter -[RHS]big_filter.
      apply: congr_big ⇒ //.
      rewrite !filter_predI !filter_pred1_uniq //.
      exact: mem_head. }
    rewrite big_mkcond big_seq1 Pj eq_refl //=.
    by rewrite service_at_is_scheduled_at SCHED.
  Qed.

The amount of service accrued in an empty interval is trivially zero.

  Lemma service_of_jobs_geq :
    ∀ (sched : schedule PState) P js t1 t2,
      t1 ≥ t2 →
      service_of_jobs sched P js t1 t2 = 0.
  Proof.
    move⇒ sched P js t1 t2 LEQ.
    rewrite /service_of_jobs; apply/eqP.
    rewrite sum_nat_seq_eq0; apply/allP ⇒ j IN.
    apply/implyP ⇒ Pj.
    by apply/eqP/big_geq.
  Qed.

When considering the amount of service accrued by a set of jobs during some interval, if we know that at each point some job from the set is scheduled, then the total amount of service accrued (on a unitspeed processor) in total by the set of jobs is equal to the length of the interval.

  Lemma service_of_jobs_always_scheduled :
    ∀ (sched : schedule PState) (P : pred Job) js t1 t2,
      uniq js →
      (∀ t, t1 ≤ t < t2 → ∃ j , (j \in js ) ∧ scheduled_at sched j t ∧ P j ) →
      service_of_jobs sched P js t1 t2 = t2 - t1.
  Proof.
    move⇒ sched P js t1 t2 UNIQ SCHED.
    elim: t2 SCHED ⇒ [|t2 IH SCHED];
      first by rewrite service_of_jobs_geq; lia.
    have [LEQ|LT] := leqP t1 t2;
      last by rewrite service_of_jobs_geq; lia.
    rewrite service_of_jobs_cat_last // IH;
      last by move⇒ t /andP[LO HI]; apply: SCHED; lia.
    rewrite service_of_jobs_at_scheduled //.
    - by lia.
    - by apply: SCHED; lia.
  Qed.

Setup for the Generic Argument

We are now ready to start establishing the desired results. Since we want to prove two variants of the sufficiency condition, one for online_job_cost and one for ref_job_cost, we are abstracting in the following from the specific job-cost parameter.

Section ParametericCostBound.

Let job_cost_bound denote an upper bound on the cost of each job in online_sched. Below, we are going to instantiate job_cost_bound once as online_job_cost and once as ref_job_cost, but in theory it could be any bound in between the two extremes.

Variable job_cost_bound : JobCost Job.

We require that job_cost_bound indeed upper-bounds the online cost of any job.

    Hypothesis H_job_cost_bounded :
      ∀ j,
        online_job_cost j ≤ job_cost_bound j.

Conversely, we require that the reference cost ref_job_cost upper-bounds the job_cost_bound used in this section.

    Hypothesis H_ref_cost_dominates :
      ∀ j,
        job_cost_bound j ≤ ref_job_cost j.

As a trivial corollary, by transitivity the reference cost also bounds the online cost.

    Corollary ref_cost_bounds_online_cost :
      ∀ j,
        online_job_cost j ≤ ref_job_cost j.
    Proof.
      move⇒ j.
      apply: (leq_trans (H_job_cost_bounded j)).
      exact: H_ref_cost_dominates.
    Qed.

The Remaining Job-Cost Bound

We are now ready to introduce one of the central elements of the proof: the remaining job-cost bound, which for a given job j and given time t relates the amount of service received in the online schedule by j up to time t to the generic upper bound given by job_cost_bound.

Definition remaining_cost_bound j t :=
(job_cost_bound j ) - (service online_sched j t ).

As the proofs must reason about remaining_cost_bound quite a bit, we require a few auxiliary lemmas related to this definition, which we introduce below. Most of these are commonsense facts that will be obvious to a human reader.

Basic Facts About the Remaining Job-Cost Bound

The remaining job-cost bound at a given time t is equal to the remaining cost at the next point in time plus any service received at t.

    Lemma remcost_service :
      ∀ j t,
        remaining_cost_bound j t = remaining_cost_bound j t .+1 + service_at online_sched j t.
    Proof.
      move⇒ j t.
      have := H_job_cost_bounded j.
      have : service online_sched j t.+1 ≤ online_job_cost j by apply: service_at_most_cost.
      by rewrite /remaining_cost_bound -!service_last_plus_before; lia.
    Qed.

We can trivially lift the preceding fact to entire intervals.

    Lemma remcost_service_during :
      ∀ j t1 t2,
        t1 ≤ t2 →
        remaining_cost_bound j t1 = remaining_cost_bound j t2 + service_during online_sched j t1 t2.
    Proof.
      move⇒ j t1 t2 LEQ.
      have := H_job_cost_bounded j.
      have : service online_sched j t2 ≤ online_job_cost j by apply: service_at_most_cost.
      rewrite /remaining_cost_bound.
      by rewrite -(service_cat _ _ t1) //; lia.
    Qed.

Furthermore, we can lift the preceding whole-interval observation to arbitrary sets of jobs.

Notation hint: xpredT is the trivial dummy predicate that is always true, i.e., no jobs are being filtered here.

    Lemma remcost_total_service_during :
      ∀ (js : seq Job) t1 t2,
        t1 ≤ t2 →
        \sum_(j <- js ) remaining_cost_bound j t1
        = (\sum_(j <- js ) remaining_cost_bound j t2 ) + service_of_jobs online_sched xpredT js t1 t2.
    Proof.
      move⇒ js t1 t2 LEQ.
      rewrite /service_of_jobs.
      rewrite -[RHS]big_split_idem //=.
      apply: eq_bigr ⇒ j _.
      exact: remcost_service_during.
    Qed.

If we further know that at each point in the interval some job in the set of jobs under consideration is scheduled, then we can relate the remaining job-cost bound to the interval length.

This is a crucial reasoning step, as it allows us to conclude that the remaining cost must be zero at time t2 if the interval length equals the total remaining cost (as it will in our proof below).

    Lemma remaining_cost_invariant :
      ∀ (js : seq Job) t1 t2,
        t1 ≤ t2 →
        uniq js →
        (∀ t, t1 ≤ t < t2 → ∃ j , (j \in js ) && scheduled_at online_sched j t ) →
        \sum_(j <- js ) remaining_cost_bound j t1
        = (\sum_(j <- js ) remaining_cost_bound j t2 ) + (t2 - t1 ).
    Proof.
      move⇒ js t1 t2 LEQ UNIQ SCHED.
      suff <-: service_of_jobs online_sched xpredT js t1 t2 = t2 - t1 by apply: remcost_total_service_during.
      apply: service_of_jobs_always_scheduled ⇒ // t RANGE.
      have [j /andP[IN SCHED']] := SCHED t RANGE.
      by ∃ j; repeat split.
    Qed.

Relation to the Remaining Online Cost

As the purpose of the remaining job-cost bound is to upper-bound the leftover runtime of jobs in the online schedule, we introduce a few auxiliary lemmas relating the (true) remaining online cost to the (over-approximating) job-cost bound.

As before, we introduce an intuitive alias to succinctly refer to the remaining online cost. The definition used here, remaining_cost, is a standard Prosa construct.

Let online_remaining_cost := (@remaining_cost _ _ online_sched online_job_cost).

As intended, the remaining job-cost bound indeed upper-bounds the remaining online cost.

    Lemma online_remaining_cost_bounded :
      ∀ j t,
          online_remaining_cost j t ≤ remaining_cost_bound j t.
    Proof.
      move⇒ j t.
      rewrite leq_sub2rE //.
      apply: (@leq_trans (online_job_cost j)) ⇒ //.
      by apply: service_at_most_cost.
    Qed.

Furthermore, the remaining job-cost bound of any incomplete job is necessarily positive.

    Lemma remaining_cost_positive :
      ∀ j t,
        ~~ online_completed_by j t →
        remaining_cost_bound j t > 0.
    Proof.
      move⇒ j t.
      rewrite incomplete_is_positive_remaining_cost.
      rewrite /remaining_cost/remaining_cost_bound/job_cost.
      rewrite !subn_gt0 ⇒ LT.
      by apply: (leq_trans LT).
    Qed.

Conversely, if the total remaining job-cost bound of a set of jobs hits zero, then every job in the set is necessarily complete.

    Lemma remaining_cost_zero :
      ∀ (js : seq Job) t,
        \sum_(j <- js ) remaining_cost_bound j t == 0 →
        ∀ j,
          j \in js →
          online_completed_by j t.
    Proof.
      move⇒ js t ZERO j IN.
      apply: contraT.
      rewrite incomplete_is_positive_remaining_cost.
      suff: online_remaining_cost j t == 0 by rewrite /online_remaining_cost; lia.
      have REM0: remaining_cost_bound j t == 0.
      { move: ZERO.
        rewrite sum_nat_eq0_nat ⇒ /allP; apply.
        by rewrite mem_filter; apply/andP; split. }
      have := online_remaining_cost_bounded j t.
      by lia.
    Qed.

The Set of Critical Jobs

The second major element in the proof is the notion of the set of critical jobs at a given time t1 w.r.t. to a reference time t2. Intuitively, the critical jobs are those that must be scheduled immediately in order to avoid a deadline miss.

Technically, based on the arrival sequence arr_seq, given an interval [t1, t2), we define the set of critical jobs to be those that

are not finished at time t1 in the online schedule and
are finished in the reference schedule at time t2.

Notation hint: [seq j <- some_sequence | filter_predicate_on j ] is MathComp's notation for a list comprehension similar to those encountered e.g. in Haskell or Python.

    Definition critical_jobs t1 t2 :=
      [seq j <- arrivals_up_to arr_seq t2 |
        ref_completed_by j t2
        && ~~ online_completed_by j t1 ].

Basic Facts About the Set of Critical Jobs

To reason about critical jobs, we establish a number of facts about them that will be fairly obvious to a human reader.

To begin, if a job is critical at a time t2 w.r.t. a reference time t3, then it is also critical at any earlier time t1 w.r.t. the same reference time.

    Lemma critical_jobs_monotonicity :
      ∀ t1 t2 t3,
        t1 ≤ t2 ≤ t3 →
        ∀ j,
          j \in critical_jobs t2 t3 →
          j \in critical_jobs t1 t3.
    Proof.
      move⇒ t1 t2 t3 /andP[LEQ12 LEQ23] j.
      rewrite !mem_filter ⇒ /andP[ /andP[COMP NCOMP] IN].
      repeat (apply/andP; split ⇒ //).
      by apply: incompletion_monotonic; first exact: LEQ12.
    Qed.

If a job is critical at a time t1 w.r.t. a reference time t3 and no longer critical at a later time t2 (w.r.t. the same reference time), then it must have completed in the meantime.

    Lemma critical_jobs_dropout :
      ∀ t1 t2 t3,
        t1 ≤ t2 ≤ t3 →
        ∀ j,
          j \in critical_jobs t1 t3 →
          j \notin critical_jobs t2 t3 →
          online_completed_by j t2.
    Proof.
      move⇒ t1 t2 t3 /andP[LEQ12 LEQ23] j.
      rewrite !mem_filter ⇒ /andP[ /andP[COMP NCOMP1] IN].
      by rewrite COMP IN andbT andTb ⇒ /negPn.
    Qed.

We can thus express the set of critical jobs at a time t2 w.r.t. a reference time t3 as the set of critical jobs at an earlier time t1 (w.r.t. the same reference time) by filtering out all jobs that completed in the meantime.

    Lemma critical_jobs_filter_complete :
      ∀ t1 t2 t3,
        t1 ≤ t2 →
        critical_jobs t2 t3 =
          [seq j <- critical_jobs t1 t3 | ~~ online_completed_by j t2 ].
    Proof.
      move⇒ t1 t2 t3 LEQ.
      rewrite -filter_predI.
      apply: eq_filter ⇒ j /=.
      case: (ref_completed_by j t3);
        case ON2: (online_completed_by j t2) ⇒ //=.
      case ON1: (online_completed_by j t1) ⇒ //.
      exfalso.
      suff: online_completed_by j t2 ⇒ //.
      by apply: completion_monotonic; [exact LEQ|exact ON1].
    Qed.

Since the set of jobs is defined in terms of the arrival sequence (in which each job arrives at most once), the set of critical jobs is indeed a proper set (that is represented as a sequence without repeated elements).

    Lemma critical_jobs_uniq :
      ∀ t1 t2,
        uniq (critical_jobs t1 t2).
    Proof.
      move⇒ t1 t2.
      by apply/filter_uniq/arrivals_uniq.
    Qed.

We observe that the generic job-cost bound implies a lower bound on the earliest-possible completion time of any critical jobs at time zero.

This lemma may appear somewhat contrived on first sight, but represents an important reasoning step to rule out a cornercase at time zero.

    Lemma critical_jobs_min_completion_time :
      ∀ t,
        t ≥ \sum_(j <- critical_jobs 0 t ) job_cost_bound j.
    Proof.
      move⇒ t.
      apply: leq_trans;
        first by apply: leq_sum ⇒ j _; exact: H_ref_cost_dominates.
      have ->: \sum_(j <- critical_jobs 0 t) ref_job_cost j
               = \sum_(j <- critical_jobs 0 t) service_during ref_sched j 0 t.
      { rewrite big_seq [RHS]big_seq.
        apply: eq_bigr ⇒ j.
        rewrite mem_filter ⇒ /andP[ /andP[COMP NCOMP] IN].
        apply/eqP; rewrite eqn_leq.
        apply/andP; split ⇒ //.
        by apply: service_at_most_cost. }
      rewrite -/(service_of_jobs ref_sched xpredT _ 0 t).
      rewrite -[leqRHS]subn0.
      apply: service_of_jobs_le_length_of_interval' ⇒ //.
      exact: critical_jobs_uniq.
    Qed.

Finally, we observe that the total remaining job-cost bound of a set of critical jobs is monotonically decreasing.

    Lemma critical_jobs_remaining_cost_monotonic :
      ∀ t1 t2 t3,
        t1 ≤ t2 ≤ t3 →
        \sum_(j <- critical_jobs t1 t3 ) remaining_cost_bound j t1
        ≥ \sum_(j <- critical_jobs t2 t3 ) remaining_cost_bound j t2.
    Proof.
      move⇒ t1 t2 t3 /andP[LEQ12 LEQ23].
      apply: leq_trans; last first.
      { apply: (leq_sum_subseq _ (critical_jobs t2 t3)).
        rewrite subseq_filter //; apply/andP; split; last exact: filter_subseq.
        apply/allP ⇒ j.
        rewrite mem_filter ⇒ /andP[ /andP[COMP NCOMP] IN].
        repeat (apply/andP; split ⇒ //).
        by apply: incompletion_monotonic; first exact: LEQ12. }
      { apply: leq_sum ⇒ j _.
        rewrite leq_sub2lE.
        - exact: service_monotonic.
        - apply: (@leq_trans (online_job_cost j)) ⇒ //.
          exact: service_at_most_cost. }
    Qed.

Definition of Slackless Intervals

The third and final major element in the proof is the concept of "slackless intervals," which we define next. Slackless intervals tie together the remaining job-cost bound and the notion of critical jobs.

In the definition of a "slackless interval," the "slack" is computed based on the generic job-cost bound, since the online job cost is assumed to be unknown until after the job's completion (i.e., we seek to support also the non-clairvoyant setting). More precisely, we call a non-empty interval [t1, t2) slackless if the total remaining job-cost bound of the critical jobs at time t1 (w.r.t. reference time t2) is exactly equal to the interval length t2 - t1.

    Definition slackless_interval t1 t2 :=
      (t1 < t2 )
      && \sum_(j <- critical_jobs t1 t2 ) remaining_cost_bound j t1 == t2 - t1.

In fact, in our proof we require a stronger notion of slackless intervals: slackless intervals without "holes." To this end, we call an interval [t1, t2) contiguously slackless if [t1, t2) is slackless (and hence non-empty) and every suffix interval ending at t2 is also slackless.

Notation hints:

The notation 'I_(t2 - t1) is MathComp's notation for a bounded natural number, i.e., for the set {0, 1, 2, ..., t2 - t1 - 1}.
The notation [∀ delta, some_predicate_on delta ] is conceptually the same as the standard (∀ delta, some_property_on delta), but defined on a finite type and hence in bool and not Prop, and therefore computable (which we'll need).

Technical comment: the definition is slightly redundant, because the forall-quantified part covers also [t1, t2), but by requiring slackless_interval t1 t2 explicitly we avoid having to deal with empty intervals.

    Definition contiguously_slackless_interval t1 t2 :=
      slackless_interval t1 t2
      && [∀ delta : 'I_(t2 - t1 ), slackless_interval (t1 + delta) t2 ].

We are now ready to state the main property: To guarantee the transfer of schedulability, we define the following property, which forces critical jobs to be scheduled at the beginning of slackless intervals.

The Schedulability Transfer Criterion

The condition schedulability_transferred --- no job finishes later in the online schedule than in the reference schedule --- is simple and intuitive, but has one major downside: it can only be checked after the fact, that is, whether a schedule satisfies it becomes apparent only when it's already too to do anything about a possible deadline violation.

We therefore next introduce a definition equivalent to schedulability_transferred that can be checked before reaching a job's deadline, namely at the beginning of a slackless interval in which it is part of the critical jobs.

In short, the criterion requires that a critical job is scheduled at the beginning of any slackless interval in the online schedule. Establishing that this definition is indeed equivalent to schedulability_transferred is the over proof objective of this file.

    Definition transfer_schedulability_criterion :=
      ∀ t1 t2,
        slackless_interval t1 t2 →
        ∃ j ,
          scheduled_at online_sched j t1
          && (j \in critical_jobs t1 t2 ).

In the remainder of this section, we assume the criterion to be satisfied.

Hypothesis H_ts_criterion : transfer_schedulability_criterion.

The main proof establishing that transfer_schedulability_criterion is a sufficient condition for schedulability_transferred consists of three steps that lead to contradiction:

First, assume that some job j finishes later in the online schedule than in the reference schedule, and let t2 denote a time such that j is complete in the reference schedule and incomplete in the online schedule.
Second, we establish there exists a preceding contiguously slackless interval [t1, t2) and that j is a critical job at time t1 w.r.t. reference time t2.
Third, we establish that any job that is critical at the start of the contiguously slackless interval is necessarily complete in the online schedule at the end of it, which contradicts the assumption that j is incomplate at time t2.

Of the the three steps, the second step is by far the most challenging one. We consider it next.

Existence of a Contiguously Slackless Interval

In the second step of the overall proof strategy, the goal is to establish the existence of a contiguously slackless interval under two major assumptions: (1) the transfer_schedulability_criterion holds and (2) there exists a job that completes later in the online schedule than in the reference schedule.

While this existence claim may not be so difficult for a human to "see," it is not so easy to formally establish this existence proof such that Rocq verifies it. We therefore first establish a number of supporting auxiliary lemmas.

Supporting Lemmas

If a job is complete in the reference schedule and not complete in the online schedule, it is by definition a critical job at the time.

    Lemma late_in_critical_jobs :
      ∀ j t,
        ref_completed_by j t →
        ~~ online_completed_by j t →
        j \in critical_jobs t t.
    Proof.
      move⇒ j t COMP NCOMP.
      have [ZERO|POS] := (posnP (ref_job_cost j)).
      { exfalso.
        have := ref_cost_bounds_online_cost j.
        by move: NCOMP; rewrite /online_completed_by/completed_by/job_cost; lia. }
      { rewrite mem_filter.
        repeat (apply/andP; split ⇒ //).
        have [t' [/andP[ARR LT] SCHED]]: ∃ t' : nat , job_arrival j ≤ t' < t ∧ scheduled_at ref_sched j t'.
        { apply: positive_service_implies_scheduled_since_arrival ⇒ //.
          by move: COMP; rewrite /ref_completed_by/completed_by/job_cost; lia. }
        rewrite /arrivals_up_to.
        by apply: job_in_arrivals_between ⇒ //; lia. }
    Qed.

No job is late at the start of the schedule, which rules out some cornercases.

    Lemma late_not_at_start :
      ∀ j t,
        ref_completed_by j t →
        ~~ online_completed_by j t →
        t > 0.
    Proof.
      move⇒ j t COMP NCOMP.
      apply: (contraNltn _ NCOMP).
      rewrite leqn0 ⇒ /eqP ZERO.
      move: COMP; rewrite /ref_completed_by/online_completed_by/completed_by/job_cost.
      rewrite ZERO !service0.
      by move: (ref_cost_bounds_online_cost j); lia.
    Qed.

Intervals of Non-Positive Slack

As a stepping stone towards finding slackless intervals, we introduce the related notion of an interval with non-positive slack. This notion relaxes the slackless interval's strict equality to an inequality. It thus over-approximates slackless intervals (i.e., every slackless interval has non-positive slack, but an interval with non-positive slack may not satisfy the slackless definition if there is in fact negative "slack").

Definition nonpositive_slack t1 t2 :=
\sum_(j <- critical_jobs t1 t2 ) remaining_cost_bound j t1 ≥ t2 - t1.

Mirroring the step from slackless intervals to contiguously slackless intervals, we establish the notion of contiguously non-positive slack intervals, with the obvious interpretation: every suffix-interval must also have non-positive slack.

Definition contiguously_nps t1 t2 :=
[∀ delta : 'I_(t2 - t1 ), nonpositive_slack (t1 + delta) t2 ].

Facts about Intervals with Non-Positive Slack

We establish some further auxiliary lemmas covering various cases coming up in the main proofs below before moving on.

First, before the start of a maximally contiguously non-positive slack interval is an interval with positive slack.

    Lemma contiguously_nps_start :
      ∀ t0 t2,
        ~~ contiguously_nps t0 t2 →
        contiguously_nps t0 .+1 t2 →
        ~~ nonpositive_slack t0 t2.
    Proof.
      move⇒ t0 t2 /forallPn /= [d NPS] /forallP /= CNPS.
      case: d NPS; case ⇒ [d //= /[1! addn0 ] LT|] //.
      move⇒ d LT NPS; exfalso.
      move: NPS ⇒ /negP; apply ⇒ //=.
      have LT': d < t2 - t0.+1 by lia.
      move: (CNPS (Ordinal LT')) ⇒ //=.
      by rewrite addSnnS.
    Qed.

If a job is finished at a given time t2 in the reference schedule, but not in the online schedule, then there exists a non-empty contiguously non-positive slack interval [t1, t2) that either starts at time zero or is preceded by an interval with positive slack.

NB: Note the comments in the proof! This is a key step.

    Lemma contiguously_nps_existence :
      ∀ j t2,
        ref_completed_by j t2 →
        ~~ online_completed_by j t2 →
        ∃ t1 ,
          contiguously_nps t1 t2
          ∧ t1 < t2
          ∧ (t1 = 0 ∨ ~~ nonpositive_slack t1 .-1 t2 ).
    Proof.
      move⇒ j t2 COMP NCOMP.

As a starting point, we establish that [t2 -1, t2) has non-positive slack.

      have NPS2 : nonpositive_slack t2.-1 t2.
      { apply: (@leq_trans (\sum_(j' <- [:: j]) _)); last first.
        - apply: leq_sum_subseq.
          rewrite sub1seq.
          apply: critical_jobs_monotonicity; last exact: late_in_critical_jobs.
          by lia.
        - rewrite big_seq1.
          suff: remaining_cost_bound j t2.-1 > 0 by lia.
          apply: remaining_cost_positive.
          apply: (incompletion_monotonic _ _ _ _ _ NCOMP).
          by lia. }

We "upgrade" NPS2 to a contiguously non-positive slack interval. Since the interval contains only one point, this is conceptually trivial, but we need it as a witness for the below search via MathComp's ex_minn facility.

      have CNPS2 : contiguously_nps t2.-1 t2.
      { rewrite /contiguously_nps.
        apply: contraT ⇒ /forallPn /= [d +].
        move⇒ /negP; suff: nonpositive_slack (t2.-1 + d) t2 ⇒ //.
        have ->: nat_of_ord d = 0 by move: (ltn_ord d); lia.
        rewrite addn0.
        exact NPS2. }

The following is a key step of the overall proof strategy: We search "backwards" in time from t2.-1 until we find the starting point of the maximally, contiguously non-positive slack interval ending at t2.

      have WITNESS : ∃ t , contiguously_nps t t2 by ∃ t2.-1.
      have [t1 CNPS MIN] := (find_ex_minn WITNESS).
      ∃ t1; repeat split ⇒ //;
        first by move: (MIN t2.-1 CNPS2) (late_not_at_start j t2 COMP NCOMP); lia.

Finally, we do a case analysis on t1 =?= 0 to figure out the last disjunction of the existence claim: either t1 = 0, in which case the first case holds trivially, or t1 = t0.+1 > 0, in which case we show that [t0, t2) has positive slack.

      case: t1 CNPS MIN ⇒ [| t0 CNPS MIN]; [by left|right].
      have [CNPS0|NCNPS] := boolP (contiguously_nps t0 t2);
        first by move: (MIN t0 CNPS0); lia.
      rewrite -pred_Sn.
      exact: contiguously_nps_start.
    Qed.

The following is a key technical lemma used in the induction "growing" the contiguously slackless interval (the existence of which we seek to establish). It establishes that, if we have a slackless interval [t1, t2) and [t1 + 1, t2) has non-positive slack, then [t1 + 1, t2) is also a slackless interval.

    Lemma slackless_interval_step :
      ∀ t1 t2,
        t1 .+1 < t2 →
        nonpositive_slack t1 .+1 t2 →
        slackless_interval t1 t2 →
        slackless_interval t1 .+1 t2.
    Proof.
      move⇒ t1 t2 LT NPS SL.
      move: (SL) ⇒ /andP[LT' ZS].
      apply/andP; split ⇒ //.
      move: (H_ts_criterion t1 t2 SL) ⇒ [j /andP[SCHED IN]].
      have [COMP|NCOMP] := boolP( online_completed_by j t1.+1 ).
      { rewrite (critical_jobs_filter_complete t1) // big_filter_cond.
        have [ZERO|POS] := posnP (remaining_cost_bound j t1.+1).
        { rewrite big_rmcond_in /=.
          { move: ZS; rewrite (remaining_cost_invariant _ t1 t1.+1) //.
            - by lia.
            - exact: critical_jobs_uniq.
            - move⇒ t /andP[LO HI].
              ∃ j; apply/andP; split ⇒ //.
              by have → : t = t1 by lia. }
          { move⇒ j' IN'.
            rewrite andbT ⇒ /negPn COMP'.
            suff → : j' = j ⇒ //.
            apply/eqP/contraT ⇒ NEQ.
            suff /negP: ~~ online_completed_by j' t1.+1 ⇒ //.
            rewrite /online_completed_by.
            apply not_scheduled_remains_incomplete;
              first by move: IN'; rewrite mem_filter /online_completed_by ⇒ /andP[/andP[_ NCOMP'] _].
            move: NEQ; rewrite eq_sym ⇒ NEQ.
            by apply: uniproc_only_one_scheduled; first exact: NEQ. }}
        { exfalso.
          move: NPS; rewrite /nonpositive_slack.
          rewrite (critical_jobs_filter_complete t1) // big_filter_cond
            big_seq_cond.
          rewrite (eq_bigr (fun j' ⇒ remaining_cost_bound j' t1)); last first.
          { move⇒ j' /andP[IN' /andP[NCOMP' _]].
            rewrite /remaining_cost_bound.
            apply/eqP; rewrite eqn_sub2lE;
              try (apply: leq_trans;
                   last exact: H_job_cost_bounded;
                   exact: service_at_most_cost).
            rewrite /service -service_during_last_plus_before //.
            apply/eqP; rewrite service_at_is_scheduled_at -[RHS]addn0.
            apply/eqP; rewrite eqn_add2l eqb0.
            apply: uniproc_only_one_scheduled; last by exact: SCHED.
            apply: contraT ⇒ /negPn/eqP EQ.
            move: NCOMP' ⇒ /negP.
            by rewrite -EQ. }
          { rewrite (eq_bigl (fun j' ⇒ (j' \in critical_jobs t1 t2) && (j != j'))); last first.
            { move⇒ j'.
              case IN': (j' \in critical_jobs t1 t2) ⇒ //=.
              case: (eqVneq j j') ⇒ [<-|NEQ //=];
                first by rewrite COMP.
              rewrite andbT.
              have INCOMP: ~~ online_completed_by j' t1
                by move: IN'; rewrite mem_filter ⇒ /andP[/andP[]].
              apply: not_scheduled_remains_incomplete ⇒ //.
              by apply: (uniproc_only_one_scheduled NEQ). }
            { rewrite -big_seq_cond ⇒ NPS.
              have GT1: remaining_cost_bound j t1 > 1.
              { move: POS; rewrite /remaining_cost_bound.
                rewrite /service -service_during_last_plus_before //.
                rewrite service_at_is_scheduled_at SCHED.
                by lia. }
              move: ZS.
              rewrite (bigID (fun j' ⇒ j == j')) /=.
              rewrite (big_pred1_seq _ _ IN) //; last exact: critical_jobs_uniq.
              by lia. } } } }
      { rewrite (critical_jobs_filter_complete t1) //.
        rewrite -(@eq_in_filter _ predT); last first.
        { move⇒ j' IN'.
          case: (eqVneq j' j) ⇒ [-> //| /[1! eq_sym ] NEQ //=]; symmetry.
          have INCOMP: ~~ online_completed_by j' t1
            by move: IN'; rewrite mem_filter ⇒ /andP[/andP[]].
          apply: not_scheduled_remains_incomplete ⇒ //.
          by apply: (uniproc_only_one_scheduled NEQ). }
        { rewrite filter_predT.
          move: ZS; rewrite (remaining_cost_invariant _ t1 t1.+1) //.
          - by lia.
          - exact: critical_jobs_uniq.
          - move⇒ t /andP[LO HI].
            ∃ j; apply/andP; split ⇒ //.
            by have → : t = t1 by lia. } }
    Qed.

Main Argument: Slackless Interval Existence

With key helper lemmas in place, we can proceed to the main argument establishing the existence of contiguously slackless intervals preceding a late completion.

We first establish the main "upgrade" lemma: if we have a slackless interval [t1, t2), and know that [t1, t2) is also a contiguously non-positive slack interval, then we can conclude that [t1, t2) is in fact also contiguously slackless.

    Lemma slackless_interval_continuation :
      ∀ t1 t2,
        slackless_interval t1 t2 →
        contiguously_nps t1 t2 →
        [∀ delta : 'I_(t2 - t1 ), slackless_interval (t1 + delta) t2 ].
    Proof.
      move⇒ t1 t2 SL CNPS.
      apply /forallP ⇒ /= d.
      case: d ⇒ d //=.
      (* NB: The following line is a "magic incantation" from MathComp that
         makes elim do a _strong induction_ on d (rather than a regular
         induction). *)
      case: (ubnPgeq d).
      elim: d ⇒ [d /[!leqn0 ]/eqP ->|b IH d DB LT]; first by rewrite addn0.
      have [LEQ|LTbd] := leqP d b; first by apply IH.
      move: SL ⇒ /andP [LT' _].
      have → : d = b.+1 by lia.
      rewrite addnS.
      apply: slackless_interval_step; first by lia.
      - move: CNPS ⇒ /forallP /= CNPS.
        rewrite -addnS.
        have LT'' : b.+1 < t2 - t1 by lia.
        by move: (CNPS (Ordinal LT'')).
      - by apply IH; lia.
    Qed.

With the upgrade lemma in place, we are finally ready to derive the existence of contiguously slackless intervals from a late completion.

Note: This proof is commented more than usual to highlight the key reasoning steps.

    Lemma slackless_interval_existence :
      ∀ j t2,
        ref_completed_by j t2 →
        ~~ online_completed_by j t2 →
        ∃ (t1 : instant ),
          contiguously_slackless_interval t1 t2
          && (j \in critical_jobs t1 t2 ).
    Proof.

Setup: job j is incomplete at time t2 in the online schedule, but complete in the reference schedule.

move⇒ j t2 COMP NCOMP.

A: Recall that a contiguously non-positive slack interval exists before t2.

      have [t1 [CNPS [LT START]]] :=
        contiguously_nps_existence j t2 COMP NCOMP.
      move: (CNPS) ⇒ /forallP /= CNPS'.

B: We will show that [t1, t2) is a contiguously slackless interval.

∃ t1; apply/andP; split;

Showing that j is in critical_jobs t1 t2 is trivial and done here.

last by (apply: critical_jobs_monotonicity; last exact: late_in_critical_jobs); lia.

C: We recall that [t1, t2) has non-positive slack.

      have NPS1 : nonpositive_slack t1 t2.
      { have LT' : 0 < t2 - t1 by lia.
        move: (CNPS' (Ordinal LT')) ⇒ //=.
        by rewrite addn0. }

D: From the observation that [t1, t2) has non-positive slack, we infer that [t1, t2) is in fact slackless. This step needs to deal with a bunch of cornercases (e.g., at time zero).

      have SL1 : slackless_interval t1 t2.
      { move: (NPS1); rewrite /nonpositive_slack leq_eqVlt ⇒ /orP [EQ|NEQ];
          first by repeat (apply/andP; split ⇒ //).
        exfalso.
        move: START ⇒ [EQ1|POS].
        - move: NEQ; rewrite EQ1 /nonpositive_slack/remaining_cost_bound.
          rewrite subn0.
          under eq_bigr do rewrite service0 subn0.
            move: (critical_jobs_min_completion_time t2).
          by lia.
        - move: POS.
          rewrite /nonpositive_slack -ltnNge.
          by feed (critical_jobs_remaining_cost_monotonic t1.-1 t1 t2); lia. }
      apply/andP; split; first exact: SL1.

E: Finally, the above "upgrade" lemma allows us to go from [t1, t2) being slackless to [t1, t2) being contiguously slackless.

exact: slackless_interval_continuation.
Qed.

All Critical Jobs Complete in a Contiguously Slackless Interval

The third step of the overall proof strategy requires that all critical jobs are complete at the end of a contiguously slackless interval. We establish this key "stepping stone" fact in the following lemma.

From the length of the proof and the absence of many additional supporting lemmas, it should be obvious that this step is much easier than the preceding one. Which makes sense because the "contiguous" property is a very strong property, which is both hard to establish and easy to exploit.

    Lemma slackless_interval_completion :
      ∀ j t1 t2,
        contiguously_slackless_interval t1 t2 →
        (j \in critical_jobs t1 t2 ) →
        online_completed_by j t2.
    Proof.
      move⇒ j t1 t2 /andP[SL /forallP /= CSL] CRIT.

We are going to argue that the total remaining job-cost bound for the critical jobs across [t1, t2) is zero, and they all must have completed. What remains to be shown afterwards is that the remaining job-cost bound is indeed zero.

apply: (remaining_cost_zero (critical_jobs t1 t2)) ⇒ //.

The main setup step: convert the fact that [t1, t2) is contiguously slackless into the property that at each point in the interval there is a critical job scheduled.

      have SCHED:
        ∀ t', t1 ≤ t' < t2
              → ∃ j', (j' \in critical_jobs t1 t2)
                      && scheduled_at online_sched j' t'.
      { move⇒ t' /andP[LO HI].
        have LT' : t' - t1 < (t2 - t1) by lia.
        move: (CSL (Ordinal LT')) ⇒ //=.
        have → : t1 + (t' - t1) = t' by lia.
        move⇒ SL'.
        have [j' /andP[SCHED' IN']] := (H_ts_criterion _ _ SL').
        ∃ j'; apply/andP; split ⇒ //.
        apply: critical_jobs_monotonicity; last exact IN'.
        by lia. }
      move: SL ⇒ /andP[LT /eqP SL'].

From the property that there is always a critical job scheduled, we can apply a helper lemma that lets us relate the interval length to the accumulated service.

have REM := remaining_cost_invariant (critical_jobs t1 t2) t1 t2 _ _ SCHED.
feed_n 2 REM; [by lia|exact: critical_jobs_uniq|].

The rest is simple arithmetic.

by move: REM; rewrite SL'; lia.
Qed.

This marks the end of the generic argument for an abstract job_cost_bound. We will now close this section and establish the concrete results.

End ParametericCostBound.

Main Results

Naturally, to derive any guarantees, the reference schedule needs to over-approximate the job costs encountered in the online schedule. We add this assumption now.

Hypothesis H_bounded_job_costs : ∀ j, online_job_cost j ≤ ref_job_cost j.

Sufficiency Theorem w.r.t. Online Job Costs

Using the generic argument for job_cost_bound := online_job_cost, we establish that transfer_schedulability_criterion is a sufficient condition for schedulability_transferred to hold.

  Theorem online_transfer_schedulability_criterion_sufficiency :
    transfer_schedulability_criterion online_job_cost → schedulability_transferred.
  Proof.
    move⇒ CRIT j t2 COMP.

By contradiction: suppose j is not complete in the online schedule at time t, but it is in the reference schedule.

apply: contraT ⇒ NCOMP.

Observe that online_job_cost trivially "bounds" online_job_cost.

have BOUNDED : ∀ j, online_job_cost j ≤ online_job_cost j by done.

There is necessarily a contiguously slackless interval [t1, t2).

have [t1 /andP[CSL IN]] :=
slackless_interval_existence _ BOUNDED H_bounded_job_costs CRIT j t2 COMP NCOMP.

That means that j is complete at time t2, which contradicts the initial assumption that j is incomplete at time t2.

    suff: online_completed_by j t2 by move: NCOMP ⇒ /negP.
    by apply: (slackless_interval_completion _ BOUNDED CRIT j t1).
   Qed.

As a straightforward corollary, we lift online_transfer_schedulability_criterion_sufficiency to the level of job deadlines for the sake of completeness.

  Corollary online_transfer_schedulability_criterion_ensures_schedulability :
    transfer_schedulability_criterion online_job_cost →
    (∀ j, ref_job_meets_deadline j → online_job_meets_deadline j ).
  Proof.
    move⇒ CRIT j MET.
    apply: deadlines_met ⇒ //.
    exact: online_transfer_schedulability_criterion_sufficiency.
  Qed.

Necessity Theorem w.r.t. Online Job Costs

For job_cost_bound := online_job_cost, we can also establish the reverse direction: transfer_schedulability_criterion online_job_cost is a necessary condition for schedulability_transferred, which establishes the equivalency of the two definitions for online job costs.

As a stepping stone, we first establish a lemma that shows that, if there ever is a slackless interval in which none of the critical jobs is scheduled at the start of the interval, then some job must finish later in the online schedule than in the reference schedule.

  Lemma delay_if_no_critical_job_is_scheduled :
    ∀ t1 t2,
      slackless_interval online_job_cost t1 t2 →
      {in critical_jobs t1 t2 , ∀ j, ~~ scheduled_at online_sched j t1 } →
      (∃ j , (j \in critical_jobs t1 t2 ) ∧ ~~ online_completed_by j t2 ).
  Proof.
    move⇒ t1 t2 /andP [LT ZS] NONE.

Let's restate the claim in terms of has, which we can contradict more easily.

suff /hasP[j IN NCOMP]:
has (fun j ⇒ ~~ online_completed_by j t2) (critical_jobs t1 t2) by ∃ j.

By contradiction: suppose that all critical jobs are complete at time t2.

apply: contraT ⇒ /hasPn COMP.

As a stepping stone, we observe that an incomplete critical job necessarily exists if the total remaining cost bound is non-zero.

    have NCOMP: \sum_(j <- critical_jobs t1 t2)
                  remaining_cost_bound online_job_cost j t2 > 0
                → exists2 j , (j \in critical_jobs t1 t2)
                             & ~~ online_completed_by j t2.
    { rewrite sum_nat_gt0 ⇒ /hasP [j IN NZ].
      ∃ j; first by move: IN; rewrite filter_predT.
      rewrite /online_completed_by/completed_by -ltnNge.
      move: NZ; rewrite /remaining_cost_bound/job_cost.
      by lia. }

Hence we proceed to show that the total remaining job cost is non-zero at time t2.

    suff NZ: \sum_(j <- critical_jobs t1 t2) remaining_cost_bound online_job_cost j t2 > 0.
    { have [j' IN' NCOMP'] := NCOMP NZ.
      move: (COMP j' IN') ⇒ /negPn.
      by move: NCOMP' ⇒ /negP. }

In the following, we exploit the assumption that no critical job is scheduled at time t1 implies that the critical jobs collectively receive no service at that time. Before we can use that fact, though, we must first reshape the sum of remaining cost bounds to expose the collective service received at time t1 in the formula.

move: ZS; rewrite /remaining_cost_bound.

First, split the sum of remaining cost bounds into a sum of job costs and a sum of service received.

rewrite !sumnB ⇒ [|j _|j _]; try exact: service_at_most_cost.
move⇒ /eqP ZS.

Next, split the service received into the service received up to (but not including) time t1 and the service received during [t1 + 1,t2).

Note this leaves out the service received at time t1, which we know to be zero due the assumption that no critical job is scheduled at time t1.

    rewrite [X in _ - X]big_seq_cond.
    under [X in _ - X]eq_bigr ⇒ j IN.
    { rewrite -(service_cat _ j t1 t2) // -service_during_first_plus_later //.
      rewrite service_at_is_scheduled_at.
      have → //=: scheduled_at online_sched j t1 = false.
      { move: IN; rewrite andbT ⇒ IN.
        by apply/negbTE/NONE. }
      rewrite add0n.
      over. }
    rewrite -big_seq_cond big_split_idem //=.

Observe that the sum of service_during in the goal matches the definition of service_of_jobs, for which there are useful lemmas in Prosa.

rewrite -/(service_of_jobs _ predT _ t1.+1 t2).

Rewrite the goal to expose that we need to show that the service received by the critical jobs during [t1 + 1, t2) is strictly less than t2 - t1.

rewrite subnDA ZS.

Recall a basic fact about service_of_jobs on unit-speed uniprocessors: the total amount of service received in an interval is trivially upper-bounded by the interval length.

    have: service_of_jobs online_sched predT (critical_jobs t1 t2) t1.+1 t2 ≤ t2 - (t1.+1 ).
    { apply: service_of_jobs_le_length_of_interval' ⇒ //.
      exact: critical_jobs_uniq. }

The goal then follows immediately from simple arithmetic.

by lia.
Qed.

From the preceding helper lemma, we can easily prove that schedulability_transferred implies transfer_schedulability_criterion online_job_cost.

  Theorem online_transfer_schedulability_criterion_necessity :
    schedulability_transferred → transfer_schedulability_criterion online_job_cost.
  Proof.

Consider a slackless interval [t1, t2).

move⇒ TRANS t1 t2 SL.

To prove the claim, it suffices to show that one of the critical jobs is scheduled at t1.

suff: has (fun j ⇒ scheduled_at online_sched j t1) (critical_jobs t1 t2)
by move⇒ /hasP [j IN SCHED]; ∃ j; apply/andP; split.

By contradiction: suppose there is no such job scheduled at t1.

apply: contraT.
rewrite -all_predC ⇒ /allP ⇒ NSCHED.

From the stepping stone lemma, we have that some job finishes late as a result.

    have [j [IN NCOMP]]: ∃ j , (j \in critical_jobs t1 t2) ∧ ~~ online_completed_by j t2
      by apply: delay_if_no_critical_job_is_scheduled.
    move: IN; rewrite mem_filter ⇒ /andP[ /andP[COMP _] _].

But this contradicts the precondition that no job finishes later than in the reference schedule.

    move: (TRANS j t2 COMP) ⇒ COMP'.
    by move: NCOMP ⇒ /negP.
  Qed.

Sufficiency Theorem w.r.t. Reference Job Costs

Using the generic argument for job_cost_bound := ref_job_cost, we establish that transfer_schedulability_criterion is a sufficient condition for schedulability_transferred to hold even if job costs are over-approximated.

  Theorem ref_transfer_schedulability_criterion_sufficiency :
    transfer_schedulability_criterion ref_job_cost → schedulability_transferred.
  Proof.
    move⇒ CRIT j t2 COMP.

By contradiction: suppose j is not complete in the online schedule at time t, but it is in the reference schedule.

apply: contraT ⇒ NCOMP.

Observe that ref_job_cost trivially "bounds" ref_job_cost.

have BOUNDED : ∀ j, ref_job_cost j ≤ ref_job_cost j by done.

There is necessarily a contiguously slackless interval [t1, t2).

have [t1 /andP[CSL IN]] :=
slackless_interval_existence _ H_bounded_job_costs BOUNDED CRIT j t2 COMP NCOMP.

That means that j is complete at time t2, which contradicts the initial assumption that j is incomplete at time t2.

    suff: online_completed_by j t2 by move: NCOMP ⇒ /negP.
    by apply: (slackless_interval_completion _ H_bounded_job_costs CRIT j t1).
   Qed.

For completeness' sake, we once more lift the sufficient condition to the level of job deadlines.

  Corollary ref_transfer_schedulability_criterion_ensures_schedulability :
    transfer_schedulability_criterion ref_job_cost →
    (∀ j, ref_job_meets_deadline j → online_job_meets_deadline j ).
  Proof.
    move⇒ CRIT j MET.
    apply: deadlines_met ⇒ //.
    exact: ref_transfer_schedulability_criterion_sufficiency.
  Qed.

Without further restrictions, it is not possible to establish necessity for job_cost_bound := ref_job_cost.

End TransferSchedulability.