Commit 2545ffb9 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

retire classic Prosa

Remove the classic module from the source tree, to speed up CI and to
avoid having to maintain it going forward as we adopt newer Coq and
mathcomp versions.

Issue: #98
parent f7a3ae37
Pipeline #74402 passed with stage
in 10 minutes and 52 seconds
......@@ -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,7 +95,7 @@ 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
......@@ -116,30 +116,11 @@ compile-and-validate:
- .preferred-stable-version
script:
- !reference [.install-dependencies, script]
- ./create_makefile.sh --without-classic --without-refinements
- ./create_makefile.sh --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"
paths:
- "with-proofs/"
- "without-proofs/"
- "pretty/"
expire_in: 1 week
proof-length:
stage: build
image: python:3-alpine
......@@ -152,7 +133,7 @@ spell-check:
stage: build
image: bbbrandenburg/aspell-ci
script:
- scripts/flag-typos-in-comments.sh `find . -iname '*.v' ! -path './classic/*'`
- scripts/flag-typos-in-comments.sh `find . -iname '*.v'`
# mathcomp-dev with stable Coq
#coq-8.15:
......@@ -178,7 +159,7 @@ proof-state:
script:
- eval $(opam env "--switch=${COMPILER_EDGE}" --set-switch)
- !reference [.install-dependencies, script]
- ./create_makefile.sh --without-classic
- ./create_makefile.sh
- make -j ${NJOBS} alectryon
artifacts:
name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
......
# Prosa: Formally Proven Schedulability Analysis
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).
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.
From 2018–201, Prosa was furter 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).
<center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
Prosa continues to be maintained and developed by the MPI-SWS Real-Time Systems group and contributors. Patches and merge requests are very welcome!
## Documentation
Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:
......@@ -14,23 +18,26 @@ Up-to-date documentation for all branches of the main Prosa repository is availa
Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage.
## Directory and Module Structure
### Classic Prosa
All results published prior to 2020 used the "classic" version of Prosa as first presented at ECRTS'16. Classic Prosa has been superseded by this development and is no longer being maintained. Refer to [the `classic-prosa` branch](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/classic-prosa) to find this original version of Prosa.
The directory and module structure is organized as follows. First, the main parts, of which there are currently four.
## Directory and Module Structure
- [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**.
The directory and module structure is organized as follows. First, the main parts, of which there are currently six.
- [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. These models are *axiomatic* in the sense that they are collections of hypotheses and not necessarily backed by concrete implementations (but see below).
- [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**.
- [implementation](implementation/): This module collects concrete implementations of some of the axiomatic models and scheduling policies to which the results apply. These are used to instantiate (i.e., apply) high-level results in an assumption-free environment for concrete job and task types, which establishes the absence of contradictions in the axiomatic models refined by the implementations.
- [implementation.refinements](implementation/refinements/): The refinements needed by [POET](https://drops.dagstuhl.de/opus/volltexte/2022/16336/) to compute with large numbers, based on [CoqEAL](https://github.com/coq-community/CoqEAL).
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.
Furthermore, there are a couple of additional folders and namespaces.
- [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.
- [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.
## Installation
......@@ -111,16 +118,10 @@ 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:
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:
```bash
./create_makefile.sh --without-classic --without-refinements
./create_makefile.sh --without-refinements
```
Second, compile the library.
......
# Classic Prosa
This module contains the Coq specification & proof development of the Prosa project as presented in the ECRTS'16 paper by Cerqueira et al.
- Felipe Cerqueira, Felix Stutz, and Björn Brandenburg, “[Prosa: A Case for Readable Mechanized Schedulability Analysis](https://www.mpi-sws.org/~bbb/papers/pdf/ecrts16f.pdf)”, *Proceedings of the 28th Euromicro Conference on Real-Time Systems (ECRTS 2016)*, pp. 273–284, July 2016.
This "classic" version of Prosa has since been superseded by a restructuring and refactoring effort that took place throughout most of 2019 in the context of the [RT-Proofs project](https://rt-proofs.inria.fr/) (kindly funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
For the sake of historical completeness, and since not all "classic" proofs have (yet) been ported to the new Prosa base, "classic" Prosa is still included in the master branch of Prosa of the time being.
## Directory Structure
The Classic Prosa directory was intended to be organized in a hierarchy: while generic, reusable foundations stay in the upper levels, definitions for specific analyses may be found deeper in the directory tree. However, this organizational principle is not consistently followed due to historical developments.
### Base Directories
Classic Prosa contains the following base directories:
- **classic/model/:** Specification of task and scheduler models, as well as generic lemmas related to scheduling.
- **classic/analysis/:** Definition, proofs and implementation of schedulability analyses.
- **classic/implementation/:** Instantiation of each schedulability analysis with concrete task and scheduler implementations.
Instantiating the main theorems in an assumption free environment shows the absence of contradictory assumptions in the proofs.
- **classic/util/:** additional helper lemmas, notations, and tactics that are no longer used in the "new Prosa".
### Internal Directories
The major concepts in classic Prosa are specified in the *classic/model/* folder.
- **classic/model/arrival:** Arrival sequences and arrival bounds
- **classic/model/schedule:** Definitions and properties of schedules
Inside *classic/model/schedule*, one can find the different classes of schedulers.
- **classic/model/schedule/uni:** Uniprocessor scheduling.
- **classic/model/schedule/global:** Global scheduling.
- **classic/model/schedule/partitioned:** Partitioned scheduling.
- **classic/model/schedule/apa:** APA scheduling.
For example, the schedulability analysis for global scheduling with release jitter is organized as follows.
- **classic/model/schedule/global/jitter:** Definitions and lemmas for global scheduling with release jitter.
- **classic/analysis/global/jitter:** Analysis for global scheduling with release jitter.
- **classic/implementation/global/jitter:** Implementation of the concrete scheduler with release jitter.
## Extending Prosa
Please do not extend this classic version of Prosa in ongoing or future work. As of 2019, all efforts should now be focused on the new, restructured base.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.analysis.apa.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundGeneric.
Section Definitions.
Import Schedule WorkloadBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
Variable num_cpus: nat.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
Let task_with_response_time := (sporadic_task * time)%type.
(* Assume a known response-time bound for each interfering task ... *)
Variable R_prev: seq task_with_response_time.
(* ... and an interval length delta. *)
Variable delta: time.
Section PerTask.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
(* Based on the workload bound, Bertogna and Cirinei define the
following interference bound for a task. *)
Definition interference_bound_generic :=
minn (W task_cost task_period tsk_other R_other delta) (delta - (task_cost tsk) + 1).
End PerTask.
End Definitions.
End InterferenceBoundGeneric.
\ No newline at end of file
This diff is collapsed.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.workload.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.interference prosa.classic.model.schedule.apa.affinity.
Require Import prosa.classic.analysis.apa.workload_bound prosa.classic.analysis.apa.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP.
Import Schedule WorkloadBound Priority Interference Affinity.
Export InterferenceBoundGeneric.
Section Definitions.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
(* Assume that each task has a processor affinity alpha. *)
Context {num_cpus: nat}.
Variable alpha: task_affinity sporadic_task num_cpus.
(* Let tsk be the task to be analyzed ... *)
Variable tsk: sporadic_task.
(* ... under subaffinity alpha'. *)
Variable alpha': affinity num_cpus.
Let task_with_response_time := (sporadic_task * time)%type.
(* Assume a known response-time bound for each interfering task ... *)
Variable R_prev: seq task_with_response_time.
(* ... and an interval length delta. *)
Variable delta: time.
(* Assume an FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
(* Recall the generic interference bound. *)
Let total_interference_bound := interference_bound_generic task_cost task_period tsk delta.
(* Let (hp_task_in alpha') denote the higher-priority tasks that can execute on alpha'. *)
Let hp_task_in alpha' := higher_priority_task_in alpha higher_eq_priority tsk alpha'.
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences of tasks in (hp_task_in alpha'). *)
Definition total_interference_bound_fp :=
\sum_((tsk_other, R_other) <- R_prev | hp_task_in alpha' tsk_other)
total_interference_bound (tsk_other, R_other).
End Definitions.
End InterferenceBoundFP.
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.analysis.global.basic.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundGeneric.
Section Definitions.
Import Schedule WorkloadBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
Let task_with_response_time := (sporadic_task * time)%type.
(* Assume a known response-time bound for each interfering task ... *)
Variable R_prev: seq task_with_response_time.
(* ... and an interval length delta. *)
Variable delta: time.
Section PerTask.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
(* Based on the workload bound, Bertogna and Cirinei define the
following interference bound for a task. *)
Definition interference_bound_generic :=
minn (W task_cost task_period tsk_other R_other delta) (delta - task_cost tsk + 1).
End PerTask.
End Definitions.
End InterferenceBoundGeneric.
\ No newline at end of file
This diff is collapsed.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.workload.
Require Import prosa.classic.model.schedule.global.basic.schedule prosa.classic.model.schedule.global.basic.interference.
Require Import prosa.classic.analysis.global.basic.workload_bound
prosa.classic.analysis.global.basic.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP.
Import Schedule WorkloadBound Priority Interference.
Export InterferenceBoundGeneric.
Section Definitions.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
Let task_with_response_time := (sporadic_task * time)%type.
(* Assume a known response-time bound for each higher-priority task ... *)
Variable R_prev: seq task_with_response_time.
(* ... in any interval of length delta. *)
Variable delta: time.
(* Assume an FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
(* Recall the generic interference bound. *)
Let total_interference_bound := interference_bound_generic task_cost task_period tsk delta.
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences. *)
Definition total_interference_bound_fp :=
\sum_((tsk_other, R_other) <- R_prev)
total_interference_bound (tsk_other, R_other).
End Definitions.
End InterferenceBoundFP.
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment