Finish Abstract RTA

model/schedule/uni/limited/abstract_RTA/definitions.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job.
+Require Import rt.model.schedule.uni.schedule. 
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * Definitions for Abstract Response-Time Analysis *)
+(** In this module, we propose a set of definitions for the general framework for response-time analysis (RTA) 
+    of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
+Module AbstractRTADefinitions. 
+
+  Import Job Epsilon UniprocessorSchedule.
+
+  (* In this section, we introduce all the abstract notions required by the analysis. *)
+  Section Definitions.
+ 
+    Context {Task: eqType}.
+     
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+    
+    (* Consider any arrival sequence... *) 
+    Variable arr_seq: arrival_sequence Job.
+    
+    (* ... and any uniprocessor schedule of this arrival sequence. *)
+    Variable sched: schedule Job.
+
+    (* Let tsk be any task that is to be analyzed *)
+    Variable tsk: Task.
+    
+    (* For simplicity, let's define some local names. *)
+    Let job_scheduled_at := scheduled_at sched.
+    Let job_completed_by := completed_by job_cost sched.
+
+    (* Recall that a job j is pending_earlier_and_at a time instant t iff job
+       j arrived before time t and is still not completed by time t. *)
+    Let job_pending_earlier_and_at := pending_earlier_and_at job_arrival job_cost sched.
+
+    (* We are going to introduce two main variables of the analysis: 
+       (a) interference, and (b) interfering workload. *)
+
+    (** a) Interference *)
+    (* Execution of a job may be postponed by the environment and/or the system due to different
+       factors (preemption by higher-priority jobs, jitter, black-out periods in hierarchical 
+       scheduling, lack of budget, etc.), which we call interference. 
+
+       Besides, note that even the n’th activation of a task can suffer from interference at 
+       the beggining of its busy interval (despite the fact that this job hasn’t even arrived 
+       at that moment!). Thus, it makes more sense (at least for the current busy-interval 
+       analysis) to think about interference of a job as any interference within the 
+       corresponding busy interval, and not after release of the job.
+
+       Based on that, assume a predicate that expresses whether a job j under consideration 
+       incurs interference at a given time t (in the context of the schedule under consideration).
+       This will be used later to upper-bound job j's response time. Note that a concrete 
+       realization of the function may depend on the schedule, but here we do not require this 
+       for the sake of simplicity and generality. *)
+    Variable interference: Job -> time -> bool.
+
+    (** b) Interfering Workload *)
+    (* In addition to interference, the analysis assumes that at any time t, we know an upper 
+       bound on the potential cumulative interference that can be incurred in the future by any
+       job (i.e., the total remaining potential delays). Based on that, assume a function 
+       interfering_workload that indicates for any job j, at any time t, the amount of potential 
+       interference for job j that is introduced into the system at time t. This function will be
+       later used to upper-bound the length of the busy window of a job.
+       One example of workload function is the "total cost of jobs that arrive at time t and 
+       have higher-or-equal priority than job j". In some task models, this function expresses 
+       the amount of the potential interference on job j that "arrives" in the system at time t. *)
+    Variable interfering_workload: Job -> time -> time.
+
+    (* In order to bound the response time of a job, we must to consider the cumulative 
+       interference and cumulative interfering workload. *)
+    Definition cumul_interference j t1 t2 := \sum_(t1 <= t < t2) interference j t.
+    Definition cumul_interfering_workload j t1 t2 := \sum_(t1 <= t < t2) interfering_workload j t.
+
+    (** Definition of Busy Interval *)
+    (* Further analysis will be based on the notion of a busy interval. The overall idea of the 
+       busy interval is to take into account the workload that cause a job under consideration to 
+       incur interference. In this section, we provide a definition of an abstract busy interval. *)
+    Section BusyInterval.
+
+      (* We say that time instant t is a quiet time for job j iff two conditions hold. 
+         First, the cumulative interference at time t must be equal to the cumulative
+         interfering workload, to indicate that the potential interference seen so far 
+         has been fully "consumed" (i.e., there is no more higher-priority work or other 
+         kinds of delay pending). Second, job j cannot be pending at any time earlier
+         than t _and_ at time instant t (i.e., either it was pending earlier but is no 
+         longer pending now, or it was previously not pending and may or may not be 
+         released now), to ensure that the busy window captures the execution of job j. *)
+      Definition quiet_time (j: Job) (t: time) :=
+        cumul_interference j 0 t = cumul_interfering_workload j 0 t /\
+        ~~ job_pending_earlier_and_at j t.
+      
+      (* Based on the definition of quiet time, we say that interval [t1, t2) is 
+         a (potentially unbounded) busy-interval prefix w.r.t. job j iff the 
+         interval (a) contains the arrival of job j, (b) starts with a quiet
+         time and (c) remains non-quiet. *)
+      Definition busy_interval_prefix (j: Job) (t1 t2: time) :=
+        t1 <= job_arrival j < t2 /\
+        quiet_time j t1 /\
+        (forall t, t1 < t < t2 -> ~ quiet_time j t). 
+
+      (* Next, we say that an interval [t1, t2) is a busy interval iff
+         [t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
+      Definition busy_interval (j: Job) (t1 t2: time) :=
+        busy_interval_prefix j t1 t2 /\
+        quiet_time j t2.
+
+      (* Note that the busy interval, if it exists, is unique. *)
+      Lemma busy_interval_is_unique:
+        forall j t1 t2 t1' t2',
+          busy_interval j t1 t2 ->
+          busy_interval j t1' t2' ->
+          t1 = t1' /\ t2 = t2'.
+      Proof.
+        intros ? ? ? ? ? BUSY BUSY'.
+        have EQ: t1 = t1'.
+        { apply/eqP.
+          apply/negPn/negP; intros CONTR.
+          move: BUSY => [[IN [QT1 NQ]] _].
+          move: BUSY' => [[IN' [QT1' NQ']] _].
+          move: CONTR; rewrite neq_ltn; move => /orP [LT|GT].
+          { apply NQ with t1'; try done; clear NQ.
+            apply/andP; split; first by done.
+            move: IN IN' => /andP [_ T1] /andP [T2 _].
+              by apply leq_ltn_trans with (job_arrival j).
+          }
+          { apply NQ' with t1; try done; clear NQ'.
+            apply/andP; split; first by done.
+            move: IN IN' => /andP [T1 _] /andP [_ T2].
+              by apply leq_ltn_trans with (job_arrival j).
+          }
+        }
+        subst t1'.
+        have EQ: t2 = t2'.
+        { apply/eqP.
+          apply/negPn/negP; intros CONTR.
+          move: BUSY => [[IN [_ NQ]] QT2].
+          move: BUSY' => [[IN' [_ NQ']] QT2'].
+          move: CONTR; rewrite neq_ltn; move => /orP [LT|GT].
+          { apply NQ' with t2; try done; clear NQ'.
+            apply/andP; split; last by done.
+            move: IN IN' => /andP [_ T1] /andP [T2 _].
+              by apply leq_ltn_trans with (job_arrival j).
+          }
+          { apply NQ with t2'; try done; clear NQ.
+            apply/andP; split; last by done.
+            move: IN IN' => /andP [T1 _] /andP [_ T2].
+              by apply leq_ltn_trans with (job_arrival j).
+          }
+        }
+        subst t2'.
+          by done.
+      Qed.
+      
+    End BusyInterval.
+
+    (* In this section, we introduce some assumptions about the
+       busy interval that are fundamental for the analysis. *)
+    Section BusyIntervalProperties.
+
+      (* We say that a schedule is "work_conserving" iff for any job j from task tsk and 
+         at any time t within a busy interval, there are only two options:
+         either (a) interference(j, t) holds or (b) job j is scheduled at time t. *)
+      Definition work_conserving :=
+        forall j t1 t2 t,
+          arrives_in arr_seq j ->
+          job_task j = tsk ->
+          job_cost j > 0 ->
+          busy_interval j t1 t2 ->
+          t1 <= t < t2 ->
+          ~ interference j t <-> job_scheduled_at j t.
+
+      (* Next, we say that busy intervals of task tsk are bounded by L iff, for any job j of task
+         tsk, there exists a busy interval with length at most L. Note that the existence of such a
+         bounded busy interval is not guaranteed if the schedule is overloaded with work. 
+         Therefore, in the later concrete analyses, we will have to introduce an additional 
+         condition that prevents overload. *)
+      Definition busy_intervals_are_bounded_by L :=
+        forall j,
+          arrives_in arr_seq j ->
+          job_task j = tsk ->
+          job_cost j > 0 -> 
+          exists t1 t2,
+            t1 <= job_arrival j < t2 /\
+            t2 <= t1 + L /\
+            busy_interval j t1 t2.
+
+      (* Although we have defined the notion of cumulative interference of a job, it is still hard to be 
+         used in a response-time analysis because of the variability of job parameters. To address this 
+         issue, we define the notion of an interference bound. Note that according to the definition of
+         a work conserving schedule, interference does _not_ include execution of a job itself. Therefore,
+         an interference bound is not obliged to take into account the execution of this job. We say that 
+         the job interference is bounded by an interference_bound_function (IBF) iff for any job j of 
+         task tsk the cumulative interference incurred by j in the subinterval [t1, t1 + delta) of busy
+         interval [t1, t2) does not exceed interference_bound_function(tsk, A, delta), where A is a 
+         relative arrival time of job j (with respect to time t1). 
+         Let's examine this definition in more detail. First, the IBF bounds the interference only
+         within the interval [t1, t1 + delta) (see a.1, a.2 below). Second, the IBF bounds the 
+         interference only until the job is completed, after which the function can behave 
+         arbitrarily (see b). And finally, the IBF function might depend not only on the length 
+         of the interval, but also on the relative arrival time of job j (see c). 
+         While (a.1), (a.2) and (b) are useful for discarding excessive cases, (c) adds 
+         flexibility to the IBF, which is important, for instance, when analyzing EDF scheduling. *)
+      Definition job_interference_is_bounded_by (interference_bound_function: Task -> time -> time -> time) := 
+        forall t1 t2 delta j,
+          busy_interval j t1 t2 ->                                                                        (* (a.1) *)
+          t1 + delta < t2 ->                                                                              (* (a.2) *)
+          arrives_in arr_seq j ->                                                            
+          job_task j = tsk ->                                                               
+          ~~ job_completed_by j (t1 + delta) ->                                                           (* (b) *)
+          let offset := job_arrival j - t1 in 
+          cumul_interference j t1 (t1 + delta) <= interference_bound_function tsk offset delta  (* (c) *).
+
+    End BusyIntervalProperties.
+    
+  End Definitions.    
+
+End AbstractRTADefinitions.
+
+  
\ No newline at end of file

model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job.
+Require Import rt.model.schedule.uni.schedule.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * Reduction of the serach space for Abstract RTA *)
+(** In this module, we prove that in order to calculate the worst-case response time 
+    it is sufficient to consider only values of A that lie in the search space defined below. *)  
+   
+Module AbstractRTAReduction. 
+
+  Import Epsilon UniprocessorSchedule.
+
+  (* The response-time analysis we are presenting in this series of documents is based on searching 
+     over all possible values of A, the relative arrival time of the job respective to the beginning 
+     of the busy interval. However, to obtain a practically useful response-time bound, we need to 
+     constrain the search space of values of A. In this section, we define an approach to 
+     reduce the search space. *)
+  Section SearchSpace.
+
+    Context {Task: eqType}.
+    
+    (* First, we provide a constructive notion of equivalent functions. *)
+    Section EquivalentFunctions.
+
+      (* Consider an arbitrary type T... *)
+      Context {T: eqType}.
+
+      (*  ...and two function from nat to T. *)
+      Variables f1 f2: nat -> T.
+
+      (* Let B be an arbitrary constant. *) 
+      Variable B: nat.
+      
+      (* Then we say that f1 and f2 are equivalent at values less than B iff
+         for any natural number x less than B [f1 x] is equal to [f2 x].  *)
+      Definition are_equivalent_at_values_less_than :=
+        forall x, x < B -> f1 x = f2 x.
+
+      (* And vice versa, we say that f1 and f2 are not equivalent at values 
+         less than B iff there exists a natural number x less than B such
+         that [f1 x] is not equal to [f2 x].  *)
+      Definition are_not_equivalent_at_values_less_than :=
+        exists x, x < B /\ f1 x <> f2 x.
+
+    End EquivalentFunctions. 
+
+    (* Let tsk be any task that is to be analyzed *)
+    Variable tsk: Task.
+    
+    (* To ensure that the analysis procedure terminates, we assume an upper bound B on 
+       the values of A that must be checked. The existence of B follows from the assumption 
+       that the system is not overloaded (i.e., it has bounded utilization). *)
+    Variable B: time.
+
+    (* Instead of searching for the maximum interference of each individual job, we 
+       assume a per-task interference bound function [IBF(tsk, A, x)] that is parameterized 
+       by the relative arrival time A of a potential job (see abstract_RTA.definitions.v file). *)
+    Variable interference_bound_function: Task -> time -> time -> time.
+
+    (* Recall the definition of ε, which defines the neighborhood of a point in the timeline.
+       Note that epsilon = 1 under discrete time. *)
+    (* To ensure that the search converges more quickly, we only check values of A in the interval 
+       [0, B) for which the interference bound function changes, i.e., every point x in which 
+       interference_bound_function (A - ε, x) is not equal to interference_bound_function (A, x). *)
+    Definition is_in_search_space A :=
+      A = 0 \/
+      0 < A < B /\ are_not_equivalent_at_values_less_than
+                     (interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.
+    
+    (* In this section we prove that for every A there exists a smaller A_sp 
+       in the search space such that interference_bound_function(A_sp,x) is 
+       equal to interference_bound_function(A, x). *)
+    Section ExistenceOfRepresentative.
+
+      (* Let A be any constant less than B. *) 
+      Variable A: time.
+      Hypothesis H_A_less_than_B: A < B.
+      
+      (* We prove that there exists a constant A_sp such that:
+         (a) A_sp is no greater than A, (b) interference_bound_function(A_sp, x) is 
+         equal to interference_bound_function(A, x) and (c) A_sp is in the search space.
+         In other words, either A is already inside the search space, or we can go 
+         to the "left" until we reach A_sp, which will be inside the search space. *)
+      Lemma representative_exists:
+        exists A_sp, 
+          A_sp <= A /\
+          are_equivalent_at_values_less_than (interference_bound_function tsk A)
+                                             (interference_bound_function tsk A_sp) B /\
+          is_in_search_space A_sp.
+      Proof.
+        induction A as [|n].
+        - exists 0; repeat split.
+            by rewrite /is_in_search_space; left.
+        - have ALT:
+            all (fun t => interference_bound_function tsk n t == interference_bound_function tsk n.+1 t) (iota 0 B)
+            \/ has (fun t => interference_bound_function tsk n t != interference_bound_function tsk n.+1 t) (iota 0 B).
+          { apply/orP.
+            rewrite -[_ || _]Bool.negb_involutive Bool.negb_orb.
+            apply/negP; intros CONTR.
+            move: CONTR => /andP [NALL /negP NHAS]; apply: NHAS.
+              by rewrite -has_predC /predC in NALL.
+          }
+          feed IHn; first by apply ltn_trans with n.+1. 
+          move: IHn => [ASP [NEQ [EQ SP]]].
+          move: ALT => [/allP ALT| /hasP ALT].
+          { exists ASP; repeat split; try done.
+            { by apply leq_trans with n. }
+            { intros x LT.
+              move: (ALT x) => T. feed T; first by rewrite mem_iota; apply/andP; split. 
+              move: T => /eqP T.
+                by rewrite -T EQ.
+            }
+          }
+          { exists n.+1; repeat split; try done.
+            rewrite /is_in_search_space; right.
+            split; first by  apply/andP; split.
+            move: ALT => [y IN N].
+            exists y.
+            move: IN; rewrite mem_iota add0n. move => /andP [_ LT]. 
+            split; first by done.
+            rewrite subn1 -pred_Sn.
+            intros CONTR; move: N => /negP N; apply: N.
+              by rewrite CONTR.
+          }
+      Qed.
+
+    End ExistenceOfRepresentative.
+
+    (* In this section we prove that any solution of the response-time recurrence for
+       a given point A_sp in the search space also gives a solution for any point 
+       A that shares the same interference bound. *)
+    Section FixpointSolutionForAnotherA.
+
+      (* Suppose A_sp + F_sp is a "small" solution (i.e. less than B) of the response-time recurrence. *)
+      Variables A_sp F_sp: time.
+      Hypothesis H_less_than: A_sp + F_sp < B.
+      Hypothesis H_fixpoint: A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).
+
+      (* Next, let A be any point such that: (a) A_sp <= A <= A_sp + F_sp and 
+         (b) interference_bound_function(A, x) is equal to 
+         interference_bound_function(A_sp, x) for all x less than B. *)
+      Variable A: time.
+      Hypothesis H_bounds_for_A: A_sp <= A <= A_sp + F_sp.
+      Hypothesis H_equivalent:
+        are_equivalent_at_values_less_than
+          (interference_bound_function tsk A)
+          (interference_bound_function tsk A_sp) B.
+
+      (* We prove that there exists a consant F such that [A + F] is equal to [A_sp + F_sp]
+         and [A + F] is a solution for the response-time recurrence for A. *)
+      Lemma solution_for_A_exists:
+        exists F,
+          A_sp + F_sp = A + F /\
+          F <= F_sp /\
+          A + F = interference_bound_function tsk A (A + F).
+      Proof.  
+        move: H_bounds_for_A => /andP [NEQ1 NEQ2].
+        set (X := A_sp + F_sp) in *.
+        exists (X - A); split; last split.
+        - by rewrite subnKC.
+        - by rewrite leq_subLR /X leq_add2r.
+        - by rewrite subnKC // H_equivalent.
+      Qed.
+
+    End FixpointSolutionForAnotherA.
+    
+  End SearchSpace.    
+  
+End AbstractRTAReduction.
+

model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job.
+Require Import rt.model.schedule.uni.service
+               rt.model.schedule.uni.schedule.
+Require Import rt.model.schedule.uni.limited.schedule
+               rt.model.schedule.uni.limited.abstract_RTA.definitions.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * Lock-in service of a job *)
+(** In this module, we provide a sufficient condition under which a job 
+    receives enough service to become nonpreemptive. *)
+Module AbstractRTALockInService. 
+
+  Import Job Epsilon UniprocessorSchedule Service  AbstractRTADefinitions.
+
+  (* Previously we defined the notion of lock-in service (see limited.schedule.v file). 
+     Lock-in service is the amount of service after which a job cannot be preempted until 
+     its completion. In this section we prove that if cumulative interference inside a 
+     busy interval is bounded by a certain constant then a job executes long enough to 
+     reach its lock-in service and become nonpreemptive. *)
+  Section LockInService.
+
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.    
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+    
+    (* Consider any arrival sequence with consistent arrivals... *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+    
+    (* Next, consider any uniprocessor schedule of this arrival sequence. *)
+    Variable sched: schedule Job.
+
+    (* Assume that the job costs are no larger than the task costs. *)
+    Hypothesis H_job_cost_le_task_cost:
+      cost_of_jobs_from_arrival_sequence_le_task_cost
+        task_cost job_cost job_task arr_seq. 
+
+    (* Let tsk be any task that is to be analyzed. *)
+    Variable tsk: Task.
+    
+    (* Assume we are provided with abstract functions for interference and interfering workload. *)
+    Variable interference: Job -> time -> bool.
+    Variable interfering_workload: Job -> time -> time.
+
+    (* For simplicity, let's define some local names. *)
+    Let work_conserving := work_conserving job_arrival job_cost job_task arr_seq sched tsk.
+    Let cumul_interference := cumul_interference interference.
+    Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
+    Let busy_interval := busy_interval job_arrival job_cost sched interference interfering_workload.
+    
+    (* We assume that the schedule is work-conserving. *)
+    Hypothesis H_work_conserving: work_conserving interference interfering_workload.
+
+    (* Let j be any job of task tsk with positive job cost. *)
+    Variable j: Job. 
+    Hypothesis H_j_arrives: arrives_in arr_seq j.
+    Hypothesis H_job_of_tsk: job_task j = tsk.
+    Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
+
+    (* Next, consider any busy interval [t1, t2) of job j. *)
+    Variable t1 t2: time.
+    Hypothesis H_busy_interval: busy_interval j t1 t2.
+
+    (* First, we prove that job j completes by the end of the busy interval. 
+       Note that the busy interval contains the execution of job j, in addition
+       time instant t2 is a quiet time. Thus by the definition of a quiet time
+       the job should be completed before time t2. *)
+    Lemma job_completes_within_busy_interval:
+      completed_by job_cost sched j t2.
+    Proof.
+      move: (H_busy_interval) => [[/andP [_ LT] [_ _]] [_ QT2]].
+      unfold pending, has_arrived in QT2.
+      move: QT2; rewrite  /pending negb_and; move => /orP [QT2|QT2].
+      { by move: QT2 => /negP QT2; exfalso; apply QT2, ltnW. }
+        by rewrite Bool.negb_involutive in QT2.
+    Qed.
+
+    (* In this section we show that the cumulative interference is a complement to 
+       the total time where job j is scheduled inside the busy interval. *)
+    Section InterferenceIsComplement.
+
+      (* Consider any subinterval [t, t + delta) inside the busy interval [t1, t2). *)
+      Variable t delta: time.
+      Hypothesis H_greater_than_or_equal: t1 <= t.
+      Hypothesis H_less_or_equal: t + delta <= t2.
+      
+      (* We prove that sum of cumulative service and cumulative interference 
+         in the interval [t, t + delta) is equal to delta. *)
+      Lemma interference_is_complement_to_schedule:
+        service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.
+      Proof. 
+        rewrite /service_during /cumul_interference.  
+        rewrite -big_split //=.
+        rewrite -{2}(sum_of_ones t delta).
+        apply/eqP; rewrite eqn_leq; apply/andP; split.
+        - rewrite [X in X <= _]big_nat_cond [X in _ <= X]big_nat_cond.
+          apply leq_sum; move => x /andP [/andP [GE2 LT2] _ ].
+          case IJX: (interference j x); last by rewrite addn0 /service_at; case scheduled_at. 
+          rewrite addn1 ltnNge; apply/negP; intros CONTR.
+          specialize (H_work_conserving j t1 t2 x).
+          feed_n 5 H_work_conserving; try done.
+          { apply/andP; split.
+            apply leq_trans with t; try done.
+            apply leq_trans with (t + delta); try done.
+          }
+          move: H_work_conserving => [H1 H2].
+          feed H2. rewrite lt0b in CONTR. by done.
+            by rewrite IJX in H2.
+        - rewrite [X in X <= _]big_nat_cond [X in _ <= X]big_nat_cond.
+          apply leq_sum; move => x /andP [/andP [GE2 LT2] _ ].
+          case IJX: (interference j x); first by rewrite addn1.
+          rewrite addn0.
+          specialize (H_work_conserving j t1 t2 x); feed_n 5 H_work_conserving; try done.
+          { apply/andP; split.
+            apply leq_trans with t; try done.
+            apply leq_trans with (t + delta); try done. }
+          move: H_work_conserving => [H1 H2].
+          feed H1; first by rewrite IJX.
+            by rewrite lt0b.
+      Qed.
+
+    End InterferenceIsComplement.
+
+    (* In this section, we prove a sufficient condition under which job j receives enough service. *)
+    Section InterferenceBoundedImpliesEnoughService.
+
+      (* Let progress_of_job be the desired service of job j. *)
+      Variable progress_of_job: time.
+      Hypothesis H_progress_le_job_cost: progress_of_job <= job_cost j.
+      
+      (* Assume that for some delta, the sum of desired progress and cumulative 
+         interference is bounded by delta (i.e., the supply). *)
+      Variable delta: time.
+      Hypothesis H_total_workload_is_bounded:
+        progress_of_job + cumul_interference j t1 (t1 + delta) <= delta.
+
+      (* Then, it must be the case that the job has received no less service than progress_of_job. *)
+      Theorem j_receives_at_least_lock_in_service: 
+        service sched j (t1 + delta) >= progress_of_job.
+      Proof.
+        case NEQ: (t1 + delta <= t2); last first.
+        { intros.
+          have L8 := job_completes_within_busy_interval.
+          move: L8 => /eqP L8.
+          rewrite /service.
+          rewrite (service_during_cat _ _ t2).
+          unfold service in L8. rewrite L8.
+          apply leq_trans with (job_cost j); first by auto. 
+          rewrite leq_addr //.
+            by apply/andP; split; last (apply negbT in NEQ; apply ltnW; rewrite ltnNge).
+        } 
+        { move: H_total_workload_is_bounded => BOUND.
+          apply subh3_ext in BOUND.
+          apply leq_trans with (delta - cumul_interference j t1 (t1 + delta)); first by done.
+          apply leq_trans with (service_during sched j t1 (t1 + delta)).
+          { rewrite -{1}[delta](interference_is_complement_to_schedule t1) //. 
+            rewrite -addnBA // subnn addn0 //.
+          }
+          { unfold service.
+            rewrite [X in _ <= X](service_during_cat _ _ t1).
+            rewrite leq_addl //.
+              by apply/andP; split; last rewrite leq_addr.
+          }
+        }
+      Qed.
+      
+    End InterferenceBoundedImpliesEnoughService.
+
+    (* In this section we prove a simple lemma about completion of 
+       a job after is reaches lock-in service. *)
+    Section CompletionOfJobAfterLockInService.
+
+      (* Assume that completed jobs do not execute. *)
+      Hypothesis H_completed_jobs_dont_execute:
+        completed_jobs_dont_execute job_cost sched.
+      
+      (* Consider a proper job lock-in service function, i.e... *)
+      Variable job_lock_in_service: Job -> time.
+
+      (* ...(1) for any job j the lock-in service of job j is positive... *)
+      Hypothesis H_lock_in_service_positive:
+        job_lock_in_service_positive job_cost arr_seq job_lock_in_service.
+      
+      (* ...(2) it also less-than-or-equal to the job_cost... *)
+      Hypothesis H_lock_in_service_le_job_cost:
+        job_lock_in_service_le_job_cost job_cost arr_seq job_lock_in_service.
+
+      (* ..., and (3) we assume that the scheduler respects the notion of the lock-in service. *)
+      Hypothesis H_job_nonpreemptive_after_lock_in_service:
+        job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service.
+
+      (* Then, job j must complete in [job_cost j - job_lock_in_service j] time 
+         units after it reaches lock-in service. *)
+      Lemma job_completes_after_reaching_lock_in_service:
+        forall t,
+          job_lock_in_service j <= service sched j t -> 
+          completed_by job_cost sched j (t + (job_cost j - job_lock_in_service j)).
+      Proof. 
+        move => t ES.
+        set (job_cost j - job_lock_in_service j) as job_last.
+        move: (H_job_nonpreemptive_after_lock_in_service j t) => LSNP. 
+        apply negbNE; apply/negP; intros CONTR.
+        have SCHED: forall t', t <= t' <= t + job_last -> scheduled_at sched j t'.
+        { move => t' /andP [GE LT].
+          rewrite -[t'](@subnKC t) //.
+          apply LSNP; [ by apply H_j_arrives | by rewrite leq_addr | by done | ].
+          rewrite subnKC //.
+          apply/negP; intros COMPL.
+          move: CONTR => /negP Temp; apply: Temp.
+          apply completion_monotonic with (t0 := t'); try done.
+        }
+        have SERV: job_last + 1 <= \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'.
+        { rewrite -{1}[job_last + 1]addn0  -{2}(subnn t) addnBA // addnC.
+          rewrite -{1}[_+_-_]addn0 -[_+_-_]mul1n -iter_addn -big_const_nat.
+          rewrite big_nat_cond [in X in _ <= X]big_nat_cond.
+          rewrite leq_sum //.
+          move => t' /andP [NEQ _].
+          rewrite /service_at lt0b.
+          apply SCHED.
+            by rewrite addn1 addnS ltnS in NEQ.
+        }
+        move: (H_completed_jobs_dont_execute j (t + job_last.+1)).
+        rewrite /completed_jobs_dont_execute.
+        rewrite leqNgt; move => /negP T; apply: T.
+        rewrite /service (service_during_cat _ _ t); last by (apply/andP; split; last rewrite leq_addr).
+        apply leq_trans with (
+          job_lock_in_service j + service_during sched j t (t + job_last.+1));
+          last by rewrite leq_add2r.
+        apply leq_trans with  (job_lock_in_service j + job_last.+1); last by rewrite leq_add2l /service_during -addn1.
+          by rewrite addnS ltnS subnKC; eauto 2.
+      Qed.
+ 
+    End CompletionOfJobAfterLockInService.
+    
+  End LockInService.
+
+End AbstractRTALockInService.
+