Edf equivalence
Proving the equivalence of the predicates respects_policy_at_preemption_point
and EDF_schedule
- where both specify that a schedule is an EDF one (given an EDF priority definition).
Merge request reports
Activity
- Resolved by Björn Brandenburg
Also, I'm not sure if I were supposed to create a new file and a new branch or not. Let me know if I should fix that.
- analysis/facts/edf_definitions.v 0 → 100644
72 73 End RespectsPolicyAtPreemptionPointsImpEDFSchedule. 74 75 Section EquivalenceOfEDFDefinitions. 76 77 (** For any given type of jobs, each characterized by execution 78 costs, an arrival time, an absolute deadline, and a preemption function... *) 79 Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job} `{JobPreemptable Job}. 80 81 (** ... and any valid job arrival sequence, ... *) 82 Variable arr_seq: arrival_sequence Job. 83 Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq. 84 85 (** ... and any schedule that is valid with respect to [arr_seq], ... *) 86 Variable sched : schedule (ideal.processor_state Job). 87 Hypothesis H_valid_schedule: valid_schedule sched arr_seq. changed this line in version 2 of the diff
added 1 commit
- 30096139 - Progressed with the equivalence of EDF predicates proof
- Resolved by Björn Brandenburg
added 1 commit
- d703eddc - Finish proof of equivalence of EDF predicates
added 1 commit
- bd301c94 - Finish proof of equivalence of EDF predicates
So, I finished the proof. Other than the fact that I'm not sure whether I've placed the proof in the corrext directory with a suitable file name or not, here are some more notes:
-
I added one lemma in prosa.analysis.facts.behavior.completion, I'll add a standalone comment on that one.
-
I added a section called
NoDeadlineMissesImplications
(there's already a comment for this one) -
In the proof, I assumed the following:
- jobs come from the arrival sequence (
jobs_come_from_arrival_sequence
) - jobs don't execute after completion (
completed_jobs_dont_execute
) - no job misses its deadline (
all_deadlines_of_arrivals_met
) Is that okay?
- jobs come from the arrival sequence (
-
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
Just stumbled across this MR. Since I wasn't tagged, I didn't get any notifications about your activity. I'll take a look.
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by Björn Brandenburg
- Resolved by LailaElbeheiry
added 21 commits
-
7a453a6e...a5637158 - 15 commits from branch
master
- 5425d0b6 - Proved optimality of work-conserving EDF schedules
- f0d65e06 - Adjust style of EDF work-conservation proofs
- 6e55d980 - Add proof of equivalence of EDF definitions
- 9f29b585 - Progressed with the equivalence of EDF predicates proof
- 43d03bda - Finish proof of equivalence of EDF predicates
- 6f933083 - Fix style
Toggle commit list-
7a453a6e...a5637158 - 15 commits from branch
added 1 commit
- 6c958f1a - restate optimality proof in terms policy compliance
- Resolved by LailaElbeheiry
So, is this done?
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
- Resolved by LailaElbeheiry
added 2 commits
- Resolved by Björn Brandenburg
For some reason the proof state script is failing for
analysis/facts/transform/edf_wc.v
. This seems to be overflowing from the previous merge request, but I don't know why
- Resolved by LailaElbeheiry