Skip to content

Move lemma [early_hep_job_is_scheduled] to separate file

Sergey Bozhko requested to merge sbozhko/rt-proofs:move_lemma into master

Partially solves #78 (closed)

  • Move file facts/edf.v to facts/priority/edf.v
  • Move lemma early_hep_job_is_scheduled to a separate file so it no longer depends on EDF schedule
  • Dependence on ideal schedule is still present, because early_hep_job_is_scheduled uses lemma scheduling_of_any_segment_starts_with_preemption_time which assumes an ideal scheduler

Merge request reports