Skip to content
Snippets Groups Projects

Edf equivalence

Closed LailaElbeheiry requested to merge edf-equivalence into master

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

Pipeline #33228 passed

Pipeline passed for 8a2a67d1 on edf-equivalence

Approval is optional

Closed by LailaElbeheiryLailaElbeheiry 4 years ago (Sep 9, 2020 4:25pm UTC)

Merge details

  • The changes were not merged into master.

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
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.
  • LailaElbeheiry added 1 commit

    added 1 commit

    • 30096139 - Progressed with the equivalence of EDF predicates proof

    Compare with previous version

  • LailaElbeheiry
  • LailaElbeheiry added 1 commit

    added 1 commit

    • d703eddc - Finish proof of equivalence of EDF predicates

    Compare with previous version

  • LailaElbeheiry added 1 commit

    added 1 commit

    • bd301c94 - Finish proof of equivalence of EDF predicates

    Compare with previous version

  • 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:

    1. I added one lemma in prosa.analysis.facts.behavior.completion, I'll add a standalone comment on that one.

    2. I added a section called NoDeadlineMissesImplications (there's already a comment for this one)

    3. 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?
  • LailaElbeheiry
  • LailaElbeheiry added 1 commit

    added 1 commit

    Compare with previous version

  • LailaElbeheiry added 1 commit

    added 1 commit

    Compare with previous version

  • LailaElbeheiry added 21 commits

    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

    Compare with previous version

  • LailaElbeheiry added 1 commit

    added 1 commit

    • 6c958f1a - restate optimality proof in terms policy compliance

    Compare with previous version

  • LailaElbeheiry added 1 commit

    added 1 commit

    Compare with previous version

  • Björn Brandenburg
  • LailaElbeheiry resolved all threads

    resolved all threads

  • LailaElbeheiry resolved all threads

    resolved all threads

  • LailaElbeheiry added 2 commits

    added 2 commits

    Compare with previous version

  • LailaElbeheiry added 2 commits

    added 2 commits

    • db6cea80 - Add proof of equivalence of EDF definitions
    • 3907f97f - Add optimality of work-conserving policy compliant schedules

    Compare with previous version

  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Please register or sign in to reply
    Loading