Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • prepare_MC_PR
  • tutorial
  • classic-prosa protected
  • wip-hunspell
  • fset
  • embed_arr_seq_uniq
  • v0.5 protected
  • v0.4 protected
  • v0.3 protected
  • v0.2 protected
  • v0.1 protected
12 results
Blame Permalink
  • LailaElbeheiry's avatar
    271464a5
    add proof of equivalence of EDF definitions · 271464a5
    LailaElbeheiry authored and Björn Brandenburg's avatar Björn Brandenburg committed 
    This commit connects the two ways with which one can specify that a
schedule is an EDF schedule in PROSA: the `EDF_schedule` predicate
and the `respects_policy_at_preemption_point` with the EDF priority
policy predicate. We connect these two definitions by showing that
they're equivalent. We then restate the optimality proof of EDF
schedules using the proven equivalence.
    271464a5
    History
    add proof of equivalence of EDF definitions
    LailaElbeheiry authored and Björn Brandenburg's avatar Björn Brandenburg committed 
    This commit connects the two ways with which one can specify that a
schedule is an EDF schedule in PROSA: the `EDF_schedule` predicate
and the `respects_policy_at_preemption_point` with the EDF priority
policy predicate. We connect these two definitions by showing that
they're equivalent. We then restate the optimality proof of EDF
schedules using the proven equivalence.