preserve Classic Prosa upon retirement

Preserve the Classic Prosa development as it is retired from the main
development branch.

Issue: #98

.gitlab-ci.yml

@@ -77,7 +77,7 @@ compile-and-doc:
     - .preferred-stable-version
   script:
     - !reference [.install-dependencies, script]
-    - ./create_makefile.sh --without-classic
+    - ./create_makefile.sh
     - make -j ${NJOBS}
     - !reference [.make-html, script]
   artifacts:
@@ -95,45 +95,13 @@ compile-and-doc-and-validate:
     - .preferred-stable-version
   script:
     - !reference [.install-dependencies, script]
-    - ./create_makefile.sh --without-classic
+    - ./create_makefile.sh
     - make -j ${NJOBS}
     - !reference [.make-html, script]
     - make validate 2>&1 | tee validation-results.txt
-    - scripts/check-validation-output.sh --accept-proof-irrelevance validation-results.txt
-  artifacts:
-    name: "prosa-spec-$CI_COMMIT_REF_NAME"
-    paths:
-      - "with-proofs/"
-      - "without-proofs/"
-      - "pretty/"
-    expire_in: 1 week
-
-# Check that proof irrelevance shows up only due to refinements.
-compile-and-validate:
-  stage: build
-  extends:
-    - .not_in_wip_branches
-    - .preferred-stable-version
-  script:
-    - !reference [.install-dependencies, script]
-    - ./create_makefile.sh --without-classic --without-refinements
-    - make -j ${NJOBS}    
-    - make validate 2>&1 | tee validation-results.txt
     - scripts/check-validation-output.sh validation-results.txt
-
-classic-compile-and-doc-and-validate:
-  stage: build
-  extends:
-    - .preferred-stable-version
-    - .not_in_wip_branches
-  script:
-    - !reference [.install-dependencies, script]
-    - ./create_makefile.sh --only-classic
-    - make -j ${NJOBS}
-    - !reference [.make-html, script]
-    - make validate
   artifacts:
-    name: "prosa-classic-spec-$CI_COMMIT_REF_NAME"
+    name: "prosa-spec-$CI_COMMIT_REF_NAME"
     paths:
       - "with-proofs/"
       - "without-proofs/"
@@ -146,42 +114,3 @@ proof-length:
   script:
     - scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
 
-spell-check:
-  extends:  
-    - .not_in_wip_branches  
-  stage: build
-  image: bbbrandenburg/aspell-ci
-  script:
-    - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`
-
-# mathcomp-dev with stable Coq
-#coq-8.15:
-#  extends:
-#    - .build-dev
-#    - .not_in_wip_branches    
-#  # it's ok to fail with an unreleased version of ssreflect
-#  allow_failure: true
-
-# mathcomp-dev with coq-dev
-#coq-dev:
-#  extends:
-#    - .build-dev
-#    - .not_in_wip_branches    
-#  # it's ok to fail with an unreleased version of ssreflect and Coq
-#  allow_failure: true
-
-proof-state:
-  extends:
-   - .not_in_wip_branches  
-  stage: build
-  image: bbbrandenburg/alectryon-ci:1.14.0-coq-8.15.0
-  script:
-    - eval $(opam env "--switch=${COMPILER_EDGE}" --set-switch)
-    - !reference [.install-dependencies, script]
-    - ./create_makefile.sh --without-classic
-    - make -j ${NJOBS} alectryon
-  artifacts:
-    name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
-    paths:
-      - "html-alectryon/"
-    expire_in: 1 week

README.md

-# Prosa: Formally Proven Schedulability Analysis
+# Classic Prosa (2015-2019)
 
-This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016. As of 2018, Prosa is primarily being developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (kindly funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
+---
 
-<center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
+**Deprecation warning:** Classic Prosa is no longer being maintained. Please base any new developments on "modern" Prosa. 
 
-## Documentation
+---
 
-Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:
+This branch preserves the *classic* version of the [Prosa open-source project](https://prosa.mpi-sws.org), as originally presented at ECRTS'16. This version of Prosa was developed from 2015 until 2019, and further maintained until 2022.
 
-- <https://prosa.mpi-sws.org/branches>
+Throughout 2018–2021, Prosa was developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
 
-## Publications
+<center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
 
-Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage. 
 
-## Directory and Module Structure
+As of now, classic Prosa has been superseded by "modern Prosa" (as tracked in the main branch of this repository), which is under active development. Classic Prosa is no longer being maintained. 
 
-The directory and module structure is organized as follows. First, the main parts, of which there are currently four.
+This branch serves to preserve a working snapshot based on **Coq 8.16** and **mathcomp 1.15.0**. 
 
-- [behavior/](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module. 
-- [model/](model/): The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected "pick and choose" whatever definitions and assumptions are appropriate.
-- [analysis/](analysis/): The `analysis` namespace collects all definitions and proof libraries needed to establish **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
-- [results/](results/): The `results` namespace contains all **high-level analysis results**. 
 
+## Documentation
 
-In future work, there will also (again) be an `implementation` or `examples` namespace in which important high-level results are instantiated (i.e., applied) in an assumption-free environment for concrete job and task types to establish the absence of any contradiction in assumptions.
+Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:
 
-Furthermore, there are a couple of additional folders and namespaces.
+- <https://prosa.mpi-sws.org/branches>
 
-- [classic/](classic/): This module contains the "classic" version of Prosa as first presented at ECRTS'16.  
-All results published prior to 2020 build on this "classic" version of Prosa.
-- [util/](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
-- [scripts/](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
+## Publications
 
-## Installation
+Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage. 
 
-### With OPAM
+All results published prior to 2020 build on this "classic" version of Prosa.
 
-Prosa can be installed using the [OPAM package manager](https://opam.ocaml.org/) (>= 2.0).
+## Installation
 
-```bash
-opam repo add coq-released https://coq.inria.fr/opam/released
-# or for the dev version (git master): https://coq.inria.fr/opam/extra-dev
-opam update
-opam install coq-prosa
-```
+First, make sure you have **Coq 8.16** and **mathcomp 1.15.0** installed.
 
 ### From Sources with `opam`
 
@@ -57,32 +45,6 @@ opam pin add -n -y -k path coq-prosa .
 opam install coq-prosa
 ```
 
-### From Sources With `esy`
-
-Prosa can be installed using [esy](https://esy.sh/).
-
-#### Installing `esy`
-
-`esy` itself can typically be installed through `npm`.
-It should look something like this on most `apt`-based systems:
-
-```bash
-sudo apt install npm
-sudo npm install --global esy@latest
-```
-
-#### Installing Prosa
-
-With `esy` in place, it is easy to compile Prosa in one go. To download and compile all of Prosa's dependencies (including Coq), and then to compile Prosa itself, simply issue the command:
-
-```bash
-esy
-```
-
-Note that `esy` uses an internal compilation environment, which is not exported to the current shell.
-To work within this environment, prefix any command with `esy`: for instance `esy coqide` to run your system’s coqIDE within the right environment.
-Alternatively, `esy shell` opens a shell within its environment.
-
 ### Manually From Sources
 
 #### Dependencies
@@ -91,16 +53,13 @@ Besides on Coq itself, Prosa depends on
 
 1. the `ssreflect` library of the [Mathematical Components project](https://math-comp.github.io),
 2. the [Micromega support for the Mathematical Components library](https://github.com/math-comp/mczify) provided by `mczify`, and
-3. the [The Coq Effective Algebra Library](https://github.com/coq-community/coqeal) (optional, needed only for POET-related refinements).
 
-These dependencies can be easily installed with OPAM.
+These dependencies can be easily installed with OPAM. 
 
 ```bash
-opam install -y coq-mathcomp-ssreflect coq-mathcomp-zify coq-coqeal
+opam install -y coq-mathcomp-ssreflect<=1.15.0 coq-mathcomp-zify
 ```
 
-Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.
-
 #### Compiling Prosa
 
 Assuming all dependencies are available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa consists of only two steps.
@@ -111,18 +70,6 @@ First, create an appropriate `Makefile`.
 ./create_makefile.sh
 ```
 
-Alternatively, to avoid compiling the older "classic" Prosa, specify the `--without-classic` option. This can speed up compilation considerably and is a good idea during development.  (It's also possible to *only* compile the "classic" Prosa by specifying the `--only-classic` option, but this is rarely needed.)
-
-```bash
-./create_makefile.sh --without-classic
-```
-
-To avoid compiling the POET-related refinements (which require CoqEAL to be installed and inject a dependency on the *proof irrelevance* axiom), specify the switch `--without-refinements`. For example, to skip both "classic" Prosa and the refinements library, use the following command:
-
-```bash
-./create_makefile.sh --without-classic --without-refinements
-```
-
 Second, compile the library.
 
 ```bash
@@ -139,29 +86,3 @@ The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/doc
 - `make gallinahtml -j` --- just the specification, without proofs,
 - `make html -j`  --- full specification with all proofs.
 
-
-Since Coqdoc requires object files (`*.vo`) as input, please make sure that the code is compilable.
-
-## Commit and Development Rules
-
-We very much welcome external contributions. Please don't hesitate to [get in touch](http://prosa.mpi-sws.org/get-in-touch.html)!
-
-To make things as smooth as possible, here are a couple of rules and guidelines that we seek to abide by.
-
-1. Always follow the project [coding and writing guidelines](doc/guidelines.md).
-
-2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times. 
-
-3. It's ok (and even recommended) to develop in a (private) dirty branch, but clean up and rebase (i.e., `git-rebase -i`) on top of the current master branch before opening a merge request.
-
-4. Create merge requests liberally. No improvement is too small or too insignificant for a merge request. This applies to documentation fixes (e.g., typo fixes, grammar fixes, clarifications, etc.)  as well.
-
-5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:". 
-
-6. We strive to have only "fast-forward merges" without merge commits, so always rebase your branch to linearize the history before merging. (WIP branches do not need to be linear.)
-
-7. Recommendation: Document the tactics that you use in the [list of tactics](doc/tactics.md), especially when introducing/using non-standard tactics.
-
-8. If something seems confusing, please help with improving the documentation. :-)
-
-9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discusion, please file a ticket. 

analysis/README.md

-# Prosa Analysis Library
-
-This module provides virtually all **analysis concepts and definitions** and encapsulates the bulk of the **intermediate proofs** in Prosa. 
-
-More precisely, this module collects all definitions that are not needed to define the behavioral semantics (found in [prosa.behavior](../behavior)) and that also do not conceptually form part of the task and system model (found in [prosa.model](../model)). For example, precise notions of "schedulability," "busy window," or "response time" are clearly analysis concepts and consequently defined here. 
-
-The proofs found in this module are "intermediate proofs" in the sense that they are not an end in of themselves; rather, they are a means to enable the proofs of the high-level results provided in the [prosa.results](../results) module.
-
-## Structure
-
-The Prosa analysis library is currently organized as follows:
-
-- [abstract](./abstract): This provides **abstract RTA** analysis framework, a general and extensible approach to response-time analysis (RTA).
-- [definitions](./definitions): This folder currently collects all major and minor **analysis definitions** (such as schedulability, priority inversion, etc.).
-- [transform](./transform): This folder contains procedures for transforming schedules, to be used in proofs that rely on modifying a given reference schedule in some way (e.g., the EDF "swapping argument").
-- [facts](./facts): Currently the home of virtually all **intermediate proofs**. In particular, [facts.behavior](./facts/behavior) provides a library of basic facts that follow (mostly) directly from Prosa's trace semantics (as given in [prosa.behavior](../behavior)).
-
-**NB**: It is expected that the analysis module will be further (re)organized and (re)structured in future versions of Prosa.
-
-## Guidelines
-
-- As a general rule, keep definitions and proofs separate, so that casual readers may read and understand the Prosa specification without encountering intermediate lemmas and proofs. 
-- Prefer subfolders with many short files over fewer, longer files. 
-- In each file that is specific to some system model, explicitly `Require` the specific modules that jointly constitute the assumed system model (e.g., `Require prosa.model.processor.ideal` to express that the results in a file depend on the ideal-uniprocessor assumption).
\ No newline at end of file

analysis/abstract/definitions.v

-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-Require Export prosa.model.task.concept.
-
-(** * 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 uni-processor scheduling of real-time tasks with arbitrary arrival models. *)
-Section AbstractRTADefinitions. 
-
-  (** In this section, we introduce all the abstract notions required by the analysis. *)
-  Section Definitions.
-
-    (** Consider any type of job associated with any type of tasks... *)
-    Context {Job : JobType}.
-    Context {Task : TaskType}.
-    Context `{JobTask Job Task}.
-
-    (** ... with arrival times and costs. *)
-    Context `{JobArrival Job}.
-    Context `{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 of this arrival sequence. *)
-    Variable sched : schedule PState.
-
-    (** Let [tsk] be any task that is to be analyzed *)
-    Variable tsk : Task.
-
-    (** 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 subsequent activation of a task can suffer from interference at 
-       the beginning 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 -> instant -> 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 -> instant -> duration.
-
-    (** 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 : instant) :=
-        cumul_interference j 0 t = cumul_interfering_workload j 0 t /\
-        ~~ pending_earlier_and_at sched 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 : instant) :=
-        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 : instant) :=
-        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).
-          }
-        } by subst t2'.
-      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_cost j > 0 ->
-          busy_interval j t1 t2 ->
-          t1 <= t < t2 ->
-          ~ interference j t <-> scheduled_at sched 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 system is overloaded.  Therefore, in
-          the later concrete analyses, we will have to introduce an additional
-          condition that rules out overload. *)
-      Definition busy_intervals_are_bounded_by L :=
-        forall j,
-          arrives_in arr_seq j ->
-          job_of_task tsk j ->
-          job_cost j > 0 ->
-          exists t1 t2,
-            t2 <= t1 + L /\
-            busy_interval j t1 t2.
-
-      (** Although we have defined the notion of cumulative interference of a job, it cannot 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 sub-interval [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]). *)
-      Definition job_interference_is_bounded_by (interference_bound_function: Task -> duration -> duration -> duration) :=
-        (** Let's examine this definition in more detail. *)
-        forall t1 t2 delta j,
-          (** First, we require [j] to be a job of task [tsk]. *)
-          arrives_in arr_seq j ->
-          job_of_task tsk j ->
-          (** Next, we require the IBF to bound the interference only within the interval <<[t1, t1 + delta)>>. *)
-          busy_interval j t1 t2 ->
-          t1 + delta < t2 ->
-          (** Next, we require the IBF to bound the interference only until the job is 
-             completed, after which the function can behave arbitrarily. *)
-          ~~ completed_by sched j (t1 + delta) ->
-          (** 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] (offset). *)
-          (** While the first three conditions are needed for discarding excessive cases, offset adds 
-             flexibility to the IBF, which is important, for instance, when analyzing EDF scheduling. *)
-          let offset := job_arrival j - t1 in 
-          cumul_interference j t1 (t1 + delta) <= interference_bound_function tsk offset delta.
-
-    End BusyIntervalProperties.
-
-  End Definitions.
-
-End AbstractRTADefinitions.

analysis/abstract/run_to_completion.v

-Require Export prosa.analysis.facts.model.service_of_jobs.
-Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
-Require Export prosa.analysis.abstract.definitions.
-
-(** * Run-to-Completion Threshold of a job *)
-(** In this module, we provide a sufficient condition under which a job
-    receives enough service to become non-preemptive. *)
-(** Previously we defined the notion of run-to-completion threshold (see file
-   abstract.run_to_completion_threshold.v). Run-to-completion threshold 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
-   run-to-completion threshold and become non-preemptive. *)
-Section AbstractRTARunToCompletionThreshold.
-  
-  (**  Consider any type of jobs. *)
-  Context {Job : JobType}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
-
-  (** In addition, we assume existence of a function
-     mapping jobs to their preemption points. *)
-  Context `{JobPreemptable Job}.
-
-  (** Consider any kind of uni-service ideal processor state model. *)
-  Context {PState : ProcessorState Job}.
-  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
-  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
-
-  (** Consider any arrival sequence with consistent arrivals ... *)
-  Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  
-  (** ... and any schedule of this arrival sequence. *)
-  Variable sched : schedule PState.
-  
-  (** Assume we are provided with abstract functions for interference and interfering workload. *)
-  Variable interference : Job -> instant -> bool.
-  Variable interfering_workload : Job -> instant -> duration.
-
-  (** For simplicity, let's define some local names. *)
-  Let work_conserving := work_conserving arr_seq sched.
-  Let cumul_interference := cumul_interference interference.
-  Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
-  Let busy_interval := busy_interval 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 cost. *)
-  Variable j : Job.
-  Hypothesis H_j_arrives : arrives_in arr_seq j.
-  Hypothesis H_job_cost_positive : job_cost_positive j.
-
-  (** Next, consider any busy interval <<[t1, t2)>> of job [j]. *)
-  Variable t1 t2 : instant.
-  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 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 sub-interval <<[t, t + delta)>> inside the busy interval [t1, t2). *)
-    Variables (t : instant) (delta : duration).
-    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/service_at.
-      rewrite -big_split //=.
-      rewrite -{2}(sum_of_ones t delta).
-      rewrite big_nat [in RHS]big_nat.
-      apply: eq_bigr=> x /andP[Lo Hi].
-      move: (H_work_conserving j t1 t2 x) => Workj.
-      feed_n 4 Workj; try done.
-      { by apply/andP; split; eapply leq_trans; eauto 2. }
-      destruct interference.
-      - replace (service_in _ _) with 0; auto; symmetry.
-        apply no_service_not_scheduled; auto.
-        now apply/negP; intros SCHED; apply Workj in SCHED; apply SCHED.
-      - replace (service_in _ _) with 1; auto; symmetry.
-        apply/eqP; rewrite eqn_leq; apply/andP; split.
-        + apply H_unit_service_proc_model.
-        + now apply H_ideal_progress_proc_model, Workj.
-    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 : duration.
-    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 : duration.
-    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_run_to_completion_threshold:
-      service sched j (t1 + delta) >= progress_of_job.
-    Proof.
-      case NEQ: (t1 + delta <= t2); last first.
-      { intros.
-        have L8 := job_completes_within_busy_interval.
-        apply leq_trans with (job_cost j); first by done.
-        rewrite /service.
-        rewrite -(service_during_cat _ _ _ t2).
-        apply leq_trans with (service_during sched j 0 t2); [by done | by rewrite leq_addr].
-          by apply/andP; split; last (apply negbT in NEQ; apply ltnW; rewrite ltnNge).
-      }
-      {  move: H_total_workload_is_bounded => BOUND.
-         rewrite addnC in BOUND.
-         apply leq_subRL_impl 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 //.
-         }
-         { rewrite /service -[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 run-to-completion threshold. *)
-  Section CompletionOfJobAfterRunToCompletionThreshold.
-
-    (** Assume that completed jobs do not execute ... *)
-    Hypothesis H_completed_jobs_dont_execute:
-      completed_jobs_dont_execute sched.
-
-    (** .. and the preemption model is valid. *)
-    Hypothesis H_valid_preemption_model:
-      valid_preemption_model arr_seq sched.
-
-    (** Then, job [j] must complete in [job_cost j - job_rtct j] time
-       units after it reaches run-to-completion threshold. *)
-    Lemma job_completes_after_reaching_run_to_completion_threshold:
-      forall t,
-        job_rtct j <= service sched j t ->
-        completed_by sched j (t + (job_cost j - job_rtct j)).
-    Proof.
-      move => t ES.
-      set (job_cost j - job_rtct j) as job_last.
-      have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
-                     Job H0 H1 _ arr_seq sched _ j _ t.
-      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) //.
-        eapply LSNP; eauto 2; first by rewrite leq_addr.
-        rewrite subnKC //.
-        apply/negP; intros COMPL.
-        move: CONTR => /negP Temp; apply: Temp.
-        exact: completion_monotonic COMPL.
-      }
-      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 _].
-        apply H_ideal_progress_proc_model; apply SCHED.
-          by rewrite addn1 addnS ltnS in NEQ.
-      }
-      move: (service_at_most_cost
-               _ H_completed_jobs_dont_execute j H_unit_service_proc_model
-               (t + job_last.+1)).
-      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_rtct j + service_during sched j t (t + job_last.+1));
-        last by rewrite leq_add2r.
-      apply leq_trans with  (job_rtct j + job_last.+1); last by rewrite leq_add2l /service_during -addn1.
-        by rewrite addnS ltnS subnKC //; eapply job_run_to_completion_threshold_le_job_cost; eauto.
-    Qed.
-
-  End CompletionOfJobAfterRunToCompletionThreshold.
-
-End AbstractRTARunToCompletionThreshold.

analysis/abstract/search_space.v

-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-Require Import prosa.util.epsilon.
-Require Import prosa.util.tactics.
-Require Import prosa.model.task.concept.
-
-(** * Reduction of the search space for Abstract RTA *)
-(** In this file, 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. *)  
-
-Section AbstractRTAReduction. 
-
-  (** 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. *)
-  
-  Context {Task : TaskType}.
-  
-  (** 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 : duration.
-
-  (** 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 -> duration -> duration -> duration.
-
-  (** Recall the definition of [ε], which defines the neighborhood of a point in the timeline.
-     Note that [ε = 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 : duration.
-    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 : duration.
-    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 : duration.
-    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 constant [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 AbstractRTAReduction. 

analysis/definitions/always_higher_priority.v

-Require Export prosa.model.priority.classes.
-
-(** * Always Higher Priority *)
-(** In this section, we define what it means for a job to always have
-    a higher priority than another job. *) 
-Section AlwaysHigherPriority.
- 
-  (** Consider any type of jobs ... *) 
-  Context {Job : JobType}.
-
-  (** ... and any JLDP policy. *) 
-  Context `{JLDP_policy Job}.
-  
-  (** We say that a job [j1] always has higher priority than job [j2]
-      if, at any time [t], the priority of job [j1] is strictly higher than
-      the priority of job [j2]. *)
-  Definition always_higher_priority (j1 j2 : Job) :=
-    forall t, hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1.  
-
-End AlwaysHigherPriority. 

analysis/definitions/busy_interval.v

-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}.    
-
-  (** 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.
-  
-  (** ... and a schedule of this arrival sequence. *)
-  Variable sched : schedule PState.
-  
-  (** Assume a given JLFP policy. *)
-  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. *)
-    Definition quiet_time (t : instant) :=
-      forall (j_hp : Job),
-        arrives_in arr_seq j_hp ->
-        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 
-         priority job is released and remains non-quiet. We also require
-         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. *)
-    Definition busy_interval (t1 t2 : instant) :=
-      busy_interval_prefix t1 t2 /\
-      quiet_time t2.
-
-  End BusyInterval.
-
-  (** In this section we define the computational
-      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. *)
-    Definition quiet_time_dec (j : Job) (t : instant) :=
-      all
-        (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. *)
-    Lemma quiet_time_P :
-      forall j t, reflect (quiet_time j t) (quiet_time_dec j t).
-    Proof.
-      intros; apply/introP.
-      - 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.
-      - move => /negP DEC; intros QT; apply: DEC.
-        apply/allP; intros s ARRs.
-        apply/implyP; intros HPs.
-        apply QT; try done.
-        + by apply in_arrivals_implies_arrived in ARRs.
-        + by eapply in_arrivals_implies_arrived_between in ARRs; eauto 2.
-    Qed.
-
-  End DecidableQuietTime.
-
-End BusyIntervalJLFP.

analysis/definitions/carry_in.v

-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 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, where each
-      job has an arrival time and a cost. *)
-  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobCost Job}.
-
-  (** 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.
-
-  (** ... 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 ->
-      arrived_before j_o t ->
-      completed_by sched j_o t.
-
-End NoCarryIn.

analysis/definitions/completion_sequence.v

-From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
-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/hyperperiod.v

-From mathcomp Require Import div.
-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/job_properties.v

-Require Export prosa.behavior.all.
-
-(** In this section, we introduce properties of a job. *)
-Section PropertiesOfJob.
-
-  (** Assume that job costs are known. *)
-  Context {Job : JobType}.
-  Context `{JobCost Job}.
-
-  (** Consider an arbitrary job. *)
-  Variable j : Job.
-
-  (** The job cost must be positive. *)
-  Definition job_cost_positive := job_cost j > 0.
-
-End PropertiesOfJob. 
\ No newline at end of file

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_inversion.v

-Require Export prosa.analysis.definitions.busy_interval.
-
-(** * 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}.
-  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 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
-      implicitly assumes that the scheduler is
-      work-conserving. Therefore, it cannot be applied to models with
-      jitter or self-suspensions. *)
-  Definition priority_inversion (t : instant) :=
-    ~~ scheduled_at sched j t /\
-      exists jlp,
-        scheduled_at sched jlp t && ~~ hep_job jlp j.
-
-  (** Similarly, we define a decidable counterpart of
-      [priority_inversion]. *)
-  Definition priority_inversion_dec (t : instant) :=
-    ~~ scheduled_at sched j t &&
-      has (fun jlp => scheduled_at sched jlp t && ~~ hep_job jlp j)
-          (arrivals_before arr_seq t.+1).
-
-  (** In the following short section we show that the propositional
-      and computational versions of [priority_inversion] are
-      equivalent. *)
-  Section PriorityInversionReflection.
-
-    (** We assume that all jobs come from the arrival sequence and do
-        not execute before their arrival nor after completion. *)
-    Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
-    Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-    Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-
-    (** Then the propositional and computational versions of
-        [priority_inversion] are equivalent.*)
-    Lemma priority_inversion_P :
-      forall t, reflect (priority_inversion t) (priority_inversion_dec t).
-    Proof.
-      intros t; apply /introP.
-      - move=> /andP [SCHED /hasP [jlp ARR PRIO]].
-        by split => //; (exists jlp).
-      - rewrite negb_and /priority_inversion; move=> /orP NPRIO.
-        destruct NPRIO as [NSCHED | NHAS].
-        + rewrite Bool.negb_involutive in NSCHED.
-          by rewrite NSCHED; intros [F _].
-        + move => [NSCHED [jlp /andP[SCHED_jlp NHEP]]].
-          move: NHAS => /hasPn NJOBS.
-          specialize (NJOBS jlp).
-          have ARR: jlp \in arrivals_before arr_seq t.+1.
-          { move: (H_jobs_must_arrive_to_execute jlp t SCHED_jlp) => ARR.
-            apply arrived_between_implies_in_arrivals => //=.
-            by apply (H_jobs_come_from_arrival_sequence jlp t).
-          }
-          move: (NJOBS ARR) => /negP NN.
-          by apply NN; apply /andP; split => //.
-    Qed.
-
-  End PriorityInversionReflection.
-
-  (** 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_dec t.
-
-  (** We say that the priority inversion experienced by a job [j] is
-      bounded by a constant [B] if the cumulative priority inversion
-      within any busy interval prefix is bounded by [B]. *)
-  Definition priority_inversion_of_job_is_bounded_by_constant (B : duration) :=
-    forall (t1 t2 : instant),
-      busy_interval_prefix arr_seq sched j t1 t2 ->
-      cumulative_priority_inversion t1 t2 <= B.
-
-  (** More generally, if 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).
-
-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 priority inversion of task [tsk] is bounded by a constant
-      [B] if all jobs released by the task have cumulative priority inversion
-      bounded by [B]. *)
-  Definition priority_inversion_is_bounded_by_constant (B : 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_constant arr_seq sched j B.
-
-  (** 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.
-
-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.
-
-(** * 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.
-  
-End ReadinessModelProperties.