Formalize pRTA from "Critical Instant for Probabilistic Timing Guarantees: Refuted and Revisited"
Please review this MR commit-by-commit.
Merge request reports
Activity
requested review from @bbb
assigned to @sbozhko
@fmarkovic, you can review the MR, too
added 1 commit
- 4078aa67 - add definitions and lemmas about arrival sequence
added 8 commits
- 6e14ade6 - define probabilistic deadline
- 47cbfc30 - copy some files from main Prosa
- 0e64ad8d - prove a few basic lemmas about arrivals
- c92d274d - define basic readiness with job abortion
- 3c8bbafa - delete [stdpp/total] typeclass to avoid name clash
- cf997cc4 - prove a few aux lemmas about lists and sums
- 33a726b0 - define common assumptions
- 4db59c9a - prove workload and carry-in properties
Toggle commit list-
rt/model/common_assumptions.v 0 → 10064422 {job_task : JobTask Job Task}. 23 24 Variable (ts : seq Task) (tsk : Task). 25 26 Definition arrivals_from_task_set := 27 forall (j : Job) (ω : Ω), arrives_in (arr_seq ω) j -> job_task j \in ts. 28 29 Definition arrivals_cost_consistent := 30 forall (j : Job) (ω : Ω), 31 arrives_in (arr_seq ω) j -> 32 isSome (job_cost j ω). 33 34 Definition pr_arrival_sequence_uniq := 35 forall (ω : Ω), arrival_sequence_uniq (arr_seq ω). 36 37 Definition restricted_deadlines := - rt/analysis/nth_cost.v 0 → 100644
93 { apply: leq_trans; last by apply H. 94 by move: IN1; rewrite mem_iota => /andP [_ T2]. } 95 { apply: leq_trans; last by apply H. 96 by move: IN2; rewrite mem_iota => /andP [_ T2]. } 97 { rewrite map_inj_uniq; last by intros ? ? E; inversion E. 98 by apply filter_uniq, index_enum_uniq. } 99 } 100 { rewrite map_inj_uniq. 101 - by apply index_enum_uniq. 102 - by intros ? ? E; inversion E. 103 } 104 Qed. 105 106 Lemma task_job_cost_independence : 107 forall (a b : nat), 108 independent [seq nth_cost tsk i | i <- iota a b]. - rt/model/pRBF.v 0 → 100644
3 4 (* --------------------------------- ProBsa --------------------------------- *) 5 From probsa.probability Require Export pmf. 6 7 (* ---------------------------------- Main ---------------------------------- *) 8 9 Section ProbRBF. 10 11 Context {Task : TaskType} 12 {α : MaxArrivals Task} 13 {pWCET_pmf : ProbWCET Task}. 14 15 (* NOTE: Ideally, ProbWCET should be a distrib. However, there are 16 some type-related problems. Converting pWCET into a proper 17 distribution is left as future maintenance work. *) 18 Definition to_distrib (pWCET : ProbWCET Task) : Task -> distrib [countType of nat] := - rt/model/assumptions/basic.v 0 → 100644
25 {job_task : JobTask Job Task}. 26 27 Variable (ts : seq Task) (tsk : Task). 28 29 Definition arrivals_from_task_set := 30 forall (j : Job) (ω : Ω), arrives_in (arr_seq ω) j -> job_task j \in ts. 31 32 Definition arrivals_cost_consistent := 33 forall (j : Job) (ω : Ω), 34 arrives_in (arr_seq ω) j -> 35 isSome (job_cost j ω). 36 37 Definition pr_arrival_sequence_uniq := 38 forall (ω : Ω), arrival_sequence_uniq (arr_seq ω). 39 40 Definition restricted_deadlines := - rt/model/assumptions/pr_must_be_ready.v 0 → 100644
5 Section PrMustBeReadyToExecture. 6 7 Context {Ω} {μ : measure Ω}. 8 9 Context {Job : finType} 10 {job_cost : JobCostRV Job Ω μ} 11 {job_arrival : JobArrivalRV Job Ω μ}. 12 13 Context {PState : ProcessorState Job}. 14 Variable sched : pr_schedule μ PState. 15 16 Let JobReadyRV := 17 forall (ω : Ω), 18 @JobReady 19 Job PState 20 (fun j => odflt0 (job_cost j) ω) (fun j => odflt0 (job_arrival j) ω).
Please register or sign in to reply