Library prosa.analysis.transform.swap
This file defines simple allocation substitutions and a swapping operation
as used for instance in the classic EDF optimality proof.
We begin by defining the notion of a schedule with a "tweaked" (i.e.,
overridden) allocation.
For any given type of jobs...
... any given type of processor states, ...
...consider any given reference schedule.
Suppose we are given a specific time t' ...
...and a replacement state new_state.
Then the schedule with replacement is simply one that returns the given
new_state at t', and the original allocation at all other times.
Definition replace_at (t : instant) :=
if t' == t then new_state else (original_sched t).
End ReplaceAt.
if t' == t then new_state else (original_sched t).
End ReplaceAt.
Based on replace_at, we define the notion of a schedule with swapped
allocations.
For any given type of jobs...
... any given type of processor states, ...
...consider any given reference schedule.
Definition swapped : schedule PState :=
let s1 := original_sched t1 in
let s2 := original_sched t2 in
let replaced_s1 := replace_at original_sched t1 s2 in
replace_at replaced_s1 t2 s1.
End Swapped.
let s1 := original_sched t1 in
let s2 := original_sched t2 in
let replaced_s1 := replace_at original_sched t1 s2 in
replace_at replaced_s1 t2 s1.
End Swapped.