PROSA - Formally Proven Schedulability Analysis merge requestshttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests2022-03-07T17:44:54Zhttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/195Draft: Resolve "Update the `esy` package"2022-03-07T17:44:54ZMartin Constantino–BodinDraft: Resolve "Update the `esy` package"Closes #88Closes #88Martin Constantino–BodinMartin Constantino–Bodinhttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/188Draft : Explicit policy in [respects_policy_at_preemption_point]2022-03-24T14:26:24ZKimaya BedarkarDraft : Explicit policy in [respects_policy_at_preemption_point]Currently, the policy under consideration is implicitly passed to `respects_policy_at_preemption_point`. This is unhelpful from a readability POV. The goal of this MR is to change the definition of `respects_policy_at_preemption_point` s...Currently, the policy under consideration is implicitly passed to `respects_policy_at_preemption_point`. This is unhelpful from a readability POV. The goal of this MR is to change the definition of `respects_policy_at_preemption_point` such that the policy has to be explicitly passed to it.https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/185Embeds arrival_uniq into arrival sequences2022-09-06T11:15:03ZPierre RouxEmbeds arrival_uniq into arrival sequencesThis avoid having to state arrival_uniq again and again almost each
time an arrival sequence is used, since arrival sequence without
uniq_arrival aren't really a thing.
If we decide to merge this, I could probably do the same for a few ...This avoid having to state arrival_uniq again and again almost each
time an arrival sequence is used, since arrival sequence without
uniq_arrival aren't really a thing.
If we decide to merge this, I could probably do the same for a few other hypotheses.https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/181WIP: POET2022-09-01T22:52:35ZSergey BozhkoWIP: POETI'll create a merge request so everyone can see the progress in this directionI'll create a merge request so everyone can see the progress in this directionhttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/173FIFO basic facts additions2021-11-22T13:30:24ZKimaya BedarkarFIFO basic facts additions* 2 new lemmas in FIFO basic facts
* 1 new lemma in `analysis/facts/model/workload.v`* 2 new lemmas in FIFO basic facts
* 1 new lemma in `analysis/facts/model/workload.v`https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/140Switch basic readiness to sequential readiness2021-09-03T10:39:23ZMarco MaidaSwitch basic readiness to sequential readinessThis is the first part of !130
This MR fixes problems that the basic readiness model causes to implementations.
Namely, consider the fixed-priority scheduling with basic readiness model. Note that neither fixed-priority nor basic read...This is the first part of !130
This MR fixes problems that the basic readiness model causes to implementations.
Namely, consider the fixed-priority scheduling with basic readiness model. Note that neither fixed-priority nor basic readiness imply the order in which two jobs of the same task should execute. Which means that the generic priority-driven implementation of a scheduler "pick a pending job with the highest priority that is ready and execute it" lacks the essential determinism regarding which job of a task to execute first.
Sequential readiness resolves this issue by stating that only the first pending job of a task is ready.https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/135documentation improvements2021-07-22T14:40:50ZBjörn Brandenburgdocumentation improvementsFound Martin's nice documentation improvements in a stale branch, which appears to have never been merged. Let's do that now.Found Martin's nice documentation improvements in a stale branch, which appears to have never been merged. Let's do that now.Björn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/134Draft: Initiate a Prosa Tutorial2022-02-22T16:24:19ZPierre RouxDraft: Initiate a Prosa TutorialThis is an attempt to revive Borislav's Prosa tutorial.
This is currently still in a very initial state but I hope to reach a reviewable state in the coming weeks.
This uses the Alectryon tool https://github.com/cpitclaudel/alectryon t...This is an attempt to revive Borislav's Prosa tutorial.
This is currently still in a very initial state but I hope to reach a reviewable state in the coming weeks.
This uses the Alectryon tool https://github.com/cpitclaudel/alectryon to build a nice webpage
while still remaining a simple vernacular file that can be stepped through.https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/133Draft: Adding branch with critical sections. Changes to beahviour/schedule.v,...2022-03-25T12:48:20ZptorrxDraft: Adding branch with critical sections. Changes to beahviour/schedule.v, new...Adding branch with critical sections. Changes to beahviour/schedule.v,
new file model/task/critical_sections.v,
minor changes in model/processor/multiprocessor.v ideal.v varspeed.v spin.v
This merge request proposes a formalization of...Adding branch with critical sections. Changes to beahviour/schedule.v,
new file model/task/critical_sections.v,
minor changes in model/processor/multiprocessor.v ideal.v varspeed.v spin.v
This merge request proposes a formalization of critical sections,
partially based on ECRTS18 https://prosa.mpi-sws.org/pdf/ecrts18-wip.pdf,
in particular for the service-based, temporal characterization,
but different insofar as we try to overcome what we perceived as a
potential semantic weakness, related to the direct association
of sections to jobs independently of any schedule.
Critical sections are generally meant to be sections of code that
involve access to resources. When a running job gets to the start of a
section, it requests access to the associated resources (at its
simplest, just one). In the case of mutually exclusive access, the
request may be added to a queue of similar ones, hence the job may be
blocked while it waits for its request to be handled. Once the job has
ended executing the critical section, it releases the lock.
In our view, there are two main modelling aspects. On one hand,
offline, a critical section is part of the code written for a task.
Empirically, by testing and cost analysis, it could be associated with
relative time bounds, loosely defined with respect to the received
service. On the other hand, if and when a critical section is
executed, can be generally known only at runtime, and it depends on
the actual control flow which might be affected by many factors,
including time variables. Of course, runtime absolute time values will
be expected to satisfy the task-level relative-time constraints.
The execution of critical sections can be characterized in terms of
events such as lock requests and release notifications, initiated by
the running job, and access granting issued by the scheduler/lock
manager. However, these events can be deduced by simply recording the
active lock requests and the locks held for each job.
Therefore we propose to split the representation of critical sections
into two layers: on one hand, a loose temporal specification at the
task level; on the other hand, information about lock requests and
held lock at the level of processor state. The two layers should be
related by consistency constraints.
The processor-state layer is implemented as a small extension of the
ProcessorState class in behaviour/schedule.v. Together with the lists
of the active requests and of the held locks for each job, we add the
type of the critical sections as a field, to avoid introducing an
extra parameter. The unit type is used as dummy, for the cases in
which there are no critical sections. From the refactoring point of
view, this extension involves only minor changes to the files in
model/processor which contains instantiations of ProcessorState.
The static specification layer is presented in a new file,
model/task/critical_sections.v, which depends on the definition of
task in concept.v. This specification follows the main lines of the
one described in ECRTS18, with some differences.
In fact, we worried that the notion of job, independently of any
schedule, might not provide a sufficiently robust basis for the
determination of the critical sections that are executed.
In the task-based specification we are proposing, we intend each control
flow branch to be associated with a list of sections. We express this
implicitly, by associating the task with a list of lists of sections.
Consistently with this non-deterministic aspect, we opt for
a loose temporal specification: we give earliest start, latest start,
minimum length and maximum length of a section, rather than strict
start and end points.
The last part of critical_sections.v contains constraints that
express critical-section validity of a schedule with respect to a
static specification.
Following what appears to be a general approach in Prosa, we use
Coq type classes to represent what, in a more concrete,
non-extensible representation, could be fields in a record definition.
We use Coq definitions to introduce constraints which, from the point
of view of our current understanding, should not be normally proven,
but only assumed as hypotheses to support higher-level reasoning.
Looking forward to your feedback!https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/132WIP: Pi cleanup2021-03-15T17:06:32ZSergey BozhkoWIP: Pi cleanupThis MR separates the general notion of priority inversion and its specific manifestation for ideal uniprocessor.
Note that this MR depends in MRs !115 and !129This MR separates the general notion of priority inversion and its specific manifestation for ideal uniprocessor.
Note that this MR depends in MRs !115 and !129Björn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/108WIP: Preemption model compliance2020-09-01T09:25:38ZLailaElbeheiryWIP: Preemption model compliancehttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/101WIP: Partitioned2022-03-11T15:34:46ZMaxime LesourdWIP: PartitionedThis is a draft of the concepts needed to work on partitioned schedules. It is driven by the ongoing work in Grenoble on generic CPA but we want aim to formalize partitioned scheduling in a manner that makes sense on its own and can be r...This is a draft of the concepts needed to work on partitioned schedules. It is driven by the ongoing work in Grenoble on generic CPA but we want aim to formalize partitioned scheduling in a manner that makes sense on its own and can be reused, as such we would like to get some feedback before we integrate it into the CPA analysis.
The intuition is that we rely on the Cores defined in ProcessorState to project per-core arrival sequences and schedules on which scheduling models can be applied.
The main design choice is to provide the definitions for any ProcessorState. An alternative would have been to only consider multiprocessor schedules in the sense of model/processor/multiprocessor.v for which the construction can be made nicer but is not as generic. It seems to me that since we have a notion of core in the definition of ProcessorState we might as well rely on it to provide a generic construction as long as it is readable.
The roadmap before we can integrate this is as follows:
- [x] Fixing the omission of service on a core in behavior/schedule.v
- [x] Definition of the projections
- [x] Per-core specification of a model
- [ ] Specific definitions related to job and task partitioned schedules (no migration)
- [ ] Examples to show how to define a simple model using the provided utilities
- [ ] Basic theory of partitioned schedules (this will probably come with the developments related to CPA)
The current state implied some changes to the behavior/schedule.v files, I have fixed the related proofs so that it compiles but I still have some work to make the CI happy on all supported pairs of coq/ssreflect versions we cover.
The rest of the relevant changes are collected in model/schedule/partitioned.v
I will be away until July 27th, so this will be stable for a week after which I will continue as this is on the critical path for the CPA proof.https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/99wip: observation interval proofs2020-06-19T02:30:39ZGhost Userwip: observation interval proofsMerge request from branch `oio` which includes notion of offset (which wasn't there in the original OI MR).
(*
Why the branch name `oio`?
=> I wanted to name it so that it represents "OI with offset included", so I thought of naming `...Merge request from branch `oio` which includes notion of offset (which wasn't there in the original OI MR).
(*
Why the branch name `oio`?
=> I wanted to name it so that it represents "OI with offset included", so I thought of naming `oi_offset` but this would be too long to write frequent commit messages, so I shortened it to `oio`.
*)https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/92WIP : Restricted Supply2020-03-26T23:26:21ZSergey BozhkoWIP : Restricted SupplyMarco MaidaMarco Maidahttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/90WIP : Restricted Supply2020-03-26T23:22:17ZSergey BozhkoWIP : Restricted SupplyMarco MaidaMarco Maidahttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/86WIP: [not to be merged] Run CI for Opam file for 0.42020-02-24T15:11:46ZPierre RouxWIP: [not to be merged] Run CI for Opam file for 0.4This is not meant to be merged, this is just to run the CI on 0.4 to know for sure which constraints to put in the opam file.This is not meant to be merged, this is just to run the CI on 0.4 to know for sure which constraints to put in the opam file.https://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/80Network calculus2020-01-20T08:28:53ZPierre RouxNetwork calculusThis is the work of @Lucien formalizing Network-Calculus, following @M.Boyer et al. book.
@sophie link with Prosa will come (soon) in a separate merge request
@M.Boyer feel free to criticize the choice of file and theorem names / repar...This is the work of @Lucien formalizing Network-Calculus, following @M.Boyer et al. book.
@sophie link with Prosa will come (soon) in a separate merge request
@M.Boyer feel free to criticize the choice of file and theorem names / repartition / documentation (`make gallinahtml` to build the doc or just ask I'll give you the html pages)
I still have to update the .gitlab file to go through the CIhttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/40WIP: Resources2019-10-18T13:25:13ZMaxime LesourdWIP: ResourcesProposal to expose a concept of Resource in ProcessorState, allowing us to define generic predicates for work conserving and priority based scheduling policiesProposal to expose a concept of Resource in ProcessorState, allowing us to define generic predicates for work conserving and priority based scheduling policieshttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/36WIP: add general notion of "job readiness"2019-08-21T09:31:09ZBjörn BrandenburgWIP: add general notion of "job readiness"This adds a new generic parameter `job_ready` that determines whether a given job is ready at a given time in a given schedule. For different workload models (e.g., release jitter, self-suspensions, shared resources, etc.), appropriate d...This adds a new generic parameter `job_ready` that determines whether a given job is ready at a given time in a given schedule. For different workload models (e.g., release jitter, self-suspensions, shared resources, etc.), appropriate definitions of `job_ready` can be provided. This allows us to define work-conservation and priority-compliance in a general way, which is needed to fully address #12.
As an example, I've defined `job_ready` for the workload model with release jitter (and without self-suspensions).
This is just a sketch; what do you think?
CC: @sbozhko @sophie @mlesourd @prouxhttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/35WIP: expose number of idle cores2019-10-29T18:04:02ZBjörn BrandenburgWIP: expose number of idle coresWhat do you think of this way of defining work-conservation in a way that *transparently* works for both uni- and multiprocessor platforms?
To me, this looks appealing. The only downside that I see is that in proofs one doesn't get to ...What do you think of this way of defining work-conservation in a way that *transparently* works for both uni- and multiprocessor platforms?
To me, this looks appealing. The only downside that I see is that in proofs one doesn't get to destruct the `exists j_other` right away (i.e., we'd need a few helper lemmas to establish that `idle_in s == 0` implies `exists j_other`.
We could also keep both notions and establish equivalency of the two definitions (once for each processor model).
CC: @sbozhko @mlesourd @sophie