From 4b4a1336bc1a9f1e8e18e324f79a35f00fcc0010 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Sun, 14 Feb 2016 10:44:52 +0100
Subject: [PATCH] Omit type from definition of backlogged
---
model/basic/platform.v | 4 ++--
model/jitter/platform.v | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/model/basic/platform.v b/model/basic/platform.v
index 41234c3ac..8ed5569b5 100644
--- a/model/basic/platform.v
+++ b/model/basic/platform.v
@@ -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.
diff --git a/model/jitter/platform.v b/model/jitter/platform.v
index 7e71ae947..01886afe3 100644
--- a/model/jitter/platform.v
+++ b/model/jitter/platform.v
@@ -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.
--
GitLab