analysis/definitions/blocking_bound/edf.v

+Require Export prosa.model.task.preemption.parameters.
+Require Export prosa.model.task.arrival.curves.
+
+(** * Blocking Bound for EDF *)
+(** In this section, we define a bound on the length of a
+    non-preemptive segment of a lower-priority job (w.r.t. a task
+    [tsk]) under EDF scheduling. *)
+Section MaxNPSegmentBlockingBound.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskDeadline Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** For clarity, let's denote the relative deadline of a task as [D]. *)
+  Let D tsk := task_deadline tsk.
+
+  (** Consider an arbitrary task set [ts]. *)
+  Variable ts : list Task.
+
+  (** Let [max_arrivals] be a family of arrival curves. *)
+  Context `{MaxArrivals Task}.
+
+  (** Only other tasks that potentially release non-zero-cost jobs are
+      relevant, so we define a predicate to exclude pathological
+      cases. *)
+  Definition blocking_relevant (tsk_o : Task) :=
+    (max_arrivals tsk_o ε > 0) && (task_cost tsk_o > 0).
+
+  (** For a job of a given task [tsk], the relative arrival offset [A]
+      within its busy window, we define the following blocking
+      bound. This bound assumes that task are independent (i.e., it
+      does not account for possible blocking due to locking
+      protocols). *)
+  Definition blocking_bound (tsk : Task) (A : duration)  :=
+    \max_(tsk_o <- ts | blocking_relevant tsk_o && (D tsk_o > D tsk + A))
+     (task_max_nonpreemptive_segment tsk_o - ε).
+
+End MaxNPSegmentBlockingBound.

analysis/definitions/blocking_bound/elf.v

+Require Export prosa.model.task.preemption.parameters.
+Require Export prosa.model.task.arrival.curves.
+Require Import prosa.model.priority.elf.
+
+(** * Blocking Bound for ELF *)
+(** In this section, we define a bound on the length of a
+    non-preemptive segment of a lower-priority job (w.r.t. a task
+    [tsk]) under ELF scheduling. *)
+Section MaxNPSegmentBlockingBound.
+
+  (** Consider any type of tasks ... *)
+  Context {Job : JobType}{Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** ... with relative priority points. *)
+  Context `{PriorityPoint Task}.
+
+  (** Consider an arbitrary task set [ts]. *)
+  Variable ts : list Task.
+
+  (** Let [max_arrivals] be a family of arrival curves. *)
+  Context `{MaxArrivals Task}.
+
+  (** Consider any FP policy. *)
+  Context {FP : FP_policy Task}.
+
+  (** Only other tasks that potentially release non-zero-cost jobs are
+      relevant, so we define a predicate to exclude pathological
+      cases. *)
+  Let blocking_relevant (tsk_o : Task) :=
+    (max_arrivals tsk_o ε > 0) && (task_cost tsk_o > 0).
+
+  (** Now we define a predicate to only include [blocking_relevant] tasks
+      that have a lower priority than [tsk]. *)
+  Let lp_tsk_blocking_relevant (tsk : Task) (tsk_o : Task) :=
+    (hp_task tsk tsk_o) && (blocking_relevant tsk_o).
+
+  (** Next we define a predicate for filtering [blocking_relevant] tasks
+      that have the same priority as [tsk]. *)
+  Let ep_tsk_blocking_relevant (tsk : Task) (tsk_o : Task) (A : duration) :=
+    let ep_tsk_j_blocking_relevant :=  (task_priority_point tsk_o > A%:R +  task_priority_point tsk)%R in
+      (ep_task tsk tsk_o) && ep_tsk_j_blocking_relevant && (blocking_relevant tsk_o).
+
+  (** For a job of a given task [tsk], given the relative arrival offset [A]
+      within its busy window, we define the following blocking
+      bound. This bound assumes that task are independent (i.e., it
+      does not account for possible blocking due to locking
+      protocols). *)
+  Definition blocking_bound (tsk : Task) (A : duration)  :=
+    \max_(tsk_o <- ts | lp_tsk_blocking_relevant tsk tsk_o || ep_tsk_blocking_relevant tsk tsk_o A)
+      (task_max_nonpreemptive_segment tsk_o - ε).
+
+End MaxNPSegmentBlockingBound.

analysis/definitions/blocking_bound/fp.v

+Require Export prosa.model.task.preemption.parameters.
+
+(** * Blocking Bound for FP *)
+(** In this section, we define a bound on the length of a
+    non-preemptive segment of a lower-priority job (w.r.t. a task
+    [tsk]) under FP scheduling. *)
+Section MaxNPSegmentBlockingBound.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** Consider an FP policy. *)
+  Context {FP : FP_policy Task}.
+
+  (** Consider an arbitrary task set [ts]. *)
+  Variable ts : list Task.
+
+  (** Assuming that tasks are independent, the maximum non-preemptive
+      segment length w.r.t. any lower-priority task bounds the maximum
+      possible duration of priority inversion. *)
+  Definition blocking_bound (tsk : Task) :=
+    \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
+     (task_max_nonpreemptive_segment tsk_other - ε).
+
+End MaxNPSegmentBlockingBound.

restructuring/analysis/definitions/busy_interval.v → analysis/definitions/busy_interval/classical.v

-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.schedule.work_conserving.
-
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.model.priority.classes.
+Require Export prosa.analysis.facts.behavior.completion.
 
 (** * Busy Interval for JLFP-models *)
 (** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
 Section BusyIntervalJLFP.
-  
+
   (** Consider any type of jobs. *)
   Context {Job : JobType}.
   Context `{JobArrival Job}.
-  Context `{JobCost Job}.    
+  Context `{JobCost Job}.
 
-  (** Consider any arrival sequence with consistent arrivals. *)
+  (** Consider any kind of processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
-  Variable sched : schedule (ideal.processor_state Job).
-  
+
+  (** ... and a schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
   (** Assume a given JLFP policy. *)
-  Variable higher_eq_priority : JLFP_policy Job. 
+  Context `{JLFP_policy Job}.
 
   (** In this section, we define the notion of a busy interval. *)
   Section BusyInterval.
-    
+
     (** Consider any job j. *)
     Variable j : Job.
     Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
-    
-    (** We say that t is a quiet time for j iff every higher-priority job from
-         the arrival sequence that arrived before t has completed by that time. *)
+
+    (** We say that [t] is a quiet time for [j] iff every higher-priority job from
+         the arrival sequence that arrived before [t] has completed by that time. *)
     Definition quiet_time (t : instant) :=
       forall (j_hp : Job),
         arrives_in arr_seq j_hp ->
-        higher_eq_priority j_hp j ->
+        hep_job j_hp j ->
         arrived_before j_hp t ->
         completed_by sched j_hp t.
-    
+
     (** Based on the definition of quiet time, we say that interval
-         [t1, t_busy) is a (potentially unbounded) busy-interval prefix
-         iff the interval starts with a quiet time where a higher or equal 
+         <<[t1, t_busy)>> is a (potentially unbounded) busy-interval prefix
+         iff the interval starts with a quiet time where a higher or equal
          priority job is released and remains non-quiet. We also require
-         job j to be released in the interval. *)    
+         job [j] to be released in the interval. *)
     Definition busy_interval_prefix (t1 t_busy : instant) :=
       t1 < t_busy /\
       quiet_time t1 /\
       (forall t, t1 < t < t_busy -> ~ quiet_time t) /\
       t1 <= job_arrival j < t_busy.
 
-    (** 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. *)
+    (** 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 (t1 t2 : instant) :=
       busy_interval_prefix t1 t2 /\
       quiet_time t2.
@@ -62,14 +59,14 @@ Section BusyIntervalJLFP.
   End BusyInterval.
 
   (** In this section we define the computational
-       version of the notion of quiet time. *)
+      version of the notion of quiet time. *)
   Section DecidableQuietTime.
 
-    (** We say that t is a quiet time for j iff every higher-priority job from
-         the arrival sequence that arrived before t has completed by that time. *)
+    (** We say that t is a quiet time for [j] iff every higher-priority job from
+        the arrival sequence that arrived before [t] has completed by that time. *)
     Definition quiet_time_dec (j : Job) (t : instant) :=
       all
-        (fun j_hp => higher_eq_priority j_hp j ==> (completed_by sched j_hp t))
+        (fun j_hp => hep_job j_hp j ==> (completed_by sched j_hp t))
         (arrivals_before arr_seq t).
 
     (** We also show that the computational and propositional definitions are equivalent. *)
@@ -80,16 +77,16 @@ Section BusyIntervalJLFP.
       - intros QT s ARRs HPs BEFs.
         move: QT => /allP QT.
         specialize (QT s); feed QT.
-        eapply arrived_between_implies_in_arrivals; eauto 2.
-          by move: QT => /implyP Q; apply Q in HPs.
+        + by eapply arrived_between_implies_in_arrivals; eauto 2.
+        + by move: QT => /implyP Q; apply Q in HPs.
       - move => /negP DEC; intros QT; apply: DEC.
         apply/allP; intros s ARRs.
         apply/implyP; intros HPs.
-        apply QT; try done.
+        apply QT => //.
         + by apply in_arrivals_implies_arrived in ARRs.
         + by eapply in_arrivals_implies_arrived_between in ARRs; eauto 2.
     Qed.
 
   End DecidableQuietTime.
 
-End BusyIntervalJLFP.
\ No newline at end of file
+End BusyIntervalJLFP.

analysis/definitions/busy_interval/edf_pi_bound.v

+Require Export prosa.model.task.preemption.parameters.
+Require Export prosa.analysis.definitions.sbf.sbf.
+Require Export prosa.analysis.definitions.request_bound_function.
+
+(** * Bound for a Busy-Interval Starting with Priority Inversion under EDF Scheduling *)
+
+(** In this file, we define a bound on the length of a busy interval
+    that starts with priority inversion (w.r.t. a job of a given task
+    under analysis) under the EDF scheduling policy. *)
+Section BoundedBusyIntervalUnderEDF.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskDeadline Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** Consider an arrival curve [max_arrivals]. *)
+  Context `{MaxArrivals Task}.
+
+  (** For brevity, let's denote the relative deadline of a task as [D]. *)
+  Let D tsk := task_deadline tsk.
+
+  (** Consider an arbitrary task set [ts] ... *)
+  Variable ts : seq Task.
+
+  (** ... and let [tsk] be any task to be analyzed. *)
+  Variable tsk : Task.
+
+  (** Assume that there is a job [j] of task [tsk] and that job [j]'s
+      busy interval starts with priority inversion. Then, the busy
+      interval can be bounded by a constant
+      [longest_busy_interval_with_pi]. *)
+
+  (** Intuitively, such a bound holds because of the following two
+      observations. (1) The presence of priority inversion implies an
+      upper bound on the job arrival offset [A < D tsk_o - D tsk],
+      where [A] is the time elapsed between the arrival of [j] and the
+      beginning of the corresponding busy interval. (2) An upper bound
+      on the offset implies an upper bound on the
+      higher-or-equal-priority workload of each task. *)
+  Definition longest_busy_interval_with_pi :=
+
+    (** Let [lp_interference tsk_lp] denote the maximum service
+        inversion caused by task [tsk_lp]. *)
+    let lp_interference tsk_lp :=
+      task_max_nonpreemptive_segment tsk_lp - ε in
+
+    (** Let [hep_interference tsk_lp] denote the maximum higher-or-equal
+        priority workload released within [D tsk_lp]. *)
+    let hep_interference tsk_lp :=
+      \sum_(tsk_hp <- ts | D tsk_hp <= D tsk_lp)
+       task_request_bound_function tsk_hp (D tsk_lp - D tsk_hp) in
+
+    (** Then, the amount of interfering workload incurred by a job of
+        task [tsk] is bounded by maximum of [lp_interference tsk_lp +
+        hep_interference tsk_lp], where [tsk_lp] is such that [D
+        tsk_lp > D tsk]. *)
+    \max_(tsk_lp <- ts | D tsk_lp > D tsk)
+     (lp_interference tsk_lp + hep_interference tsk_lp).
+
+End BoundedBusyIntervalUnderEDF.

restructuring/analysis/definitions/no_carry_in.v → analysis/definitions/carry_in.v

-Require Export rt.util.all.
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.analysis.basic_facts.all.
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.concept.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.model.priority.classes.
 
 (** * No Carry-In *)
-(** In this module we define the notion of no carry-in time for uniprocessor schedulers. *)
+(** In this module, we define the notion of a time without any carry-in work. *)
 Section NoCarryIn.
-  
+
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
 
-  (**  ... and any type of jobs associated with these tasks. *)
-  Context {Job : JobType}.
-  Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.    
+  (** ... and any type of jobs associated with these tasks, where each
+      job has an arrival time and a cost. *)
+  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobCost Job}.
 
-  (** Consider any arrival sequence with consistent arrivals. *)
+  (** Consider any arrival sequence of such jobs with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
-  Variable sched : schedule (ideal.processor_state Job).
 
-  (** The processor has no carry-in at time t iff every job (regardless of priority) 
-      from the arrival sequence released before t has completed by that time. *)
+  (** ... and the resultant schedule. *)
+  Context {PState : ProcessorState Job}.
+  Variable sched : schedule PState.
+
+  (** There is no carry-in at time [t] iff every job (regardless of priority)
+      from the arrival sequence released before [t] has completed by that time. *)
   Definition no_carry_in (t : instant) :=
     forall j_o,
       arrives_in arr_seq j_o ->

analysis/definitions/completion_sequence.v

+Require Import prosa.behavior.service.
+
+(** This module contains basic definitions and properties of job
+    completion sequences. *)
+
+(** * Notion of a Completion Sequence *)
+
+(** We begin by defining a job completion sequence. *)
+Section CompletionSequence.
+
+  (** Consider any kind of jobs with a cost
+     and any kind of processor state. *)
+  Context {Job : JobType} `{JobCost Job} {PState : ProcessorState Job}.
+
+  (** Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** For each instant [t], the completion sequence returns all
+     arrived jobs that have completed at [t]. *)
+  Definition completion_sequence : arrival_sequence Job :=
+    fun t => [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
+
+End CompletionSequence.

analysis/definitions/delay_propagation.v

+Require Export prosa.model.task.arrival.curves.
+
+(** * Arrival Curve Propagation *)
+
+Section ArrivalCurvePropagation.
+
+  (** In the following, consider two kinds of tasks, [Task1] and [Task2]. We
+      seek to relate the arrivals of jobs of the [Task1] kind to the arrivals of
+      jobs of the [Task2] kind. In particular, we will derive an arrival curve
+      for the second kind from an arrival curve for the first kind under the
+      assumption that job arrivals are related in time within some known delay
+      bound. *)
+  Context {Task1 Task2 : TaskType}.
+
+  (** Consider the corresponding jobs and their arrival times. *)
+  Context {Job1 Job2 : JobType}
+          `{JobTask Job1 Task1} `{JobTask Job2 Task2}
+          `(JobArrival Job1) `(JobArrival Job2).
+
+  (** Suppose there is a mapping of jobs (respectively, tasks) of the second
+      kind to jobs (respectively, tasks) of the first kind. For example, this
+      could be a "predecessor" or "triggered by" relationship. *)
+  Variable job1_of : Job2 -> Job1.
+  Variable task1_of : Task2 -> Task1.
+
+ (** Furthermore, suppose that the arrival time of any job of the second kind
+     occurs within a bounded time of the arrival of the corresponding job of the
+     first kind. *)
+  Variable delay_bound : Task2 -> duration.
+
+  (** ** Propagation Validity *)
+
+  (** Before we continue, let us note under which assumptions delay propagation
+      works. *)
+
+  (** First, the task- and job-level mappings of course need to agree. *)
+  Let consistent_task_job_mapping :=
+    forall j2 : Job2,
+      job_task (job1_of j2) = task1_of (job_task j2).
+
+  (** Second, the delay bound must indeed bound the separation between any two
+      jobs (for a given task set). *)
+  Let bounded_arrival_delay (ts : seq Task2) :=
+    forall (j2 : Job2),
+      (job_task j2) \in ts ->
+      job_arrival j2 <= job_arrival (job1_of j2) + delay_bound (job_task j2).
+
+  (** In summary, a delay propagation mapping is valid for a given task set [ts]
+      if it both is structurally consistent ([consistent_task_job_mapping]) and
+      ensures bounded arrival delay ([bounded_arrival_delay]). *)
+  Definition valid_delay_propagation_mapping (ts : seq Task2) :=
+    consistent_task_job_mapping /\ bounded_arrival_delay ts.
+
+  (** ** Derived Arrival Curve *)
+
+  (** Under the above assumptions, given an arrival curve for the first kind of
+      tasks ... *)
+  Context `{MaxArrivals Task1}.
+
+  (** ... we define an arrival curve for the second kind of tasks by "enlarging"
+      the analysis window by [delay_bound] ... *)
+  Let propagated_max_arrivals (tsk2 : Task2) (delta : duration) :=
+    if delta is 0 then 0
+    else max_arrivals (task1_of tsk2) (delta + delay_bound tsk2).
+
+  (** .. and register this definition with Coq as a type class instance. *)
+  #[local]
+  Instance propagated_arrival_curve : MaxArrivals Task2 := propagated_max_arrivals.
+
+  (** ** Derived Arrival Sequence *)
+
+  (** In a similar fashion, we next derive an arrival sequence of
+      jobs of the second kind. *)
+
+  (** To this end, suppose we are given an arrival sequence for jobs of the
+      first kind. *)
+  Variable arr_seq1 : arrival_sequence Job1.
+
+  (** Furthermore, suppose we are given the inverse mapping of jobs, i.e., a
+      function that maps each job in the arrival sequence to the corresponding
+      job(s) of the second kind, ...  *)
+  Variable job2_of : Job1 -> seq Job2.
+
+  (** ... and a function mapping each job of the second kind to the _exact_
+      delay that it incurs (relative to the arrival of its corresponding job of
+      the first kind). *)
+  Variable arrival_delay : Job2 -> duration.
+
+  (** Based on this information, we define the resulting arrival sequence of
+      jobs of the second kind. *)
+  Definition propagated_arrival_sequence t :=
+    let all := [seq job2_of j | j <- arrivals_up_to arr_seq1 t] in
+    [seq j2 <- flatten all | job_arrival (job1_of j2) +  arrival_delay j2 == t].
+
+  (** The derived arrival sequence makes sense under the following assumptions: *)
+
+  (** First, [job1_of] and [job2_of] must agree. *)
+  Let consistent_job_mapping :=
+    forall j1 j2,
+      j2 \in job2_of j1 <-> job1_of j2 = j1.
+
+  (** Second, the inverse mapping must be a proper set for each job in [arr_seq1]. *)
+  Definition job_mapping_uniq :=
+    forall j1,
+      arrives_in arr_seq1 j1 -> uniq (job2_of j1).
+
+  (** Third, the claimed bound on arrival delay must indeed bound all delays
+      encountered. *)
+  Let valid_arrival_delay (ts : seq Task2) :=
+    forall j2,
+      (job_task j2) \in ts ->
+      arrives_in arr_seq1 (job1_of j2) ->
+      arrival_delay j2 <= delay_bound (job_task j2).
+
+  (** Fourth, the arrival delay must indeed be the difference between the arrival
+      times of related jobs. *)
+  Let valid_job_arrival_def :=
+    forall j2,
+      job_arrival j2 = job_arrival (job1_of j2) + arrival_delay j2.
+
+  (** In summary, the derived arrival sequence is valid for a given task set
+      [ts] if all four above conditions are met. *)
+  Definition valid_arr_seq_propagation_mapping (ts : seq Task2) :=
+    [/\ consistent_job_mapping,job_mapping_uniq, valid_arrival_delay ts
+                                                & valid_job_arrival_def].
+
+End ArrivalCurvePropagation.
+
+(** * Release Jitter Propagation *)
+
+(** Under some scheduling policies, notably fixed-priority scheduling, it can be
+    useful to "fold" release jitter into the arrival curve. This can be achieved
+    in terms of the above-defined propagation operation. *)
+
+(** To this end, recall the definition of release jitter. *)
+Require Export prosa.model.task.jitter.
+
+(** In the following, we instantiate the above-defined delay propagation for
+    release jitter. *)
+
+Section ReleaseJitterPropagation.
+
+  (** Consider any type of tasks described by arrival curves ... *)
+  Context {Task : TaskType} `{MaxArrivals Task}.
+
+  (** ... and the corresponding jobs. *)
+  Context {Job : JobType} `{JobTask Job Task}.
+
+  (** Let [original_arrival] denote each job's _actual_ arrival time. *)
+  Context {original_arrival : JobArrival Job}.
+
+  (** Suppose the jobs are affected by bounded release jitter. *)
+  Context `{TaskJitter Task} `{JobJitter Job}.
+
+  (** Recall that a job's _release time_ is the first time after its arrival
+      when it becomes ready for execution. *)
+  Let job_release j := job_arrival j + job_jitter j.
+
+  (** If we _reinterpret_ release times as the _effective_ arrival times ... *)
+  #[local]
+  Instance release_as_arrival : JobArrival Job := job_release.
+
+  (** ... then we obtain a valid "arrival" (= release) curve for this
+      reinterpretation by propagating the original arrival curve while
+      accounting for the jitter bounds. *)
+  #[local]
+  Instance release_curve : MaxArrivals Task :=
+    propagated_arrival_curve id task_jitter.
+
+  (** By construction, this meets the delay-propagation validity
+      requirement. *)
+  Remark jitter_delay_mapping_valid :
+    forall ts,
+      valid_jitter_bounds ts ->
+      valid_delay_propagation_mapping
+        original_arrival release_as_arrival
+        id id task_jitter ts.
+  Proof.
+    move=> ts VALJIT; split => j // IN.
+    rewrite {1}/job_arrival /release_as_arrival /job_release.
+    exact/leq_add/VALJIT.
+  Qed.
+
+  (** Similarly, the induced "arrival" (= release) sequence ... *)
+  Definition release_sequence (arr_seq : arrival_sequence Job) :=
+    propagated_arrival_sequence original_arrival id arr_seq (fun j => [:: j]) job_jitter.
+
+  (** ... meets all requirements of the generic delay-propagation
+      construction. *)
+  Remark jitter_arr_seq_mapping_valid :
+    forall ts arr_seq,
+      valid_jitter_bounds ts ->
+      valid_arr_seq_propagation_mapping
+        original_arrival release_as_arrival
+        id task_jitter arr_seq (fun j => [:: j]) job_jitter ts.
+  Proof.
+    move=> ts arr_seq VALJIT; split => //.
+    - by move=> j1 j2; split => [|->]; rewrite mem_seq1 // => /eqP.
+    - by move=> j2 IN ARR; exact/VALJIT.
+  Qed.
+
+End ReleaseJitterPropagation.

analysis/definitions/demand_bound_function.v

+Require Export prosa.analysis.definitions.request_bound_function.
+
+(** * Demand Bound Function (DBF) *)
+(** Here we define Baruah et al.'s classic notion of a demand bound function,
+    generalized to arbitrary arrival curves. *)
+Section DemandBoundFunction.
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+
+  (** Suppose each task is characterized by a WCET, a relative deadline, and an arrival curve. *)
+  Context `{TaskCost Task} `{TaskDeadline Task} `{MaxArrivals Task}.
+
+  (** A task's DBF is its request-bound function (RBF) shifted by [task_deadline tsk - 1] time units. *)
+  Definition task_demand_bound_function (tsk : Task) (delta : duration) :=
+    let delta' := delta - (task_deadline tsk - 1) in
+      task_request_bound_function tsk delta'.
+
+  (** A task set's total demand bound function is simply the sum of each task's DBF.*)
+  Definition total_demand_bound_function (ts: seq Task) (delta : duration) :=
+    \sum_(tsk <- ts) task_demand_bound_function tsk delta.
+
+End DemandBoundFunction.

analysis/definitions/finish_time.v

+Require Export prosa.behavior.service.
+
+(** * Finish Time of a Job *)
+
+(** In this file, we define a job's precise finish time.
+
+    Note that in general a job's finish time may not be defined: if a job never
+    finishes in a given schedule, it does not have a finish time. To get around
+    this, we define a job's finish time under the assumption that _some_ (not
+    necessarily tight) response-time bound [R] is known for the job.
+
+    Under this assumption, we can simply re-use ssreflect's existing [ex_minn]
+    search mechanism (for finding the minimum natural number satisfying a given
+    predicate given a witness that some natural number satisfies the predicate)
+    and benefit from the existing corresponding lemmas. This file briefly
+    illustrates how this can be done. *)
+
+Section JobFinishTime.
+
+  (** Consider any type of jobs with arrival times and costs ... *)
+  Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.
+
+  (** ... and any schedule of such jobs. *)
+  Context {PState : ProcessorState Job}.
+  Variable sched : schedule PState.
+
+  (** Consider an arbitrary job [j]. *)
+  Variable j : Job.
+
+  (** In the following, we proceed under the assumption that [j] finishes
+      eventually (i.e., no later than [R] time units after its arrival, for any
+      finite [R]). *)
+  Variable R : nat.
+  Hypothesis H_response_time_bounded : job_response_time_bound sched j R.
+
+  (** For technical reasons, we restate the response-time assumption explicitly
+      as an existentially quantified variable. *)
+  #[local] Corollary job_finishes : exists t, completed_by sched j t.
+  Proof. by exists (job_arrival j + R); exact: H_response_time_bounded. Qed.
+
+  (** We are now ready for the main definition: job [j]'s finish time is the
+      earliest time [t] such that [completed_by sched j t] holds. This time can
+      be computed with ssreflect's [ex_minn] utility function, which is
+      convenient because then we can reuse the corresponding lemmas. *)
+  Definition finish_time : instant := ex_minn job_finishes.
+
+  (** In the following, we demonstrate the reuse of [ex_minn] properties by
+      establishing three natural properties of a job's finish time. *)
+
+  (** First, a job is indeed complete at its finish time. *)
+  Corollary finished_at_finish_time : completed_by sched j finish_time.
+  Proof.
+    rewrite /finish_time/ex_minn.
+    by case: find_ex_minn.
+  Qed.
+
+  (** Second, a job's finish time is the earliest time that it is complete. *)
+  Corollary earliest_finish_time :
+    forall t,
+      completed_by sched j t ->
+      finish_time <= t.
+  Proof.
+    move=> t COMP.
+    rewrite /finish_time/ex_minn.
+    by case: find_ex_minn.
+  Qed.
+
+  (** Third, Prosa's notion of [completes_at] is satisfied at the finish time. *)
+  Corollary completes_at_finish_time :
+    completes_at sched j finish_time.
+  Proof.
+    apply/andP; split; last exact: finished_at_finish_time.
+    apply/orP; case FIN: finish_time; [by right|left].
+    apply: contra_ltnN => [?|];
+      first by apply: earliest_finish_time.
+    by lia.
+  Qed.
+
+  (** Finally, we can define a job's precise response time as usual as the time
+      from its arrival until its finish time. *)
+  Definition response_time : duration := finish_time - job_arrival j.
+
+End JobFinishTime.

analysis/definitions/hyperperiod.v

+Require Export prosa.model.task.arrival.periodic.
+Require Export prosa.util.lcmseq.
+
+(** In this file we define the notion of a hyperperiod for periodic tasks. *)
+Section Hyperperiod.
+
+  (** Consider any type of periodic tasks ... *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** ... and any task set [ts]. *)
+  Variable ts : TaskSet Task.
+
+  (** The hyperperiod of a task set is defined as the least common multiple
+      (LCM) of the periods of all tasks in the task set. **)
+  Definition hyperperiod : duration := lcml (map task_period ts).        
+
+End Hyperperiod.
+
+(** In this section we provide basic definitions concerning the hyperperiod
+    of all tasks in a task set. *)
+Section HyperperiodDefinitions.
+
+  (** Consider any type of periodic tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskOffset Task}.
+  Context `{PeriodicModel Task}.
+
+  (** ... and any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** Consider any task set [ts] ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and any arrival sequence [arr_seq]. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** Let [O_max] denote the maximum offset of all tasks in [ts] ... *)
+  Let O_max := max_task_offset ts.
+
+  (** ... and let [HP] denote the hyperperiod of all tasks in [ts]. *)
+  Let HP := hyperperiod ts.
+
+  (** We define a hyperperiod index based on an instant [t]
+      which lies in it. *)
+  (** Note that we consider the first hyperperiod to start at time [O_max], 
+      i.e., shifted by the maximum offset (and not at time zero as can also 
+      be found sometimes in the literature) *)
+  Definition hyperperiod_index (t : instant) :=
+    (t - O_max) %/ HP.
+
+  (** Given an instant [t], we define the starting instant of the hyperperiod 
+   that contains [t]. *)
+  Definition starting_instant_of_hyperperiod (t : instant) :=
+    hyperperiod_index t * HP + O_max.
+
+  (** Given a job [j], we define the starting instant of the hyperperiod
+   in which [j] arrives. *)
+  Definition starting_instant_of_corresponding_hyperperiod (j : Job) :=
+    starting_instant_of_hyperperiod (job_arrival j).
+
+  (** We define the sequence of jobs of a task [tsk] that arrive in a hyperperiod
+      given the starting instant [h] of the hyperperiod. *)
+  Definition jobs_in_hyperperiod (h : instant) (tsk : Task) :=
+    task_arrivals_between arr_seq tsk h (h + HP).
+
+  (** We define the index of a job [j] of task [tsk] in a hyperperiod starting at [h]. *)
+  Definition job_index_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
+    index j (jobs_in_hyperperiod h tsk).
+
+  (** Given a job [j] of task [tsk] and the hyperperiod starting at [h], we define a 
+      [corresponding_job_in_hyperperiod] which is the job that arrives in given hyperperiod 
+      and has the same [job_index] as [j]. *)
+  Definition corresponding_job_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
+    nth j (jobs_in_hyperperiod h tsk) (job_index_in_hyperperiod j (starting_instant_of_corresponding_hyperperiod j) tsk).
+
+End HyperperiodDefinitions.

analysis/definitions/infinite_jobs.v

+Require Export prosa.model.task.arrivals.
+
+(** In this section we define the notion of an infinite release 
+    of jobs by a task. *)
+Section InfiniteJobs.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** Consider any arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** We say that a task [tsk] releases an infinite number of jobs 
+      if for every integer [n] there exists a job [j] of task [tsk]
+      such that [job_index] of [j] is equal to [n]. *)
+  Definition infinite_jobs :=
+    forall tsk n,
+    exists j,
+      arrives_in arr_seq j /\
+      job_task j = tsk /\
+      job_index arr_seq j = n.
+  
+End InfiniteJobs.

analysis/definitions/interference.v

+Require Export prosa.analysis.definitions.service.
+Require Export prosa.model.aggregate.workload.
+
+(** * Interference and Interfering Workload *)
+
+(** In the following, we introduce definitions of interference,
+    interfering workload and a function that bounds cumulative
+    interference. *)
+Section Definitions.
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType} {jt : JobTask Job Task} {jc : JobCost Job}.
+
+  (** Consider any kind of processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Definitions of interference for FP policies. *)
+  Section FPDefinitions.
+    Context {FP : FP_policy Task}.
+
+    (** We first define interference from higher-priority tasks. *)
+    Definition hp_task_interference (j : Job) (t : instant) :=
+      has (fun jhp => hp_task (job_task jhp) (job_task j)
+                      && receives_service_at sched jhp t)
+        (arrivals_up_to arr_seq t).
+
+    Context {JLFP : JLFP_policy Job}.
+
+    (** Then, to define interference from equal-priority tasks, we first
+        define higher-or-equal-priority jobs from an equal-priority task... *)
+    Definition ep_task_hep_job j1 j2 :=
+      hep_job j1 j2 && ep_task (job_task j1) (job_task j2).
+
+    (** ... and higher-or-equal-priority-jobs of equal-priority tasks that
+        do not stem from the same task. *)
+    Definition other_ep_task_hep_job j1 j2 :=
+      ep_task_hep_job j1 j2 && (job_task j1 != job_task j2).
+
+    (** This enables us to define interference from equal-priority tasks. *)
+    Definition hep_job_from_other_ep_task_interference (j : Job) (t : instant) :=
+      has (other_ep_task_hep_job^~ j) (served_jobs_at arr_seq sched t).
+
+    (** Similarly, to define interference from strictly higher-priority tasks, we first
+        define higher-or-equal-priority jobs from a strictly higher-priority task, which... *)
+    Definition hp_task_hep_job :=
+      fun j1 j2 => hep_job j1 j2 && (hp_task (job_task j1) (job_task j2)).
+
+    (** ... enables us to define interference from strictly higher-priority tasks. *)
+    Definition hep_job_from_hp_task_interference (j : Job) (t : instant) :=
+      has (hp_task_hep_job^~ j) (served_jobs_at arr_seq sched t).
+
+    (** Using the above definitions, we define the cumulative interference incurred in the interval
+        <<[t1, t2)>> from (1) higher-or-equal-priority jobs from strictly higher-priority tasks... *)
+    Definition cumulative_interference_from_hep_jobs_from_hp_tasks (j : Job) (t1 t2 : instant) :=
+      \sum_(t1 <= t < t2) hep_job_from_hp_task_interference j t.
+
+    (** ... and (2) higher-or-equal-priority jobs from equal-priority tasks. *)
+    Definition cumulative_interference_from_hep_jobs_from_other_ep_tasks (j : Job) (t1 t2 : instant) :=
+      \sum_(t1 <= t < t2) hep_job_from_other_ep_task_interference j t.
+
+  End FPDefinitions.
+
+  (** Definitions of interference for JLFP policies. *)
+  Section JLFPDefinitions.
+
+    (** Consider a JLFP-policy that indicates a higher-or-equal priority
+        relation. *)
+    Context {JLFP : JLFP_policy Job}.
+
+    (** We say that job [j] is incurring interference from another
+        job with higher-or-equal priority at time [t] if there exists a
+        job [jhp] (different from [j]) with a higher-or-equal priority
+        that executes at time [t]. *)
+    Definition another_hep_job_interference (j : Job) (t : instant) :=
+      has (another_hep_job^~ j) (served_jobs_at arr_seq sched t).
+
+    (** Similarly, we say that job [j] is incurring interference from a
+        job with higher-or-equal priority of another task at time [t]
+        if there exists a job [jhp] (of a different task) with
+        higher-or-equal priority that executes at time [t]. *)
+    Definition another_task_hep_job_interference (j : Job) (t : instant) :=
+      has (another_task_hep_job^~ j) (served_jobs_at arr_seq sched t).
+
+    (** Similarly, we say that job [j] is incurring interference from a
+        job with higher-or-equal priority of the same task at time [t]
+        if there exists another job [jhp] (of the same task) with
+        higher-or-equal priority that executes at time [t]. *)
+    Definition another_hep_job_of_same_task_interference (j : Job) (t : instant) :=
+      has (fun jhp => another_hep_job_of_same_task jhp j
+                      && receives_service_at sched jhp t)
+        (arrivals_up_to arr_seq t).
+
+    (** Now, we define the notion of cumulative interfering workload,
+        called [other_hep_jobs_interfering_workload], that says how many
+        units of workload are generated by jobs with higher-or-equal
+        priority released at time [t]. *)
+    Definition other_hep_jobs_interfering_workload (j : Job) (t : instant) :=
+      \sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.
+
+    (** For each of the concepts defined above, we introduce a
+        corresponding cumulative function: *)
+
+    (** (a) cumulative interference from other jobs with higher-or-equal priority ... *)
+    Definition cumulative_another_hep_job_interference (j : Job) (t1 t2 : instant) :=
+      \sum_(t1 <= t < t2) another_hep_job_interference j t.
+
+    (** ... (b) and cumulative interference from jobs with higher or
+        equal priority from other tasks, ... *)
+    Definition cumulative_another_task_hep_job_interference (j : Job) (t1 t2 : instant) :=
+      \sum_(t1 <= t < t2) another_task_hep_job_interference j t.
+
+    (** ... and (c) cumulative workload from jobs with higher or equal priority. *)
+    Definition cumulative_other_hep_jobs_interfering_workload (j : Job) (t1 t2 : instant) :=
+      \sum_(t1 <= t < t2) other_hep_jobs_interfering_workload j t.
+
+  End JLFPDefinitions.
+
+End Definitions.

restructuring/analysis/definitions/job_properties.v → analysis/definitions/job_properties.v

-Require Export rt.restructuring.behavior.all.
-From mathcomp Require Export eqtype ssrnat.
+Require Export prosa.behavior.all.
 
 (** In this section, we introduce properties of a job. *)
 Section PropertiesOfJob.

analysis/definitions/job_response_time.v

+Require Export prosa.behavior.all.
+
+(** In this section we define what it means for the response time 
+    of a job to exceed some given duration. *)
+Section JobResponseTimeExceeds.
+
+  (** Consider any kind of jobs ... *)
+  Context {Job : JobType}.
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+
+  (** ... and any kind of processor state. *)
+  Context `{PState : ProcessorState Job}.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** We say that a job [j] has a response time exceeding a number [x] 
+      if [j] is pending [x] units of time after its arrival. *)
+  Definition job_response_time_exceeds (j : Job) (x : duration) :=
+    ~~ completed_by sched j ((job_arrival j) + x).
+
+End JobResponseTimeExceeds.

analysis/definitions/priority/classes.v

+Require Export prosa.model.priority.classes.
+
+(** We define properties linking JLFP and FP policies. *)
+Section JLFP_FP.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (**  ... and any type of jobs associated with these tasks, ... *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+
+  (** Consider any pair of JLFP and FP policies. *)
+  Context (JLFP : JLFP_policy Job) (FP : FP_policy Task).
+
+  (** A JLFP policy is compatible with a FP policy if the priority
+      of the first on jobs doesn't contradict the priority of the
+      second on tasks. *)
+  Definition JLFP_FP_compatible :=
+    (forall j1 j2, hep_job j1 j2 -> hep_task (job_task j1) (job_task j2))
+    /\ (forall j1 j2, hp_task (job_task j1) (job_task j2) -> hep_job j1 j2).
+
+End JLFP_FP.

analysis/definitions/priority_inversion.v

+Require Export prosa.analysis.definitions.busy_interval.classical.
+Require Export prosa.analysis.facts.model.scheduled.
+
+(** * Priority Inversion *)
+(** In this section, we define the notion of priority inversion for
+    arbitrary processors. *)
+Section PriorityInversion.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Next, consider _any_ kind of processor state model, ... *)
+  Context {PState : ProcessorState Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Assume a given JLFP policy. *)
+  Context `{JLFP_policy Job}.
+
+  (** Consider an arbitrary job. *)
+  Variable j : Job.
+
+  (** We say that the job incurs priority inversion if it has higher
+      priority than the scheduled job. Note that this definition is
+      oblivious to whether job [j] is ready. Therefore, it may not
+      apply as intuitively expected in models with jitter or
+      self-suspensions. Further generalization of the concept is
+      likely necessary to efficiently analyze models in which jobs may
+      be pending without being ready. *)
+  Definition priority_inversion (t : instant) :=
+    (j \notin scheduled_jobs_at arr_seq sched t)
+    && has (fun jlp => ~~ hep_job jlp j) (scheduled_jobs_at arr_seq sched t).
+
+  (** Similarly we define priority inversion occurring only due to jobs
+      satisfying the predicate [P]. In other words, the lower-priority job
+      scheduled instead of [j] satisfies the predicate [P]. *)
+  Definition priority_inversion_cond (P : pred Job) (t : instant) :=
+    (j \notin scheduled_jobs_at arr_seq sched t)
+    && has (fun jlp => ~~ hep_job jlp j && P jlp) (scheduled_jobs_at arr_seq sched t).
+
+  (** Cumulative priority inversion incurred by a job within some time
+      interval <<[t1, t2)>> is the total number of time instances
+      within <<[t1,t2)>> at which job [j] incurred priority
+      inversion. *)
+  Definition cumulative_priority_inversion (t1 t2 : instant) :=
+    \sum_(t1 <= t < t2) priority_inversion t.
+
+  (** Cumulative priority inversion incurred by a job from jobs satisfying
+      a predefined condition [P] within some time interval <<[t1, t2)>>
+      is the total number of time instances within <<[t1, t2)>>
+      at which job [j] incurred priority inversion due to jobs satisfying [P]. *)
+  Definition cumulative_priority_inversion_cond (P : pred Job) (t1 t2 : instant) :=
+    \sum_(t1 <= t < t2) priority_inversion_cond P t.
+
+  (** Suppose the priority inversion experienced by job [j] depends on
+      its relative arrival time w.r.t. the beginning of its busy
+      interval at a time [t1]. We say that the priority inversion of
+      job [j] is bounded by a function [B : duration -> duration] if
+      the cumulative priority inversion within any busy interval
+      prefix is bounded by [B (job_arrival j - t1)]. *)
+  Definition priority_inversion_of_job_is_bounded_by (B : duration -> duration) :=
+    forall (t1 t2 : instant),
+      busy_interval_prefix arr_seq sched j t1 t2 ->
+      cumulative_priority_inversion t1 t2 <= B (job_arrival j - t1).
+
+  (** We define a similar notion as defined above for the priority
+      inversion that is experienced by a job due to jobs satisfying
+      the predicate [P]. *)
+  Definition priority_inversion_of_job_cond_is_bounded_by (P : pred Job) (B : duration -> duration) :=
+    forall (t1 t2 : instant),
+      busy_interval_prefix arr_seq sched j t1 t2 ->
+      cumulative_priority_inversion_cond P t1 t2 <= B (job_arrival j - t1).
+
+End PriorityInversion.
+
+(** In this section, we define a notion of the bounded priority inversion for tasks. *)
+Section TaskPriorityInversionBound.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Next, consider _any_ kind of processor state model, ... *)
+  Context {PState : ProcessorState Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Assume a given JLFP policy. *)
+  Context `{JLFP_policy Job}.
+
+  (** Consider an arbitrary task [tsk]. *)
+  Variable tsk : Task.
+
+  (** We say that task [tsk] has bounded priority inversion if all its
+      jobs have bounded cumulative priority inversion that depends on
+      its relative arrival time w.r.t. the beginning of the busy
+      interval. *)
+  Definition priority_inversion_is_bounded_by (B : duration -> duration) :=
+    forall (j : Job),
+      arrives_in arr_seq j ->
+      job_of_task tsk j ->
+      job_cost j > 0 ->
+      priority_inversion_of_job_is_bounded_by arr_seq sched j B.
+
+  (** Analogous to the above definition, we say that task [tsk] has bounded
+      priority inversion from jobs satisfying a predicate [P] if all its
+      jobs have bounded cumulative priority inversion that depends on its
+      relative arrival time w.r.t. the beginning of the busy interval. *)
+  Definition priority_inversion_cond_is_bounded_by (P: pred Job) (B : duration -> duration) :=
+    forall (j : Job),
+      arrives_in arr_seq j ->
+      job_of_task tsk j ->
+      job_cost j > 0 ->
+      priority_inversion_of_job_cond_is_bounded_by arr_seq sched j P B.
+
+End TaskPriorityInversionBound.

analysis/definitions/progress.v

+Require Export prosa.analysis.facts.behavior.service.
+
+(** * Job Progress (or Lack Thereof) *)
+
+(** In the following section, we define a notion of "job progress", and
+    conversely a notion of a lack of progress. *)
+
+Section Progress.
+  
+  (** Consider any type of jobs with a known cost... *)
+  Context {Job : JobType}.
+  Context `{JobCost Job}.
+
+  (** ... and any kind of schedule. *)
+  Context {PState : ProcessorState Job}.
+
+  (** For a given job and a given schedule... *)
+  Variable sched : schedule PState.
+  Variable j : Job.
+
+  Section NotionsOfProgress.
+
+    (** ...and two ordered points in time... *)
+    Variable t1 t2 : nat.
+    Hypothesis H_t1_before_t2: t1 <= t2.
+
+    (** ... we say that the job has progressed between the two points iff its
+        total received service has increased. *)
+    Definition job_has_progressed := service sched j t1 < service sched j t2.
+
+    (** Conversely, if the accumulated service does not change, there is no
+        progress. *)
+    Definition no_progress := service sched j t1 == service sched j t2.
+
+    (** We note that the negation of the former is equivalent to the latter
+        definition. *)
+    Lemma no_progress_equiv: ~~ job_has_progressed <-> no_progress.
+    Proof.
+      rewrite /job_has_progressed /no_progress.
+      split.
+      { rewrite -leqNgt leq_eqVlt => /orP [EQ|LT]; first by rewrite eq_sym.
+        exfalso.
+        have MONO: service sched j t1 <= service sched j t2
+          by apply service_monotonic.
+        have NOT_MONO: ~~ (service sched j t1 <= service sched j t2)
+          by apply /negPf; apply ltn_geF.
+        move: NOT_MONO => /negP NOT_MONO.
+        contradiction. }
+      { move => /eqP ->.
+        rewrite -leqNgt.
+        by apply service_monotonic. }
+    Qed.
+
+  End NotionsOfProgress.
+
+  (** For convenience, we define a lack of progress also in terms of given
+      reference point [t] and the length of the preceding interval of
+      inactivity [delta], meaning that no progress has been made for at least
+      [delta] time units. *)
+  Definition no_progress_for (t : instant) (delta : duration) := no_progress (t - delta) t.
+
+End Progress.

analysis/definitions/readiness.v

+Require Export prosa.behavior.ready.
+Require Export prosa.analysis.definitions.schedule_prefix.
+Require Export prosa.model.preemption.parameter.
+Require Export prosa.model.priority.classes.
+Require Export prosa.model.task.sequentiality.
+
+(** * Properties of Readiness Models *)
+
+(** In this file, we define commonsense properties of readiness models. *)
+Section ReadinessModelProperties.
+
+  (** For any type of jobs with costs and arrival times ... *)
+  Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
+
+  (** ... and any kind of processor model, ... *)
+  Context {PState: ProcessorState Job}.
+
+  (** ... consider a  notion of job readiness. *)
+  Variable ReadinessModel : JobReady Job PState.
+
+  (** First, we define a notion of non-clairvoyance for readiness
+      models. Intuitively, whether a job is ready or not should depend only on
+      the past (i.e., prior allocation decisions and job behavior), not on
+      future events. Formally, we say that the [ReadinessModel] is
+      non-clairvoyant if a job's readiness at a given time does not vary across
+      schedules with identical prefixes. That is, given two schedules [sched]
+      and [sched'], the predicates [job_ready sched j t] and [job_ready sched'
+      j t] may not differ if [sched] and [sched'] are identical prior to time
+      [t]. *)
+  Definition nonclairvoyant_readiness :=
+    forall sched sched' j h,
+      identical_prefix sched sched' h ->
+      forall t,
+        t <= h ->
+        job_ready sched j t = job_ready sched' j t.
+
+  (** Next, we relate the readiness model to the preemption model. *)
+  Context `{JobPreemptable Job}.
+
+  (** In a preemption-policy-compliant schedule, nonpreemptive jobs must remain
+      scheduled. Further, in a valid schedule, scheduled jobs must be
+      ready. Consequently, in a valid preemption-policy-compliant schedule, a
+      nonpreemptive job must remain ready until at least the end of its
+      nonpreemptive section. *)
+  Definition valid_nonpreemptive_readiness sched :=
+     forall j t,
+        ~~ job_preemptable j (service sched j t) -> job_ready sched j t.
+
+  (** For the next definition, consider the tasks from which the jobs stem. *)
+  Context {Task : TaskType}.
+  Context `{JobTask Job Task}.
+
+  (** We say a readiness model is sequential iff only a task's earliest
+      incomplete job is ready, meaning that later jobs can be executed only
+      after all earlier jobs have been completed. *)
+  Definition sequential_readiness (arr_seq : arrival_sequence Job) :=
+    forall sched j t,
+      job_ready sched j t -> prior_jobs_complete arr_seq sched j t.
+
+End ReadinessModelProperties.
+
+

analysis/definitions/request_bound_function.v

+Require Export prosa.model.task.arrival.curves.
+Require Export prosa.model.priority.classes.
+Require Export prosa.analysis.facts.priority.classes.
+Require Export prosa.util.sum.
+
+(** * Request Bound Function (RBF) *)
+
+(** We define the notion of a task's request-bound function (RBF), as well as
+    the total request bound function of a set of tasks. *)
+
+Section TaskWorkloadBoundedByArrivalCurves.
+
+  (** Consider any type of task characterized by a WCET bound and an arrival curve. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task} `{MaxArrivals Task}.
+
+  (** ** RBF of a Single Task *)
+
+  (** We define the classic notion of an RBF, which for a given task [tsk]
+      and interval length [Δ], bounds the maximum cumulative processor demand
+      of all jobs released by [tsk] in any interval of length [Δ]. *)
+  Definition task_request_bound_function (tsk : Task) (Δ : duration) :=
+    task_cost tsk * max_arrivals tsk Δ.
+
+  (** ** Total RBF of Multiple Tasks *)
+
+  (** Next, we extend the notion of an RBF to multiple tasks in the obvious way. *)
+
+  (** Consider a set of tasks [ts]. *)
+  Variable ts : seq Task.
+
+  (** The joint total RBF of all tasks in [ts] is simply the sum of each task's RBF. *)
+  Definition total_request_bound_function (Δ : duration) :=
+    \sum_(tsk <- ts) task_request_bound_function tsk Δ.
+
+  (** For convenience, we additionally introduce specialized notions of total RBF for use 
+      under FP scheduling that consider only certain tasks.
+      relation. *)
+  Context `{FP_policy Task}.
+
+  (** We define the following bound for the total workload of
+      tasks of higher-or-equal priority (with respect to [tsk]) in any interval
+      of length Δ. *)
+  Definition total_hep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
+    \sum_(tsk_other <- ts | hep_task tsk_other tsk)
+     task_request_bound_function tsk_other Δ.
+
+  (** We also define a bound for the total workload of higher-or-equal-priority
+      tasks other than [tsk] in any interval of length [Δ]. *)
+  Definition total_ohep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
+    \sum_(tsk_other <- ts | hep_task tsk_other tsk && (tsk_other != tsk))
+      task_request_bound_function tsk_other Δ.
+
+  (** We also define a bound for the total workload of higher-or-equal-priority
+      tasks other than [tsk] in any interval of length [Δ]. *)
+  Definition total_ep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
+    \sum_(tsk_other <- ts | ep_task tsk_other tsk)
+      task_request_bound_function tsk_other Δ.
+
+  (** Finally, we define a bound for the total workload of higher-priority
+      tasks in any interval of length [Δ]. *)
+  Definition total_hp_request_bound_function_FP (tsk : Task) (Δ : duration) :=
+    \sum_(tsk_other <- ts | hp_task tsk_other tsk)
+     task_request_bound_function tsk_other Δ.
+
+End TaskWorkloadBoundedByArrivalCurves.