Commit 37121eb7 authored by Björn Brandenburg's avatar Björn Brandenburg

clean up the new schedule definitions

- Consistently use JobType rather than eqType directly.
- Fix the comments style.
parent eee872d9
......@@ -10,7 +10,7 @@ Section Composition.
[service] and [service_during]. *)
(* Consider any job type and any processor state. *)
Context {Job: eqType}.
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
......
From rt.restructuring.behavior Require Export schedule.schedule.
(** First let us define the notion of an ideal schedule state,
* as done in Prosa so far: either a job is scheduled or the system is idle.
*)
(** First let us define the notion of an ideal schedule state, as done in Prosa
so far: either a job is scheduled or the system is idle. *)
Section State.
Variable Job: eqType.
Variable Job: JobType.
Definition processor_state := option Job.
......
......@@ -3,7 +3,7 @@ From rt.restructuring.behavior.schedule Require Export schedule.
Section Schedule.
Variable Job: eqType.
Variable Job: JobType.
Variable processor_state: Type.
Context `{ProcessorState Job processor_state}.
......
......@@ -2,19 +2,19 @@ From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From rt.restructuring.behavior Require Export arrival.arrival_sequence.
(* We define the notion of a generic processor state. The processor state type
* determines aspects of the execution environment are modeled (e.g., overheads, spinning).
* In the most simple case (i.e., Ideal.processor_state), at any time,
* either a particular job is either scheduled or it is idle. *)
Class ProcessorState (Job : eqType) (State : Type) :=
determines aspects of the execution environment are modeled (e.g., overheads, spinning).
In the most simple case (i.e., Ideal.processor_state), at any time,
either a particular job is either scheduled or it is idle. *)
Class ProcessorState (Job : JobType) (State : Type) :=
{
(* For a given processor state, the [scheduled_in] predicate checks whether a given
* job is running in that state. *)
job is running in that state. *)
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 a given job receives in that state. *)
service_in: Job -> State -> nat;
(* For a given processor state, a job does not receive service if it is not scheduled
* in that state *)
in that state *)
service_implies_scheduled :
forall j s, scheduled_in j s = false -> service_in j s = 0
}.
......@@ -23,7 +23,7 @@ Class ProcessorState (Job : eqType) (State : Type) :=
Definition schedule (PState : Type) := instant -> PState.
Section Schedule.
Context {Job : eqType} {PState : Type}.
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
Variable sched : schedule PState.
......
From rt.restructuring.behavior.schedule Require Export schedule.
(** Next we define a processor state that includes the possibility of spinning,
* where spinning jobs do not progress (= don't get service). *)
where spinning jobs do not progress (= don't get service). *)
Section State.
Variable Job: eqType.
Variable Job: JobType.
Inductive processor_state :=
Idle
......
......@@ -3,7 +3,7 @@ From rt.restructuring.behavior.schedule Require Export schedule.
(** Next, let us define a schedule with variable execution speed. *)
Section State.
Variable Job: eqType.
Variable Job: JobType.
Inductive processor_state :=
Idle
......
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