Commit 4b4a1336 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Omit type from definition of backlogged

parent 4134d178
......@@ -32,7 +32,7 @@ Module Platform.
(* A scheduler is work-conserving iff when a job j is backlogged,
all processors are busy with other jobs. *)
Definition work_conserving :=
forall (j: JobIn arr_seq) t,
forall j t,
backlogged job_cost sched j t ->
forall cpu, exists j_other,
scheduled_on sched j_other cpu t.
......@@ -40,7 +40,7 @@ Module Platform.
(* We also provide an alternative, equivalent definition of work-conserving
based on counting the number of scheduled jobs. *)
Definition work_conserving_count :=
forall (j: JobIn arr_seq) t,
forall j t,
backlogged job_cost sched j t ->
size (jobs_scheduled_at sched t) = num_cpus.
......
......@@ -34,7 +34,7 @@ Module Platform.
all processors are busy with other jobs.
NOTE: backlogged means that jitter has already passed. *)
Definition work_conserving :=
forall (j: JobIn arr_seq) t,
forall j t,
backlogged job_cost job_jitter sched j t ->
forall cpu, exists j_other,
scheduled_on sched j_other cpu t.
......@@ -42,7 +42,7 @@ Module Platform.
(* We also provide an alternative, equivalent definition of work-conserving
based on counting the number of scheduled jobs. *)
Definition work_conserving_count :=
forall (j: JobIn arr_seq) t,
forall j t,
backlogged job_cost job_jitter sched j t ->
size (jobs_scheduled_at sched t) = num_cpus.
......
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