PROSA - Formally Proven Schedulability Analysis issueshttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues2020-08-27T15:34:49Zhttps://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 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 @pointoflightIt 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 schedules2019-10-28T15:41:38ZMaxime 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 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.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/55Definition of service for ideal schedules2019-10-28T15:35:11ZMaxime LesourdDefinition of service for ideal schedulesThe definition of `service_at` in [ideal.v](restructuring/model/processor/ideal.v) is given using the implicit conversion `nat_of_bool` as `s == Some j`.
Unfolding this definition would give `if s == Some j then 1 else 0` which should be equivalent and feels more readable.The definition of `service_at` in [ideal.v](restructuring/model/processor/ideal.v) is given using the implicit conversion `nat_of_bool` as `s == Some j`.
Unfolding this definition would give `if s == Some j then 1 else 0` which should be equivalent and feels more readable.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/46Use Hint more strategically2019-07-30T15:46:26ZBjö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`s in Prosa and come up with some guidelines for when it's a good idea to do so.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 Effort2019-08-13T10:52:42ZBjö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 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
* [ ] ./model/suspension.v
* [ ] ./model/schedule/uni/workload.v
* [x] ./model/schedule/uni/schedulability.v
* [ ] ./model/schedule/uni/sustainability.v
* [x] ./model/policy_tdma.v
* [ ] ./model/priority.v
* [x] ./model/schedule/uni/schedule.v
* [ ] ./model/schedule/uni/end_time.v
* [ ] ./model/schedule/uni/schedule_of_task.v
* [ ] ./model/schedule/uni/response_time.v
* [ ] ./model/schedule/uni/service.v
### Ideal L&L Model
* [ ] ./model/schedule/uni/basic/platform.v
* [x] ./model/schedule/uni/basic/platform_tdma.v
* [ ] ./model/arrival/basic/arrival_bounds.v
* [x] ./model/arrival/basic/task.v
* [x] ./model/arrival/basic/arrival_sequence.v
* [x] ./model/arrival/basic/job.v
* [ ] ./model/arrival/basic/task_arrival.v
### Arrival Curves
* [x] ./model/arrival/curves/bounds.v
### Jitter
* [ ] ./model/arrival/jitter/arrival_bounds.v
* [ ] ./model/arrival/jitter/arrival_sequence.v
* [ ] ./model/arrival/jitter/job.v
* [ ] ./model/arrival/jitter/task_arrival.v
* [ ] ./model/schedule/uni/jitter/schedule.v
* [ ] ./model/schedule/uni/jitter/platform.v
* [ ] ./model/schedule/uni/jitter/valid_schedule.v
### Self-Suspensions
* [ ] ./model/schedule/uni/susp/suspension_intervals.v
* [ ] ./model/schedule/uni/susp/schedule.v
* [ ] ./model/schedule/uni/susp/last_execution.v
* [ ] ./model/schedule/uni/susp/build_suspension_table.v
* [ ] ./model/schedule/uni/susp/platform.v
* [ ] ./model/schedule/uni/susp/valid_schedule.v
### Non-Preemptive Workloads
* [ ] ./model/schedule/uni/nonpreemptive/schedule.v
* [ ] ./model/schedule/uni/nonpreemptive/platform.v
### Limited-Preemptive Workloads
* [ ] ./model/schedule/uni/limited/schedule.v
* [ ] ./model/schedule/uni/limited/platform/util.v
* [ ] ./model/schedule/uni/limited/platform/preemptive.v
* [ ] ./model/schedule/uni/limited/platform/limited.v
* [ ] ./model/schedule/uni/limited/platform/definitions.v
* [ ] ./model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
* [ ] ./model/schedule/uni/limited/platform/nonpreemptive.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/definitions.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/abstract_rta.v
* [ ] ./model/schedule/uni/limited/fixed_priority/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/nonpreemptive/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/fixed/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/floating/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/preemptive/response_time_bound.v
* [ ] ./model/schedule/uni/limited/rbf.v
### Transformation
* [ ] ./model/schedule/uni/transformation/construction.v
## Uniprocessor Analyses
* [ ] ./model/schedule/uni/basic/busy_interval.v
* [ ] ./model/schedule/uni/jitter/busy_interval.v
* [ ] ./model/schedule/uni/limited/busy_interval.v
* [ ] ./analysis/uni/basic/workload_bound_fp.v
* [ ] ./analysis/uni/basic/tdma_wcrt_analysis.v
* [ ] ./analysis/uni/basic/tdma_rta_theory.v
* [ ] ./analysis/uni/basic/fp_rta_theory.v
* [ ] ./analysis/uni/basic/fp_rta_comp.v
* [ ] ./analysis/uni/arrival_curves/workload_bound.v
* [ ] ./analysis/uni/jitter/workload_bound_fp.v
* [ ] ./analysis/uni/jitter/fp_rta_theory.v
* [ ] ./analysis/uni/jitter/fp_rta_comp.v
* [ ] ./analysis/uni/susp/dynamic/oblivious/reduction.v
* [ ] ./analysis/uni/susp/dynamic/oblivious/fp_rta.v
* [ ] ./analysis/uni/susp/dynamic/jitter/taskset_rta.v
* [ ] ./analysis/uni/susp/dynamic/jitter/taskset_membership.v
* [ ] ./analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
* [ ] ./analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
* [ ] ./analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
* [ ] ./analysis/uni/susp/dynamic/jitter/jitter_schedule.v
* [ ] ./analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
* [ ] ./analysis/uni/susp/sustainability/allcosts/reduction_properties.v
* [ ] ./analysis/uni/susp/sustainability/allcosts/reduction.v
* [ ] ./analysis/uni/susp/sustainability/allcosts/main_claim.v
* [ ] ./analysis/uni/susp/sustainability/singlecost/reduction_properties.v
* [ ] ./analysis/uni/susp/sustainability/singlecost/reduction.v
## Multiprocessor Behavioral Models
* [ ] ./model/schedule/apa/platform.v
* [ ] ./model/schedule/apa/interference.v
* [ ] ./model/schedule/apa/constrained_deadlines.v
* [ ] ./model/schedule/apa/affinity.v
* [ ] ./model/schedule/apa/interference_edf.v
* [ ] ./model/schedule/partitioned/schedule.v
* [ ] ./model/schedule/partitioned/schedulability.v
* [ ] ./model/schedule/global/transformation/construction.v
* [ ] ./model/schedule/global/basic/schedule.v
* [ ] ./model/schedule/global/basic/platform.v
* [ ] ./model/schedule/global/basic/interference.v
* [ ] ./model/schedule/global/basic/constrained_deadlines.v
* [ ] ./model/schedule/global/basic/interference_edf.v
* [ ] ./model/schedule/global/response_time.v
* [ ] ./model/schedule/global/workload.v
* [ ] ./model/schedule/global/jitter/schedule.v
* [ ] ./model/schedule/global/jitter/platform.v
* [ ] ./model/schedule/global/jitter/interference.v
* [ ] ./model/schedule/global/jitter/constrained_deadlines.v
* [ ] ./model/schedule/global/jitter/job.v
* [ ] ./model/schedule/global/jitter/interference_edf.v
* [ ] ./model/schedule/global/schedulability.v
## Multiprocessor Analyses
* [ ] ./analysis/apa/workload_bound.v
* [ ] ./analysis/apa/interference_bound_fp.v
* [ ] ./analysis/apa/bertogna_fp_theory.v
* [ ] ./analysis/apa/bertogna_edf_theory.v
* [ ] ./analysis/apa/interference_bound.v
* [ ] ./analysis/apa/interference_bound_edf.v
* [ ] ./analysis/apa/bertogna_edf_comp.v
* [ ] ./analysis/apa/bertogna_fp_comp.v
* [ ] ./analysis/global/parallel/workload_bound.v
* [ ] ./analysis/global/parallel/interference_bound_fp.v
* [ ] ./analysis/global/parallel/bertogna_fp_theory.v
* [ ] ./analysis/global/parallel/bertogna_edf_theory.v
* [ ] ./analysis/global/parallel/interference_bound.v
* [ ] ./analysis/global/parallel/interference_bound_edf.v
* [ ] ./analysis/global/parallel/bertogna_edf_comp.v
* [ ] ./analysis/global/parallel/bertogna_fp_comp.v
* [ ] ./analysis/global/basic/workload_bound.v
* [ ] ./analysis/global/basic/interference_bound_fp.v
* [ ] ./analysis/global/basic/bertogna_fp_theory.v
* [ ] ./analysis/global/basic/bertogna_edf_theory.v
* [ ] ./analysis/global/basic/interference_bound.v
* [ ] ./analysis/global/basic/interference_bound_edf.v
* [ ] ./analysis/global/basic/bertogna_edf_comp.v
* [ ] ./analysis/global/basic/bertogna_fp_comp.v
* [ ] ./analysis/global/jitter/workload_bound.v
* [ ] ./analysis/global/jitter/interference_bound_fp.v
* [ ] ./analysis/global/jitter/bertogna_fp_theory.v
* [ ] ./analysis/global/jitter/bertogna_edf_theory.v
* [ ] ./analysis/global/jitter/interference_bound.v
* [ ] ./analysis/global/jitter/interference_bound_edf.v
* [ ] ./analysis/global/jitter/bertogna_edf_comp.v
* [ ] ./analysis/global/jitter/bertogna_fp_comp.v
## Implementations
* [ ] ./implementation/task.v
* [ ] ./implementation/uni/basic/schedule.v
* [ ] ./implementation/uni/basic/fp_rta_example.v
* [ ] ./implementation/uni/basic/schedule_tdma.v
* [ ] ./implementation/uni/basic/tdma_rta_example.v
* [ ] ./implementation/uni/basic/extraction_tdma.v
* [ ] ./implementation/uni/jitter/schedule.v
* [ ] ./implementation/uni/jitter/fp_rta_example.v
* [ ] ./implementation/uni/jitter/task.v
* [ ] ./implementation/uni/jitter/arrival_sequence.v
* [ ] ./implementation/uni/jitter/job.v
* [ ] ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
* [ ] ./implementation/uni/susp/dynamic/task.v
* [ ] ./implementation/uni/susp/dynamic/arrival_sequence.v
* [ ] ./implementation/uni/susp/dynamic/job.v
* [ ] ./implementation/uni/susp/schedule.v
* [ ] ./implementation/apa/bertogna_edf_example.v
* [ ] ./implementation/apa/schedule.v
* [ ] ./implementation/apa/task.v
* [ ] ./implementation/apa/bertogna_fp_example.v
* [ ] ./implementation/apa/arrival_sequence.v
* [ ] ./implementation/apa/job.v
* [ ] ./implementation/arrival_sequence.v
* [ ] ./implementation/global/parallel/bertogna_edf_example.v
* [ ] ./implementation/global/parallel/bertogna_fp_example.v
* [ ] ./implementation/global/basic/bertogna_edf_example.v
* [ ] ./implementation/global/basic/schedule.v
* [ ] ./implementation/global/basic/bertogna_fp_example.v
* [ ] ./implementation/global/jitter/bertogna_edf_example.v
* [ ] ./implementation/global/jitter/schedule.v
* [ ] ./implementation/global/jitter/task.v
* [ ] ./implementation/global/jitter/bertogna_fp_example.v
* [ ] ./implementation/global/jitter/arrival_sequence.v
* [ ] ./implementation/global/jitter/job.v
* [ ] ./implementation/job.vThe 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
* [ ] ./model/suspension.v
* [ ] ./model/schedule/uni/workload.v
* [x] ./model/schedule/uni/schedulability.v
* [ ] ./model/schedule/uni/sustainability.v
* [x] ./model/policy_tdma.v
* [ ] ./model/priority.v
* [x] ./model/schedule/uni/schedule.v
* [ ] ./model/schedule/uni/end_time.v
* [ ] ./model/schedule/uni/schedule_of_task.v
* [ ] ./model/schedule/uni/response_time.v
* [ ] ./model/schedule/uni/service.v
### Ideal L&L Model
* [ ] ./model/schedule/uni/basic/platform.v
* [x] ./model/schedule/uni/basic/platform_tdma.v
* [ ] ./model/arrival/basic/arrival_bounds.v
* [x] ./model/arrival/basic/task.v
* [x] ./model/arrival/basic/arrival_sequence.v
* [x] ./model/arrival/basic/job.v
* [ ] ./model/arrival/basic/task_arrival.v
### Arrival Curves
* [x] ./model/arrival/curves/bounds.v
### Jitter
* [ ] ./model/arrival/jitter/arrival_bounds.v
* [ ] ./model/arrival/jitter/arrival_sequence.v
* [ ] ./model/arrival/jitter/job.v
* [ ] ./model/arrival/jitter/task_arrival.v
* [ ] ./model/schedule/uni/jitter/schedule.v
* [ ] ./model/schedule/uni/jitter/platform.v
* [ ] ./model/schedule/uni/jitter/valid_schedule.v
### Self-Suspensions
* [ ] ./model/schedule/uni/susp/suspension_intervals.v
* [ ] ./model/schedule/uni/susp/schedule.v
* [ ] ./model/schedule/uni/susp/last_execution.v
* [ ] ./model/schedule/uni/susp/build_suspension_table.v
* [ ] ./model/schedule/uni/susp/platform.v
* [ ] ./model/schedule/uni/susp/valid_schedule.v
### Non-Preemptive Workloads
* [ ] ./model/schedule/uni/nonpreemptive/schedule.v
* [ ] ./model/schedule/uni/nonpreemptive/platform.v
### Limited-Preemptive Workloads
* [ ] ./model/schedule/uni/limited/schedule.v
* [ ] ./model/schedule/uni/limited/platform/util.v
* [ ] ./model/schedule/uni/limited/platform/preemptive.v
* [ ] ./model/schedule/uni/limited/platform/limited.v
* [ ] ./model/schedule/uni/limited/platform/definitions.v
* [ ] ./model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
* [ ] ./model/schedule/uni/limited/platform/nonpreemptive.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/definitions.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
* [ ] ./model/schedule/uni/limited/abstract_RTA/abstract_rta.v
* [ ] ./model/schedule/uni/limited/fixed_priority/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/nonpreemptive/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/fixed/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/floating/response_time_bound.v
* [ ] ./model/schedule/uni/limited/fixed_priority/nonpr_reg/preemptive/response_time_bound.v
* [ ] ./model/schedule/uni/limited/rbf.v
### Transformation
* [ ] ./model/schedule/uni/transformation/construction.v
## Uniprocessor Analyses
* [ ] ./model/schedule/uni/basic/busy_interval.v
* [ ] ./model/schedule/uni/jitter/busy_interval.v
* [ ] ./model/schedule/uni/limited/busy_interval.v
* [ ] ./analysis/uni/basic/workload_bound_fp.v
* [ ] ./analysis/uni/basic/tdma_wcrt_analysis.v
* [ ] ./analysis/uni/basic/tdma_rta_theory.v
* [ ] ./analysis/uni/basic/fp_rta_theory.v
* [ ] ./analysis/uni/basic/fp_rta_comp.v
* [ ] ./analysis/uni/arrival_curves/workload_bound.v
* [ ] ./analysis/uni/jitter/workload_bound_fp.v
* [ ] ./analysis/uni/jitter/fp_rta_theory.v
* [ ] ./analysis/uni/jitter/fp_rta_comp.v
* [ ] ./analysis/uni/susp/dynamic/oblivious/reduction.v
* [ ] ./analysis/uni/susp/dynamic/oblivious/fp_rta.v
* [ ] ./analysis/uni/susp/dynamic/jitter/taskset_rta.v
* [ ] ./analysis/uni/susp/dynamic/jitter/taskset_membership.v
* [ ] ./analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
* [ ] ./analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
* [ ] ./analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
* [ ] ./analysis/uni/susp/dynamic/jitter/jitter_schedule.v
* [ ] ./analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
* [ ] ./analysis/uni/susp/sustainability/allcosts/reduction_properties.v
* [ ] ./analysis/uni/susp/sustainability/allcosts/reduction.v
* [ ] ./analysis/uni/susp/sustainability/allcosts/main_claim.v
* [ ] ./analysis/uni/susp/sustainability/singlecost/reduction_properties.v
* [ ] ./analysis/uni/susp/sustainability/singlecost/reduction.v
## Multiprocessor Behavioral Models
* [ ] ./model/schedule/apa/platform.v
* [ ] ./model/schedule/apa/interference.v
* [ ] ./model/schedule/apa/constrained_deadlines.v
* [ ] ./model/schedule/apa/affinity.v
* [ ] ./model/schedule/apa/interference_edf.v
* [ ] ./model/schedule/partitioned/schedule.v
* [ ] ./model/schedule/partitioned/schedulability.v
* [ ] ./model/schedule/global/transformation/construction.v
* [ ] ./model/schedule/global/basic/schedule.v
* [ ] ./model/schedule/global/basic/platform.v
* [ ] ./model/schedule/global/basic/interference.v
* [ ] ./model/schedule/global/basic/constrained_deadlines.v
* [ ] ./model/schedule/global/basic/interference_edf.v
* [ ] ./model/schedule/global/response_time.v
* [ ] ./model/schedule/global/workload.v
* [ ] ./model/schedule/global/jitter/schedule.v
* [ ] ./model/schedule/global/jitter/platform.v
* [ ] ./model/schedule/global/jitter/interference.v
* [ ] ./model/schedule/global/jitter/constrained_deadlines.v
* [ ] ./model/schedule/global/jitter/job.v
* [ ] ./model/schedule/global/jitter/interference_edf.v
* [ ] ./model/schedule/global/schedulability.v
## Multiprocessor Analyses
* [ ] ./analysis/apa/workload_bound.v
* [ ] ./analysis/apa/interference_bound_fp.v
* [ ] ./analysis/apa/bertogna_fp_theory.v
* [ ] ./analysis/apa/bertogna_edf_theory.v
* [ ] ./analysis/apa/interference_bound.v
* [ ] ./analysis/apa/interference_bound_edf.v
* [ ] ./analysis/apa/bertogna_edf_comp.v
* [ ] ./analysis/apa/bertogna_fp_comp.v
* [ ] ./analysis/global/parallel/workload_bound.v
* [ ] ./analysis/global/parallel/interference_bound_fp.v
* [ ] ./analysis/global/parallel/bertogna_fp_theory.v
* [ ] ./analysis/global/parallel/bertogna_edf_theory.v
* [ ] ./analysis/global/parallel/interference_bound.v
* [ ] ./analysis/global/parallel/interference_bound_edf.v
* [ ] ./analysis/global/parallel/bertogna_edf_comp.v
* [ ] ./analysis/global/parallel/bertogna_fp_comp.v
* [ ] ./analysis/global/basic/workload_bound.v
* [ ] ./analysis/global/basic/interference_bound_fp.v
* [ ] ./analysis/global/basic/bertogna_fp_theory.v
* [ ] ./analysis/global/basic/bertogna_edf_theory.v
* [ ] ./analysis/global/basic/interference_bound.v
* [ ] ./analysis/global/basic/interference_bound_edf.v
* [ ] ./analysis/global/basic/bertogna_edf_comp.v
* [ ] ./analysis/global/basic/bertogna_fp_comp.v
* [ ] ./analysis/global/jitter/workload_bound.v
* [ ] ./analysis/global/jitter/interference_bound_fp.v
* [ ] ./analysis/global/jitter/bertogna_fp_theory.v
* [ ] ./analysis/global/jitter/bertogna_edf_theory.v
* [ ] ./analysis/global/jitter/interference_bound.v
* [ ] ./analysis/global/jitter/interference_bound_edf.v
* [ ] ./analysis/global/jitter/bertogna_edf_comp.v
* [ ] ./analysis/global/jitter/bertogna_fp_comp.v
## Implementations
* [ ] ./implementation/task.v
* [ ] ./implementation/uni/basic/schedule.v
* [ ] ./implementation/uni/basic/fp_rta_example.v
* [ ] ./implementation/uni/basic/schedule_tdma.v
* [ ] ./implementation/uni/basic/tdma_rta_example.v
* [ ] ./implementation/uni/basic/extraction_tdma.v
* [ ] ./implementation/uni/jitter/schedule.v
* [ ] ./implementation/uni/jitter/fp_rta_example.v
* [ ] ./implementation/uni/jitter/task.v
* [ ] ./implementation/uni/jitter/arrival_sequence.v
* [ ] ./implementation/uni/jitter/job.v
* [ ] ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
* [ ] ./implementation/uni/susp/dynamic/task.v
* [ ] ./implementation/uni/susp/dynamic/arrival_sequence.v
* [ ] ./implementation/uni/susp/dynamic/job.v
* [ ] ./implementation/uni/susp/schedule.v
* [ ] ./implementation/apa/bertogna_edf_example.v
* [ ] ./implementation/apa/schedule.v
* [ ] ./implementation/apa/task.v
* [ ] ./implementation/apa/bertogna_fp_example.v
* [ ] ./implementation/apa/arrival_sequence.v
* [ ] ./implementation/apa/job.v
* [ ] ./implementation/arrival_sequence.v
* [ ] ./implementation/global/parallel/bertogna_edf_example.v
* [ ] ./implementation/global/parallel/bertogna_fp_example.v
* [ ] ./implementation/global/basic/bertogna_edf_example.v
* [ ] ./implementation/global/basic/schedule.v
* [ ] ./implementation/global/basic/bertogna_fp_example.v
* [ ] ./implementation/global/jitter/bertogna_edf_example.v
* [ ] ./implementation/global/jitter/schedule.v
* [ ] ./implementation/global/jitter/task.v
* [ ] ./implementation/global/jitter/bertogna_fp_example.v
* [ ] ./implementation/global/jitter/arrival_sequence.v
* [ ] ./implementation/global/jitter/job.v
* [ ] ./implementation/job.vBjö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 job parameter.
>
> One improvement over the initial proposal is the use of "singleton classes" which do not require wrapping the parameter.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"2019-01-03T10:20:16ZBjö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
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 @prouxIn 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 Bozhkohttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/31Comments in Util-section2021-01-29T09:06:05ZSergey BozhkoComments in Util-sectionWe need to add comments to lemmas in Util-section.
* [x] [Bigcat](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/bigcat.v)
* [ ] [Counting](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/counting.v)
* [ ] [Div_mod](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/div_mod.v)
* [x] [Epsilon](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/epsilon.v)
* [ ] Delete section
* [x] [List](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/list.v)
* [ ] Replace `(* ... *)` with `(** ... *)`
* [ ] [Minmax](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/minmax.v)
* [ ] [Nat](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/nat.v)
* [x] [Nondecreasing](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/nondecreasing.v)
* [ ] [Notation](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/notation.v)
* [ ] [Rel](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/rel.v)
* [ ] [Rewrite_facilities](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/rewrite_facilities.v)
* [x] [Search_arg](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/search_arg.v)
* [ ] Replace `(* ... *)` with `(** ... *)`
* [ ] [Ssromega](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/ssromega.v)
* [x] [Step_function](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/step_function.v)
* [ ] Replace `(* ... *)` with `(** ... *)`
* [x] [Sum](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/sum.v)
* [ ] [Tactics](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/tactics.v)We need to add comments to lemmas in Util-section.
* [x] [Bigcat](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/bigcat.v)
* [ ] [Counting](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/counting.v)
* [ ] [Div_mod](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/div_mod.v)
* [x] [Epsilon](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/epsilon.v)
* [ ] Delete section
* [x] [List](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/list.v)
* [ ] Replace `(* ... *)` with `(** ... *)`
* [ ] [Minmax](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/minmax.v)
* [ ] [Nat](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/nat.v)
* [x] [Nondecreasing](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/nondecreasing.v)
* [ ] [Notation](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/notation.v)
* [ ] [Rel](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/rel.v)
* [ ] [Rewrite_facilities](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/rewrite_facilities.v)
* [x] [Search_arg](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/search_arg.v)
* [ ] Replace `(* ... *)` with `(** ... *)`
* [ ] [Ssromega](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/ssromega.v)
* [x] [Step_function](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/step_function.v)
* [ ] Replace `(* ... *)` with `(** ... *)`
* [x] [Sum](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/sum.v)
* [ ] [Tactics](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/blob/master/util/tactics.v)https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/14Generalize implementation of periodic arrival sequence2017-05-09T11:42:12ZFelipe CerqueiraGeneralize implementation of periodic arrival sequencehttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/1Definition of JLDP priority policy is too inflexible2019-10-22T13:48:11ZBjörn BrandenburgDefinition of JLDP priority policy is too inflexibleThe current definition of JLDP priority is as follows:
```
Definition jldp_policy := time -> JobIn arr_seq -> JobIn arr_seq -> bool.
```
This is too inflexible as one cannot define common JLDP policies such as *least laxity first* or *PD^2* in which the current priority of a job depends on how much service it has already received.
Instead, the definition should be generalized to depend on the schedule prefix up to the time at which it is queried.The current definition of JLDP priority is as follows:
```
Definition jldp_policy := time -> JobIn arr_seq -> JobIn arr_seq -> bool.
```
This is too inflexible as one cannot define common JLDP policies such as *least laxity first* or *PD^2* in which the current priority of a job depends on how much service it has already received.
Instead, the definition should be generalized to depend on the schedule prefix up to the time at which it is queried.Felipe CerqueiraFelipe Cerqueira