Keep only one definition of interference
When formalizing parallel jobs, we found a more generic definition of interference:
Definition job_interference (t1 t2: time) :=
\sum_(t1 <= t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t && scheduled_on sched job_other cpu t).
Perhaps we should use this definition everywhere. It can also be easily adapted to define interference under APA scheduling:
Definition job_interference (t1 t2: time) :=
\sum_(t1 <= t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t && scheduled_on sched job_other cpu t &&
can_execute_on j cpu t).