From 96f52df249d001acf826567fa62316d14ee74182 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 15 Oct 2019 14:56:43 +0200
Subject: [PATCH] introduce 'work' as unit of service received or needed
---
restructuring/behavior/job.v | 6 +++++-
restructuring/behavior/schedule.v | 2 +-
2 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/restructuring/behavior/job.v b/restructuring/behavior/job.v
index 9743d13fc..8c28f72e8 100644
--- a/restructuring/behavior/job.v
+++ b/restructuring/behavior/job.v
@@ -4,8 +4,12 @@ From mathcomp Require Export eqtype ssrnat.
(* Throughout the library we assume that jobs have decidable equality. *)
Definition JobType := eqType.
+(* We define 'work' to denote the unit of service received or needed. In a
+ real system, this corresponds to the number of processor cycles. *)
+Definition work := nat.
+
(* Definition of a generic type of parameter relating jobs to a discrete cost. *)
-Class JobCost (Job : JobType) := job_cost : Job -> duration.
+Class JobCost (Job : JobType) := job_cost : Job -> work.
(* Definition of a generic type of parameter for job_arrival. *)
Class JobArrival (Job : JobType) := job_arrival : Job -> instant.
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index b61d05cbd..71d4153f5 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -12,7 +12,7 @@ Class ProcessorState (Job : JobType) (State : Type) :=
scheduled_in: Job -> State -> bool;
(* For a given processor state, the [service_in] function determines how much
service a given job receives in that state. *)
- service_in: Job -> State -> nat;
+ service_in: Job -> State -> work;
(* For a given processor state, a job does not receive service if it is not scheduled
in that state *)
service_implies_scheduled :
--
GitLab