EDF optimality argument
- Aug 13, 2019
-
-
Björn Brandenburg authoredThis patch adds the classic EDF optimality argument: by swapping allocations, any schedule in which no job misses a deadline can be transformed into an EDF schedule in which also no job misses a deadline.
-
Björn Brandenburg authored
-
Björn Brandenburg authored
Given an interval [a, b), a function f: nat -> T, a predicate P, and a total, reflexive, transitive relation R, [search_arg f P R a b] will find the x in [a, b) that is an extremum w.r.t. R among all elements x in [a, b) for which (f x) satisfies P. For example, this can be used to search in a schedule for a scheduled job released before some reference time with the earliest deadline.
-
Björn Brandenburg authored
This patch adds functions for transforming a given schedule either by replacing the allocation at a given point, or by swapping the allocations at two points, together with a bunch of supporting lemmas and service invariants.
-
Björn Brandenburg authored
-
Björn Brandenburg authored
-
Björn Brandenburg authored
Points before or after an interval are not in the interval...
-
Björn Brandenburg authored
n + a - b + b - a = n if n >= b
-
Björn Brandenburg authored
...to match leq_ltn_trans in ssrnat
-
Björn Brandenburg authored
To allow reasoning about an entire class of types of schedules / processor modules, it's useful to have named definitions for various invariants that processor models ensure. Let's collect these centrally where we introduce processor models and schedules.
-