PROSA - Formally Proven Schedulability Analysis merge requestshttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests2024-02-25T19:55:23Zhttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/358port to MathComp 22024-02-25T19:55:23ZBjörn Brandenburgport to MathComp 2Björn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/327Generalize one lemma2024-02-14T15:40:47ZKimaya BedarkarGeneralize one lemmaKimaya BedarkarKimaya Bedarkarhttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/360add some lemmas about RBFs2024-02-13T17:46:20ZKimaya Bedarkaradd some lemmas about RBFshttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/333add some guidelines2024-02-09T17:22:03ZKimaya Bedarkaradd some guidelineshttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/361add some lemmas about workload2024-02-09T09:50:17ZKimaya Bedarkaradd some lemmas about workloadhttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/320prove RS-RTA for fully preemptive FP2024-02-07T13:45:57ZSergey Bozhkoprove RS-RTA for fully preemptive FPBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/353small refactor of arrivals lemmas2024-02-06T15:43:50ZKimaya Bedarkarsmall refactor of arrivals lemmashttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/357prove that busy intervals are bounded for RS-FP2024-01-25T12:25:15ZSergey Bozhkoprove that busy intervals are bounded for RS-FPBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/356Prove a few auxiliary lemmas2024-01-24T15:01:19ZSergey BozhkoProve a few auxiliary lemmasBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/355Prove that job's max lower-priority non-preemptive segment is bounded2024-01-24T10:36:17ZSergey BozhkoProve that job's max lower-priority non-preemptive segment is boundedBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/352Prove that abstract search space is a subset of RS-FP search space2024-01-23T17:24:41ZSergey BozhkoProve that abstract search space is a subset of RS-FP search spaceBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/354Refactor assumptions in a lemma about RBF2024-01-23T15:44:03ZSergey BozhkoRefactor assumptions in a lemma about RBFLemma about `task_rbf ε >= task_cost tsk` assumes that there exists a job of `tsk`. However, the only goal of assuming the existence of a job is to obtain the fact that `max_arrivals tsk ε > 0`. One can directly assume that the arrival c...Lemma about `task_rbf ε >= task_cost tsk` assumes that there exists a job of `tsk`. However, the only goal of assuming the existence of a job is to obtain the fact that `max_arrivals tsk ε > 0`. One can directly assume that the arrival curve is positive and hence remove the superfluous dependency.Björn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/350De-duplicate [blocking_bound]2024-01-22T10:39:55ZSergey BozhkoDe-duplicate [blocking_bound]This MR removes a few repeating [blocking_bound] definitionsThis MR removes a few repeating [blocking_bound] definitionsBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/349Prove lemmas about restricted supply proc. and change SBF def2024-01-19T13:20:41ZSergey BozhkoProve lemmas about restricted supply proc. and change SBF defBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/348Add I/IW instantiation for restricted supply2024-01-19T12:05:21ZSergey BozhkoAdd I/IW instantiation for restricted supplyBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/347Prove existence of abstract busy interval2024-01-18T12:09:42ZSergey BozhkoProve existence of abstract busy intervalProofs of existence for busy intervals are usually quite long. They also depend on specific scheduling policy and preemption model. This leads to some unnecessary duplication. This commit introduces a proof of existence for abstract busy...Proofs of existence for busy intervals are usually quite long. They also depend on specific scheduling policy and preemption model. This leads to some unnecessary duplication. This commit introduces a proof of existence for abstract busy interval. The idea is to instantiate this proof for specific policies removing the duplication.Björn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/346generalize proof and improve structure2024-01-16T12:27:22ZSergey Bozhkogeneralize proof and improve structureBjörn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/345restructure I/IW instantiation files2024-01-15T14:48:23ZSergey Bozhkorestructure I/IW instantiation filesThere are a lot of lemmas inside of [abstract/ideal/iw_instantiation.v] that are not specific to ideal uni-processor. This MR moves such lemmas to [abstract/iw_auxiliary.v]There are a lot of lemmas inside of [abstract/ideal/iw_instantiation.v] that are not specific to ideal uni-processor. This MR moves such lemmas to [abstract/iw_auxiliary.v]Björn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/341release jitter propagation2024-01-15T09:42:52ZBjörn Brandenburgrelease jitter propagationGoal: roll release jitter into arrival curves, following the classic approach by Audsley et al. (1993), and show that it all fits together.Goal: roll release jitter into arrival curves, following the classic approach by Audsley et al. (1993), and show that it all fits together.Björn BrandenburgBjörn Brandenburghttps://gitlab.rts.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/344Define some notions about workload and service + clean up2024-01-15T09:13:05ZSergey BozhkoDefine some notions about workload and service + clean upBjörn BrandenburgBjörn Brandenburg