Commit 87f6ec3c authored by Björn Brandenburg's avatar Björn Brandenburg

generalize notion of jobs_backlogged_at

This is a general definition and not specific to a particular
implementation.
parent 6739de4f
......@@ -22,9 +22,6 @@ Section UniprocessorSchedule.
Variable sched_prefix : schedule (ideal.processor_state Job).
Definition jobs_backlogged_at (t : instant): seq Job :=
[seq j <- arrivals_up_to arr_seq t | backlogged sched_prefix j t].
Definition prev_job_nonpreemptive (t : instant) : bool:=
match t with
| 0 => false
......@@ -40,7 +37,7 @@ Section UniprocessorSchedule.
if prev_job_nonpreemptive t then
sched_prefix t.-1
else
supremum (hep_job_at t) (jobs_backlogged_at t).
supremum (hep_job_at t) (jobs_backlogged_at arr_seq sched_prefix t).
End JobAllocation.
......
......@@ -40,5 +40,11 @@ Section WorkConserving.
backlogged sched j t ->
exists j_other, scheduled_at sched j_other t.
(** Related to this, we define the set of all jobs that are backlogged at a
given time [t], i.e., the set of jobs that could be scheduled, and which
a work-conserving scheduler must hence consider. *)
Definition jobs_backlogged_at (t : instant): seq Job :=
[seq j <- arrivals_up_to arr_seq t | backlogged sched j t].
End WorkConserving.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment