PROSA - Formally Proven Schedulability Analysis issueshttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues2024-03-22T10:13:18Zhttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/134Redundancy in definition of `respects_max_arrivals`2024-03-22T10:13:18ZKimaya BedarkarRedundancy in definition of `respects_max_arrivals`In the definition of [`respects_max_arrivals`](https://prosa.mpi-sws.org/branches/master/pretty/prosa.model.task.arrival.curves.html#respects_max_arrivals), the precondition `t1 <= t2` is not needed. If the condition is not true then the...In the definition of [`respects_max_arrivals`](https://prosa.mpi-sws.org/branches/master/pretty/prosa.model.task.arrival.curves.html#respects_max_arrivals), the precondition `t1 <= t2` is not needed. If the condition is not true then the property trivially holds.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/133Upstreamed lemma from `util/bigop.v` to ssreflect2024-01-12T10:48:55ZSergey BozhkoUpstreamed lemma from `util/bigop.v` to ssreflect
@bbb started a [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/343#note_99655):
> This is a lemma that seems generally useful and missing from ssreflect. Perhaps it could be upstreamed?
```coq
Lemma...
@bbb started a [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/343#note_99655):
> This is a lemma that seems generally useful and missing from ssreflect. Perhaps it could be upstreamed?
```coq
Lemma big_pred1_seq :
forall [R : Type] [idx : R] [op : Monoid.law idx] [X : eqType] [P : pred X] [F : X -> R]
(xs : seq X) (i : X),
(i \in xs) ->
(uniq xs) ->
P =1 pred1 i ->
\big[op/idx]_(j <- xs | P j) F j = F i.
```Sergey BozhkoSergey Bozhkohttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/132Introduce "completed jobs don't consume service" notion2024-01-04T13:18:33ZSergey BozhkoIntroduce "completed jobs don't consume service" notionFor overhead-aware analysis, it might be necessary to support a scenario when a completed job (with `service >= job_cost`) continues to execute without receiving service.For overhead-aware analysis, it might be necessary to support a scenario when a completed job (with `service >= job_cost`) continues to execute without receiving service.Sergey BozhkoSergey Bozhkohttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/131Consistent naming scheme for conditional interference and IBFs2024-01-03T13:33:46ZSergey BozhkoConsistent naming scheme for conditional interference and IBFsLet's come up with a good naming scheme for all the different kinds of instantiations of conditional interference and IBFs.
Long time ago (e.g., ECRTS'20), we had only two types of IBFs: (1) IBF that bounds all interference, and (2) IBF...Let's come up with a good naming scheme for all the different kinds of instantiations of conditional interference and IBFs.
Long time ago (e.g., ECRTS'20), we had only two types of IBFs: (1) IBF that bounds all interference, and (2) IBF that bounds interference from other tasks (so, it made sense to call them `IBF` and `IBF_other`).
Now we have a bunch of different IBFs: (1) the "vanilla" IBF ([[1](https://prosa.mpi-sws.org/branches/master/pretty/prosa.analysis.abstract.definitions.html#job_interference_is_bounded_by)]), (2) IBF that bounds interference from other tasks ([[2](https://prosa.mpi-sws.org/branches/master/pretty/prosa.analysis.abstract.IBF.task.html#task_interference_is_bounded_by)], (3) IBF that bounds intra-supply interference ([[3](https://prosa.mpi-sws.org/branches/master/pretty/prosa.analysis.abstract.IBF.supply.html)]), and (4) IBF that bounds intra-supply interference that comes from other tasks (to be merged soon). So, we need more meaningful names.
(Also, see [the original discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/319#note_99306))Sergey BozhkoSergey Bozhkohttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/130Define fixpoint predicates2024-01-03T12:53:23ZSergey BozhkoDefine fixpoint predicatesThe following discussion from !319 should be addressed:
- [ ] @bbb started a [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/319#note_99333): (+1 comment)
> Should we make these predicates proper defin...The following discussion from !319 should be addressed:
- [ ] @bbb started a [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/319#note_99333): (+1 comment)
> Should we make these predicates proper definitions (`nat -> Prop`)?
>
> - `aRSA_fixpoint R`
> - `aRTA_fixpoint R`
> - `bw_fixpoint L`
>
> Looks kinda neat, I think.
>
> We keep referring to these, also in discussion (e.g., w/ Matteo), perhaps named definitions would help?Sergey BozhkoSergey Bozhkohttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/128Changing basic definitions in Prosa2023-11-10T12:59:08ZKimaya BedarkarChanging basic definitions in ProsaCurrently, prosa definitions do not leverage other definitions enough. This often leads to unnecessarily longer and harder proofs. We should use already existing definitions wherever possible. In particular, defining new big_ops should b...Currently, prosa definitions do not leverage other definitions enough. This often leads to unnecessarily longer and harder proofs. We should use already existing definitions wherever possible. In particular, defining new big_ops should be avoided as much as possible by building on top of old bigops.
For example, [`task_served_at`](https://prosa.mpi-sws.org/branches/master/pretty/prosa.analysis.definitions.task_schedule.html#task_served_at) is defined using `receives_service_at` but not using [`served_jobs_at`](https://prosa.mpi-sws.org/branches/master/pretty/prosa.analysis.definitions.service.html#served_jobs_at)
We can use this issue to collect other instances of sub-optimal definitions.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/125layer unconditional priority inversion on top of conditional priority inversion2023-07-05T14:49:51ZBjörn Brandenburglayer unconditional priority inversion on top of conditional priority inversionFollow up from: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/318#note_93625Follow up from: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/318#note_93625https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/115the GEL bounded-PI RTA requires `lia` cleanup2023-04-20T12:38:30ZBjörn Brandenburgthe GEL bounded-PI RTA requires `lia` cleanup`results/gel/rta/bounded_pi.v` contains several slow-ish `lia` invocations; these should be optimized with `clear -`.`results/gel/rta/bounded_pi.v` contains several slow-ish `lia` invocations; these should be optimized with `clear -`.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/113move work-bearing readiness2023-03-29T18:27:29ZBjörn Brandenburgmove work-bearing readinessThe definition of [`work_bearing_readiness`](https://prosa.mpi-sws.org/branches/master/pretty/prosa.analysis.definitions.work_bearing_readiness.html) should be moved alongside the other notions of categories of readiness models in [prosa...The definition of [`work_bearing_readiness`](https://prosa.mpi-sws.org/branches/master/pretty/prosa.analysis.definitions.work_bearing_readiness.html) should be moved alongside the other notions of categories of readiness models in [prosa.analysis.definitions.readiness](https://prosa.mpi-sws.org/branches/master/pretty/prosa.analysis.definitions.readiness.html).
Additionally, `work_bearing_readiness` should take the readiness model it applies to explicitly (as a `Variable`, not `Context`).https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/105Split released OPAM packages2023-03-01T15:01:19ZBjörn BrandenburgSplit released OPAM packagesThe following [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/257#note_88041) from !257 should be addressed:
Pierre (@proux):
> If we merge this I should update the OPAM packages on https://coq.inria.fr/opa...The following [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/257#note_88041) from !257 should be addressed:
Pierre (@proux):
> If we merge this I should update the OPAM packages on https://coq.inria.fr/opam/extra-dev.
> The one on https://coq.inria.fr/opam/released should be "updated" only for the next release.
>
> Note that the name of the packages is opened to discussion, we could for instance have:
> * `coq-prosa-core`
> * `coq-prosa-poet` (dependeing on `coq-prosa-core`)
> * potentially `coq-prosa` as a virtual package depending on all other
>
> or any other combination
Björn:
> Ok, that means we’ll have to update the POET instructions when making the next stable Prosa release.
Pierre:
> Actually, there is no obligation to split the package on the repo.
>
> But I tend to think it's nice to offer more flexibility to users who may be not be interested in the refinements part and don't want to install all of mathcomp and coqeal.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/97Automation for busy interval destruction2023-07-04T14:53:52ZSergey BozhkoAutomation for busy interval destructionThe following discussion from !116 should be addressed:
- [ ] @kbedarka started a [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/116#note_85151): (+1 comment)
> I guess this destruct of `H_busy_interv...The following discussion from !116 should be addressed:
- [ ] @kbedarka started a [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/116#note_85151): (+1 comment)
> I guess this destruct of `H_busy_interval` should be automated. Although, I am not sure if that is in the scope of this MR
We should make destruction of busy interval automatic, since constant manual destruction becomes a bit repetitive (for example: [1](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/blob/fcdb00b946bc7f6254538ed55694e0c700fc151a/analysis/abstract/abstract_rta.v#L172), [2](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/blob/fcdb00b946bc7f6254538ed55694e0c700fc151a/analysis/abstract/abstract_rta.v#L187), [3](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/blob/fcdb00b946bc7f6254538ed55694e0c700fc151a/analysis/abstract/abstract_rta.v#L267), [4](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/blob/fcdb00b946bc7f6254538ed55694e0c700fc151a/analysis/abstract/abstract_rta.v#L312), [5](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/blob/fcdb00b946bc7f6254538ed55694e0c700fc151a/analysis/abstract/abstract_rta.v#L451), [6](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/blob/fcdb00b946bc7f6254538ed55694e0c700fc151a/analysis/abstract/abstract_rta.v#L460), ... in just one file)Sergey BozhkoSergey Bozhkohttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/90preemption model cleanup2022-03-15T09:47:30ZBjörn Brandenburgpreemption model cleanupThe preemption model is a rather large and complicated piece of the spec, and it seems to be in need of some cleanup.
1. There seem to be duplicated definitions that (at least superficially) seem to express the same idea: [`schedule_re...The preemption model is a rather large and complicated piece of the spec, and it seems to be in need of some cleanup.
1. There seem to be duplicated definitions that (at least superficially) seem to express the same idea: [`schedule_respects_preemption_model`](http://prosa.mpi-sws.org/branches/master/pretty/prosa.model.schedule.limited_preemptive.html#schedule_respects_preemption_model) vs. [not_preemptive_implies_scheduled](http://prosa.mpi-sws.org/branches/master/pretty/prosa.model.preemption.parameter.html#not_preemptive_implies_scheduled)
2. The current definitions and layout of the spec mix two different aspects:
- (a) *job behavior* -- whether or not a given job is preemptable at a given point in its execution, plus the corresponding task-level parameters and specs
- (b) *scheduler behavior* -- properties of the schedule and its structure
Of course (a) and (b) need to agree, but I they are not the same thing and I think they should be kept more clearly apart. Maybe this is mostly a matter of better documentation, but for now it seems rather confusing and I don't yet have a good idea of what how this can and should be clarified.Björn BrandenburgBjörn Brandenburghttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/80Compile on Coq Platform in CI2022-02-16T08:03:18ZBjörn BrandenburgCompile on Coq Platform in CIMake sure Prosa compiles cleanly in a default Coq Platform environment.
This will be easy once there's a [standard Docker image for Coq Platform](https://github.com/coq-community/docker-coq/issues/35).Make sure Prosa compiles cleanly in a default Coq Platform environment.
This will be easy once there's a [standard Docker image for Coq Platform](https://github.com/coq-community/docker-coq/issues/35).Björn BrandenburgBjörn Brandenburghttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/77util.nondecreasing duplicates predicate "sorted" from ssreflect.path2021-09-22T08:46:56ZSergey Bozhkoutil.nondecreasing duplicates predicate "sorted" from ssreflect.pathIt seems that [`util.nondecreasing`](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/nondecreasing.v) at least partially duplicates functionality of predicate `sorted` from `ssreflect.path`.
It might have sense to switch...It seems that [`util.nondecreasing`](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/nondecreasing.v) at least partially duplicates functionality of predicate `sorted` from `ssreflect.path`.
It might have sense to switch to `sorted`https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/68Coding Style: use of spaces2020-08-27T15:34:49ZBjörn BrandenburgCoding Style: use of spacesIt seems we have a bit of a coding style mess in Prosa `master`. I wrote a little script to check our usage of spaces before and after colons. It probably doesn't catch everything, but the output already shows that we have a fair bit of ...It seems we have a bit of a coding style mess in Prosa `master`. I wrote a little script to check our usage of spaces before and after colons. It probably doesn't catch everything, but the output already shows that we have a fair bit of diversity in style:
---
Coding Style in Prosa (without classic Prosa)
Spacing after Lemma/Fact/Theorem/Hypothesis/Corollary name:
- 731 instances of no space before colon (good)
- 406 instances of a space before colon (bad)
Naming of hypotheses:
- 607 Hypothesis names start with 'H_' (good)
- 6 Hypothesis names do not start with 'H_' (bad)
Spacing in Variable/Variables/Context declaration:
- 550 instances of a space before colon (good)
- 183 instances of no space before colon (bad)
- 435 no colon at all (implicit Context)
Spacing in Definition/Fixpoint:
- 116 instances of a space before colon (good)
- 22 instances of no space before colon (bad)
- 123 no colon at all (no parameters)
---
Consistent spacing may seem like a minor thing, but it's quite annoying to some (e.g., me) and it's difficult to tell new contributors "just follow the style of existing code" if that code is all over the place.
So this issue serves to find consensus on this. If I recall correctly, at some point we agreed on the following:
1. `Variable foo : ItsType.` — space before and after colon when giving types of variables or parameters.
2. `Context {SomeConcept : ItsType}.` — as above.
3. `Hypothesis H_foo: ` — no space before colon after the name of a hypothesis, and the name should start with `H_`.
4. `Lemma foo: ` — same here.
5. `Definition foo (bar_arg : ItsType) : TypeOfDefinition := ...` — again, spaces before explicit types.
My question to you: Do I recall this correctly? Is this what we want(ed) to standardize on?
I guess the only two viable alternatives would be no space before the colon everywhere (as in e.g. Rust), or always place a space before a colon (which looks weird for hypotheses and lemmas IMO).
In any case, we should pick *one* style and stick to it (and check compliance as part of CI).
Any preferences or opinions, or are you ok with me picking (and ultimately enforcing) something as long as it's consistent?
CC: @proux @sophie @mlesourd @ptorrx @mmaida @sbozhko @pointoflightBjörn BrandenburgBjörn Brandenburghttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/56Reasoning principles for ideal schedules2022-10-13T17:58:00ZMaxime LesourdReasoning principles for ideal schedulesWhile fixing the proofs in order to implement !54 I realized that we end up repeating simple case analyses on `sched t` which then requires using unfolding lemmas to relate `sched t` to the fact that some job is scheduled/receiving servi...While fixing the proofs in order to implement !54 I realized that we end up repeating simple case analyses on `sched t` which then requires using unfolding lemmas to relate `sched t` to the fact that some job is scheduled/receiving service at t. I believe that we could formulate a lemma to streamline this process.
Unfortunately I don't have the time to work on this right now but I'll use this issue to collect my experiments once I get to it.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/46Use Hint more strategically2022-02-22T15:32:18ZBjörn BrandenburgUse Hint more strategicallyAs noted by @mlesourd (https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/merge_requests/32#note_38961), using `Hint`s could make some of our proofs easier / shorter by automating away tedious steps. Going forward, we should introduce `Hint`...As noted by @mlesourd (https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/merge_requests/32#note_38961), using `Hint`s could make some of our proofs easier / shorter by automating away tedious steps. Going forward, we should introduce `Hint`s in Prosa and come up with some guidelines for when it's a good idea to do so.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/41Prosa Refactoring Effort2023-08-10T15:44:53ZBjörn BrandenburgProsa Refactoring EffortThe purpose of this file is to keep track of which files still need to be ported to the new refactored Prosa (the ‘behavior’ model). Check off a file once you have verified that either
- all still-relevant definitions and lemmas have b...The purpose of this file is to keep track of which files still need to be ported to the new refactored Prosa (the ‘behavior’ model). Check off a file once you have verified that either
- all still-relevant definitions and lemmas have been ported to the new behavior model, or
- the file requires no porting or is no longer relevant.
Files in the `util` module are not being tracked as it is presumed that they will not require to be ported.
## Behavioral Model
* [x] [./model/time.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.time.html)
* [ ] [./model/suspension.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.suspension.html) :exclamation: — task parameter and validity constraints are still missing
* [x] [./model/schedule/uni/workload.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.workload.html)
* [x] [./model/schedule/uni/schedulability.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.schedulability.html)
* [ ] [./model/schedule/uni/sustainability.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.sustainability.html) :exclamation:
* [x] [./model/policy_tdma.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.policy_tdma.html)
* [x] [./model/priority.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.priority.html)
* [x] [./model/schedule/uni/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.schedule.html)
* [ ] [./model/schedule/uni/end_time.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.end_time.html) :interrobang:
* [x] [./model/schedule/uni/schedule_of_task.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.schedule_of_task.html)
* [x] [./model/schedule/uni/response_time.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.response_time.html)
* [x] [./model/schedule/uni/service.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.service.html)
### Ideal L&L Model
* [x] [./model/schedule/uni/basic/platform.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.basic.platform.html)
* [x] [./model/schedule/uni/basic/platform_tdma.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.basic.platform_tdma.html)
* [x] [./model/arrival/basic/arrival_bounds.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.basic.arrival_bounds.html)
* [x] [./model/arrival/basic/task.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.basic.task.html)
* [x] [./model/arrival/basic/arrival_sequence.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.basic.arrival_sequence.html)
* [x] [./model/arrival/basic/job.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.basic.job.html)
* [x] [./model/arrival/basic/task_arrival.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.basic.task_arrival.html)
### Arrival Curves
* [x] [./model/arrival/curves/bounds.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.curves.bounds.html)
### Jitter
* [ ] [./model/arrival/jitter/arrival_bounds.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.jitter.arrival_bounds.html) — nothing equivalent exists, but it's questionable whether we'll need this anymore
* [x] [./model/arrival/jitter/arrival_sequence.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.jitter.arrival_sequence.html)
* [ ] [./model/arrival/jitter/job.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.jitter.job.html) :exclamation: — task parameter and validity constraints are still missing
* [x] [./model/arrival/jitter/task_arrival.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.arrival.jitter.task_arrival.html)
* [x] [./model/schedule/uni/jitter/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.jitter.schedule.html)
* [x] [./model/schedule/uni/jitter/platform.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.jitter.platform.html)
* [x] [./model/schedule/uni/jitter/valid_schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.jitter.valid_schedule.html)
### Self-Suspensions
* [ ] [./model/schedule/uni/susp/suspension_intervals.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.susp.suspension_intervals.html) :exclamation:
* [x] [./model/schedule/uni/susp/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.susp.schedule.html)
* [ ] [./model/schedule/uni/susp/last_execution.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.susp.last_execution.html) :interrobang:
* [ ] [./model/schedule/uni/susp/build_suspension_table.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.susp.build_suspension_table.html) :interrobang:
* [x] [./model/schedule/uni/susp/platform.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.susp.platform.html)
* [x] [./model/schedule/uni/susp/valid_schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.susp.valid_schedule.html)
### Non-Preemptive Workloads
* [x] [./model/schedule/uni/nonpreemptive/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.nonpreemptive.schedule.html)
* [x] [./model/schedule/uni/nonpreemptive/platform.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.nonpreemptive.platform.html)
### Limited-Preemptive Workloads
* [x] [./model/schedule/uni/limited/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.schedule.html)
* [x] [./model/schedule/uni/limited/platform/util.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.platform.util.html)
* [x] [./model/schedule/uni/limited/platform/preemptive.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.platform.preemptive.html)
* [x] [./model/schedule/uni/limited/platform/limited.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.platform.limited.html)
* [x] [./model/schedule/uni/limited/platform/definitions.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.platform.definitions.html)
* [x] [./model/schedule/uni/limited/platform/priority_inversion_is_bounded.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.platform.priority_inversion_is_bounded.html)
* [x] [./model/schedule/uni/limited/platform/nonpreemptive.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.platform.nonpreemptive.html)
* [x] [./model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta.html)
* [x] [./model/schedule/uni/limited/abstract_RTA/definitions.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.abstract_RTA.definitions.html)
* [x] [./model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space.html)
* [x] [./model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service.html)
* [x] [./model/schedule/uni/limited/abstract_RTA/abstract_rta.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_rta.html)
* [x] [./model/schedule/uni/limited/fixed_priority/response_time_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.fixed_priority.response_time_bound.html)
* [x] [./model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound.html)
* [x] [./model/schedule/uni/limited/fixed_priority/nonpr_reg/nonpreemptive/response_time_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.nonpreemptive.response_time_bound.html)
* [x] [./model/schedule/uni/limited/fixed_priority/nonpr_reg/fixed/response_time_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.fixed.response_time_bound.html)
* [x] [./model/schedule/uni/limited/fixed_priority/nonpr_reg/floating/response_time_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.floating.response_time_bound.html)
* [x] [./model/schedule/uni/limited/fixed_priority/nonpr_reg/preemptive/response_time_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.preemptive.response_time_bound.html)
* [x] [./model/schedule/uni/limited/rbf.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.rbf.html)
### Transformation
* [ ] [./model/schedule/uni/transformation/construction.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.transformation.construction.html)
## Uniprocessor Analyses
#### Basic
* [ ] [./model/schedule/uni/basic/busy_interval.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.basic.busy_interval.html)
* [ ] [./analysis/uni/basic/workload_bound_fp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.basic.workload_bound_fp.html)
* [ ] [./analysis/uni/basic/tdma_wcrt_analysis.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.basic.tdma_wcrt_analysis.html)
* [ ] [./analysis/uni/basic/tdma_rta_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.basic.tdma_rta_theory.html)
* [ ] [./analysis/uni/basic/fp_rta_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.basic.fp_rta_theory.html)
* [ ] [./analysis/uni/basic/fp_rta_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.basic.fp_rta_comp.html)
#### Jitter
* [ ] [./model/schedule/uni/jitter/busy_interval.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.jitter.busy_interval.html)
* [ ] [./analysis/uni/jitter/workload_bound_fp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.jitter.workload_bound_fp.html)
* [ ] [./analysis/uni/jitter/fp_rta_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.jitter.fp_rta_theory.html)
* [ ] [./analysis/uni/jitter/fp_rta_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.jitter.fp_rta_comp.html)
#### Limited-Preemptive
* [ ] [./model/schedule/uni/limited/busy_interval.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.uni.limited.busy_interval.html)
#### Curves
* [ ] [./analysis/uni/arrival_curves/workload_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.arrival_curves.workload_bound.html)
#### Dynamic Self-Suspensions via Suspension-Oblivious Analysis
* [ ] [./analysis/uni/susp/dynamic/oblivious/reduction.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.oblivious.reduction.html)
* [ ] [./analysis/uni/susp/dynamic/oblivious/fp_rta.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.oblivious.fp_rta.html)
#### Dynamic Self-Suspensions via Jitter Analysis
* [ ] [./analysis/uni/susp/dynamic/jitter/taskset_rta.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.jitter.taskset_rta.html)
* [ ] [./analysis/uni/susp/dynamic/jitter/taskset_membership.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.jitter.taskset_membership.html)
* [ ] [./analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_service.html)
* [ ] [./analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties.html)
* [ ] [./analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation.html)
* [ ] [./analysis/uni/susp/dynamic/jitter/jitter_schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule.html)
* [ ] [./analysis/uni/susp/dynamic/jitter/rta_by_reduction.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.dynamic.jitter.rta_by_reduction.html)
#### Sustainability
* [ ] [./analysis/uni/susp/sustainability/allcosts/reduction_properties.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.sustainability.allcosts.reduction_properties.html)
* [ ] [./analysis/uni/susp/sustainability/allcosts/reduction.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.sustainability.allcosts.reduction.html)
* [ ] [./analysis/uni/susp/sustainability/allcosts/main_claim.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.sustainability.allcosts.main_claim.html)
* [ ] [./analysis/uni/susp/sustainability/singlecost/reduction_properties.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.sustainability.singlecost.reduction_properties.html)
* [ ] [./analysis/uni/susp/sustainability/singlecost/reduction.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.uni.susp.sustainability.singlecost.reduction.html)
## Multiprocessor Behavioral Models
* [ ] [./model/schedule/apa/platform.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.apa.platform.html)
* [ ] [./model/schedule/apa/interference.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.apa.interference.html)
* [ ] [./model/schedule/apa/constrained_deadlines.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.apa.constrained_deadlines.html)
* [ ] [./model/schedule/apa/affinity.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.apa.affinity.html)
* [ ] [./model/schedule/apa/interference_edf.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.apa.interference_edf.html)
* [ ] [./model/schedule/partitioned/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.partitioned.schedule.html)
* [ ] [./model/schedule/partitioned/schedulability.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.partitioned.schedulability.html)
* [ ] [./model/schedule/global/transformation/construction.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.transformation.construction.html)
* [ ] [./model/schedule/global/basic/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.basic.schedule.html)
* [ ] [./model/schedule/global/basic/platform.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.basic.platform.html)
* [ ] [./model/schedule/global/basic/interference.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.basic.interference.html)
* [ ] [./model/schedule/global/basic/constrained_deadlines.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.basic.constrained_deadlines.html)
* [ ] [./model/schedule/global/basic/interference_edf.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.basic.interference_edf.html)
* [ ] [./model/schedule/global/response_time.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.response_time.html)
* [ ] [./model/schedule/global/workload.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.workload.html)
* [ ] [./model/schedule/global/jitter/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.jitter.schedule.html)
* [ ] [./model/schedule/global/jitter/platform.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.jitter.platform.html)
* [ ] [./model/schedule/global/jitter/interference.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.jitter.interference.html)
* [ ] [./model/schedule/global/jitter/constrained_deadlines.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.jitter.constrained_deadlines.html)
* [ ] [./model/schedule/global/jitter/job.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.jitter.job.html)
* [ ] [./model/schedule/global/jitter/interference_edf.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.jitter.interference_edf.html)
* [ ] [./model/schedule/global/schedulability.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.model.schedule.global.schedulability.html)
## Multiprocessor Analyses
* [ ] [./analysis/apa/workload_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.apa.workload_bound.html)
* [ ] [./analysis/apa/interference_bound_fp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.apa.interference_bound_fp.html)
* [ ] [./analysis/apa/bertogna_fp_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.apa.bertogna_fp_theory.html)
* [ ] [./analysis/apa/bertogna_edf_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.apa.bertogna_edf_theory.html)
* [ ] [./analysis/apa/interference_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.apa.interference_bound.html)
* [ ] [./analysis/apa/interference_bound_edf.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.apa.interference_bound_edf.html)
* [ ] [./analysis/apa/bertogna_edf_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.apa.bertogna_edf_comp.html)
* [ ] [./analysis/apa/bertogna_fp_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.apa.bertogna_fp_comp.html)
* [ ] [./analysis/global/parallel/workload_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.parallel.workload_bound.html)
* [ ] [./analysis/global/parallel/interference_bound_fp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.parallel.interference_bound_fp.html)
* [ ] [./analysis/global/parallel/bertogna_fp_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.parallel.bertogna_fp_theory.html)
* [ ] [./analysis/global/parallel/bertogna_edf_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.parallel.bertogna_edf_theory.html)
* [ ] [./analysis/global/parallel/interference_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.parallel.interference_bound.html)
* [ ] [./analysis/global/parallel/interference_bound_edf.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.parallel.interference_bound_edf.html)
* [ ] [./analysis/global/parallel/bertogna_edf_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.parallel.bertogna_edf_comp.html)
* [ ] [./analysis/global/parallel/bertogna_fp_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.parallel.bertogna_fp_comp.html)
* [ ] [./analysis/global/basic/workload_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.basic.workload_bound.html)
* [ ] [./analysis/global/basic/interference_bound_fp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.basic.interference_bound_fp.html)
* [ ] [./analysis/global/basic/bertogna_fp_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.basic.bertogna_fp_theory.html)
* [ ] [./analysis/global/basic/bertogna_edf_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.basic.bertogna_edf_theory.html)
* [ ] [./analysis/global/basic/interference_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.basic.interference_bound.html)
* [ ] [./analysis/global/basic/interference_bound_edf.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.basic.interference_bound_edf.html)
* [ ] [./analysis/global/basic/bertogna_edf_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.basic.bertogna_edf_comp.html)
* [ ] [./analysis/global/basic/bertogna_fp_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.basic.bertogna_fp_comp.html)
* [ ] [./analysis/global/jitter/workload_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.jitter.workload_bound.html)
* [ ] [./analysis/global/jitter/interference_bound_fp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.jitter.interference_bound_fp.html)
* [ ] [./analysis/global/jitter/bertogna_fp_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.jitter.bertogna_fp_theory.html)
* [ ] [./analysis/global/jitter/bertogna_edf_theory.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.jitter.bertogna_edf_theory.html)
* [ ] [./analysis/global/jitter/interference_bound.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.jitter.interference_bound.html)
* [ ] [./analysis/global/jitter/interference_bound_edf.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.jitter.interference_bound_edf.html)
* [ ] [./analysis/global/jitter/bertogna_edf_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.jitter.bertogna_edf_comp.html)
* [ ] [./analysis/global/jitter/bertogna_fp_comp.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.analysis.global.jitter.bertogna_fp_comp.html)
## Implementations
* [ ] [./implementation/task.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.task.html)
* [ ] [./implementation/uni/basic/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.basic.schedule.html)
* [ ] [./implementation/uni/basic/fp_rta_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.basic.fp_rta_example.html)
* [ ] [./implementation/uni/basic/schedule_tdma.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.basic.schedule_tdma.html)
* [ ] [./implementation/uni/basic/tdma_rta_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.basic.tdma_rta_example.html)
* [ ] [./implementation/uni/basic/extraction_tdma.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.basic.extraction_tdma.html)
* [ ] [./implementation/uni/jitter/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.jitter.schedule.html)
* [ ] [./implementation/uni/jitter/fp_rta_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.jitter.fp_rta_example.html)
* [ ] [./implementation/uni/jitter/task.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.jitter.task.html)
* [ ] [./implementation/uni/jitter/arrival_sequence.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.jitter.arrival_sequence.html)
* [ ] [./implementation/uni/jitter/job.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.jitter.job.html)
* [ ] [./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.susp.dynamic.oblivious.fp_rta_example.html)
* [ ] [./implementation/uni/susp/dynamic/task.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.susp.dynamic.task.html)
* [ ] [./implementation/uni/susp/dynamic/arrival_sequence.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.susp.dynamic.arrival_sequence.html)
* [ ] [./implementation/uni/susp/dynamic/job.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.susp.dynamic.job.html)
* [ ] [./implementation/uni/susp/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.uni.susp.schedule.html)
* [ ] [./implementation/apa/bertogna_edf_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.apa.bertogna_edf_example.html)
* [ ] [./implementation/apa/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.apa.schedule.html)
* [ ] [./implementation/apa/task.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.apa.task.html)
* [ ] [./implementation/apa/bertogna_fp_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.apa.bertogna_fp_example.html)
* [ ] [./implementation/apa/arrival_sequence.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.apa.arrival_sequence.html)
* [ ] [./implementation/apa/job.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.apa.job.html)
* [ ] [./implementation/arrival_sequence.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.arrival_sequence.html)
* [ ] [./implementation/global/parallel/bertogna_edf_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.parallel.bertogna_edf_example.html)
* [ ] [./implementation/global/parallel/bertogna_fp_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.parallel.bertogna_fp_example.html)
* [ ] [./implementation/global/basic/bertogna_edf_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.basic.bertogna_edf_example.html)
* [ ] [./implementation/global/basic/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.basic.schedule.html)
* [ ] [./implementation/global/basic/bertogna_fp_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.basic.bertogna_fp_example.html)
* [ ] [./implementation/global/jitter/bertogna_edf_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.jitter.bertogna_edf_example.html)
* [ ] [./implementation/global/jitter/schedule.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.jitter.schedule.html)
* [ ] [./implementation/global/jitter/task.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.jitter.task.html)
* [ ] [./implementation/global/jitter/bertogna_fp_example.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.jitter.bertogna_fp_example.html)
* [ ] [./implementation/global/jitter/arrival_sequence.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.jitter.arrival_sequence.html)
* [ ] [./implementation/global/jitter/job.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.global.jitter.job.html)
* [ ] [./implementation/job.v](https://prosa.mpi-sws.org/branches/classic-prosa/pretty/prosa.classic.implementation.job.html)Björn BrandenburgBjörn Brandenburghttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/39Follow-up from "WIP: Base for the behavior part of refactored PROSA." : Typec...2019-10-22T13:49:59ZMaxime LesourdFollow-up from "WIP: Base for the behavior part of refactored PROSA." : Typeclass documentationThe following discussion from !12 should be addressed:
- [ ] @mlesourd started a [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/merge_requests/12#note_35005): (+5 comments)
> Here is an example of a typeclass for a jo...The following discussion from !12 should be addressed:
- [ ] @mlesourd started a [discussion](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/merge_requests/12#note_35005): (+5 comments)
> Here is an example of a typeclass for a job parameter.
>
> One improvement over the initial proposal is the use of "singleton classes" which do not require wrapping the parameter.Maxime LesourdMaxime Lesourdhttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/33Have compound hypotheses for "reasonable schedule" and "reasonable workload"2022-08-13T12:15:22ZBjörn BrandenburgHave compound hypotheses for "reasonable schedule" and "reasonable workload"In just about any theory, a couple of standard "sanity" assumptions show up:
- jobs don't execute before they are released
- jobs don't executer after they are finished
- jobs arrive only once
- job arrival times are consistent
Additi...In just about any theory, a couple of standard "sanity" assumptions show up:
- jobs don't execute before they are released
- jobs don't executer after they are finished
- jobs arrive only once
- job arrival times are consistent
Additionally, in the context of a task model, we also usually assume:
- there is a finite set of tasks
- all jobs in the arrival sequence stem from some task
- jobs don't execute for longer than their task's WCET
- jobs from the same task execute in FIFO order
Let's define some standard definitions to group these hypotheses into more succinct compound assumptions (i.e., definitions that are big conjunctions). This should help to substantially reduce the amount of boilerplate assumptions in the beginning of many files.
We could then also have a second level of even higher-level compound assumptions such as "preemptive sporadic tasks". For example, the "sporadic task model" encompasses the following assumptions:
- reasonable schedule
- reasonable workload
- sporadic arrivals
For example, I'd like to reduce the assumptions for RTA of fixed-priority preemptive scheduling of sporadic tasks to something like this:
1. preemptive sporadic task model
2. jobs are always preemptive
3. schedule is work-conserving
4. schedule follows FP policy [at preemption points]
Basically, let's aim to reduce the list of explicitly stated hypotheses to high-level concepts that one would also state in a paper (e.g., "fixed-priority", "preemptive", "sporadic tasks") and avoid explicitly listing too many low-level, detailed assumptions. Proofs can just split & extract whatever hypotheses they need from the compound assumptions.
By making these compound assumptions, we don't restrict generality --- individual analyses are still free to pick and choose whatever assumptions they need, but the vast majority of analyses making "standard assumptions" become a lot simpler.
Comments or thoughts?
CC: @sophie @mlesourd @xiaojie @prouxSergey BozhkoSergey Bozhko