PROSA - Formally Proven Schedulability Analysis merge requestshttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests2024-03-22T13:24:48Zhttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/365make typeclasses into records2024-03-22T13:24:48ZKimaya Bedarkarmake typeclasses into recordsThe current design of tyepclasses is not good. If the typeclass has a single member function with a fairly generic type (examples: job arrival and job cost) then typeclass inference can not tell instances of the typeclasses from each oth...The current design of tyepclasses is not good. If the typeclass has a single member function with a fairly generic type (examples: job arrival and job cost) then typeclass inference can not tell instances of the typeclasses from each other. For example, the typeclass inference can confuse an instance of `JobCost` as an instance of `JobArrival`. To solve this, I put the functions of the typeclasses into records.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/364Remove work conservation dependence from the priority inversion file2024-03-28T13:05:26ZKimaya BedarkarRemove work conservation dependence from the priority inversion file- Currently the file `prosa.analysis.facts.busy_interval.pi` makes the assumption that the schedule is work-conserving (in the classic sense)
- Results from this file are used to bound the service inversion. Therefore the service inversi...- Currently the file `prosa.analysis.facts.busy_interval.pi` makes the assumption that the schedule is work-conserving (in the classic sense)
- Results from this file are used to bound the service inversion. Therefore the service inversion file also relies on the classic work conservation hypothesis.
- In this MR, I try to remove the work conservation hypothesis from some of the results in the PI file.
- Eventually, this will help us to remove the reliance of service inversion on the work conservation hypothesis.
- Removing the work conservation hypothesis crucially requires strengthening two lemmas regarding preemption.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/363Draft: RTA for RS-FP-EDF2024-03-28T10:50:35ZSergey BozhkoDraft: RTA for RS-FP-EDFhttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/362Draft: add file for non seq rta2024-03-27T20:31:48ZKimaya BedarkarDraft: add file for non seq rtahttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/359remove proof-term from JobReady type-class2024-02-13T23:21:47ZSergey Bozhkoremove proof-term from JobReady type-classMy attempt to merge !351 in a sequence of atomic commits.My attempt to merge !351 in a sequence of atomic commits.Björn BrandenburgBjörn Brandenburghttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/351Draft: Completed jobs aren't served2024-02-06T16:24:03ZSergey BozhkoDraft: Completed jobs aren't servedDepends on !320.
FYI: It is not a complete fix.Depends on !320.
FYI: It is not a complete fix.https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/321Draft: Elf preemption instantiations2024-03-23T11:10:21ZMeenal GuptaDraft: Elf preemption instantiationshttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/313Draft: PCP-RTA2024-01-16T12:30:37ZSergey BozhkoDraft: PCP-RTAI shook the dust off the old PCP-RTA proof.
And it actually works fine; currently, there are no admitted lemmas.
There are a few outdated things that we need to fix, though.I shook the dust off the old PCP-RTA proof.
And it actually works fine; currently, there are no admitted lemmas.
There are a few outdated things that we need to fix, though.Björn BrandenburgBjörn Brandenburghttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/191Draft: Initiate a Prosa Tutorial2023-03-10T09:51:45ZPierre RouxDraft: Initiate a Prosa TutorialThis is a follow up of !134 that I created on the wrong branch.
Rendering available at: http://prosa.mpi-sws.org/branches/tutorial/html-tutorial/tutorial.htmlThis is a follow up of !134 that I created on the wrong branch.
Rendering available at: http://prosa.mpi-sws.org/branches/tutorial/html-tutorial/tutorial.htmlhttps://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/190Draft: Prepare MathComp pull request2023-04-20T07:46:57ZPierre RouxDraft: Prepare MathComp pull requestThis is in preparation of a pull request to MathComp to push generic lemmas upstream (I only went through util/nat.v anf util/sum.v for now). Merge plan:
* do a pull request on MathComp with the lemmas tagged `TODO: PR MathComp`
* when t...This is in preparation of a pull request to MathComp to push generic lemmas upstream (I only went through util/nat.v anf util/sum.v for now). Merge plan:
* do a pull request on MathComp with the lemmas tagged `TODO: PR MathComp`
* when this PR is merged, adapt the current merge request and change the TODO comments into something like "will be in MathComp 1.15"
* merge the current merge request
* once MathComp 1.15 (or 2.0) is released and becomes the minimal version in Prosa, remove the tagged lemmas
Is there a volunteer to open the upstream pull request? I could certainly do it but I don't feel the most legitimate, not being an actual Prosa author. Note that I probably already made most of the work here by rewriting the proofs in a more MathComp style, so the procces should be reasonnably light. It's also a great opportunity to learn more about MathComp and how to write short and robust proof scripts with ssreflect.