diff --git a/behavior/schedule.v b/behavior/schedule.v
index 0baccfdf7508c6bbfa1efd132ac43c0f672a2945..5b8fcc5a495d51096f6d15a4bef3ce5998cba8ba 100644
--- a/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -34,12 +34,22 @@ Class ProcessorState (Job : JobType) :=
(** For a given processor state and core, the [scheduled_on] predicate
checks whether a given job is running on the given core. *)
scheduled_on : Job -> State -> Core -> bool;
- (** For a given processor state and core, the [service_on] function determines
- how much service a given job receives on the given core). *)
+ (** For a given processor state and core, the [supply_on] function
+ determines how much supply the core produces in the given
+ state). *)
+ supply_on : State -> Core -> work;
+ (** For a given processor state and core, the [service_on]
+ function determines how much service a given job receives on
+ the given core). *)
service_on : Job -> State -> Core -> work;
- (** We require [scheduled_on] and [service_on] to be consistent in
- the sense that a job can receive service (on a given core)
- only if it is also scheduled (on that core). *)
+ (** We require [service_on] and [supply_on] to be consistent in
+ the sense that a job cannot receive more service on a given
+ core in a given state than there is supply on the core in this
+ state. *)
+ service_on_le_supply_on :
+ forall j s r, service_on j s r <= supply_on s r;
+ (** In addition, a job can receive service (on a given core) only
+ if it is also scheduled (on that core). *)
service_on_implies_scheduled_on :
forall j s r, ~~ scheduled_on j s r -> service_on j s r = 0
}.
@@ -56,8 +66,10 @@ Coercion State : ProcessorState >-> Sortclass.
(i.e., on any core), and how much service the job receives
anywhere (i.e., across all cores). *)
Section ProcessorIn.
+
(** Consider any type of jobs... *)
Context {Job : JobType}.
+
(** ...and any type of processor state. *)
Context {State : ProcessorState Job}.
@@ -66,8 +78,14 @@ Section ProcessorIn.
Definition scheduled_in (j : Job) (s : State) : bool :=
[exists c : Core, scheduled_on j s c].
- (** For a given processor state, the [service_in] function determines how
- much service a given job receives in that state (across all cores). *)
+ (** For a given processor state, the [supply_in] function determines
+ how much supply the processor provides (across all cores) in the given state. *)
+ Definition supply_in (s : State) : work :=
+ \sum_(r : Core) supply_on s r.
+
+ (** For a given processor state, the [service_in] function
+ determines how much service a given job receives in that state
+ (across all cores). *)
Definition service_in (j : Job) (s : State) : work :=
\sum_(r : Core) service_on j s r.
diff --git a/model/processor/ideal.v b/model/processor/ideal.v
index a2387c75632370e06d0e34f2068217a56ec35059..5f76b4afc474c47d2c4122f7565439fc3ed857d8 100644
--- a/model/processor/ideal.v
+++ b/model/processor/ideal.v
@@ -32,13 +32,19 @@ Section State.
(** We say that a given job [j] is scheduled in a
given state [s] iff [s] is [Some j]. *)
scheduled_on j s (_ : unit) := s == Some j;
- (** Similarly, we say that a given job [j] receives service in a
- given state [s] iff [s] is [Some j]. *)
+ (** Any state of an ideal processor provides exactly one unit of
+ supply. *)
+ supply_on s (_ : unit) := 1;
+ (** We say that a given job [j] receives service in a given
+ state [s] iff [s] is [Some j]. *)
service_on j s (_ : unit) := if s == Some j then 1 else 0;
|}.
Next Obligation.
by move=> j s ?; rewrite /nat_of_bool; case: ifP => // ? /negP[].
Qed.
+ Next Obligation.
+ by move=> j s ?; rewrite /nat_of_bool; case: ifP => // ? /negP[].
+ Qed.
End State.
diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index 5298f4f4867ecd582e1ba7f576b63351c209469d..abe5efbab1b6551ecbc68ab52b980b09ce2fa864 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -49,9 +49,17 @@ Section Schedule.
(j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= scheduled_in j (mps cpu).
- (** Similarly, the service received by a given job [j] in a given
- multiprocessor state [mps] on a given processor of ID [cpu] is exactly
- the service given by [j] in the processor-local state [(mps cpu)]. *)
+ (** Similarly, the supply produced by a given multiprocessor state
+ [mps] on a given core [cpu] is exactly the supply provided by the
+ core-local state [(mps cpu)]. *)
+ Definition multiproc_supply_on
+ (mps : multiprocessor_state) (cpu : processor num_cpus)
+ := supply_in (mps cpu).
+
+ (** Next, the service received by a given job [j] in a given
+ multiprocessor state [mps] on a given processor of ID [cpu] is
+ exactly the service given by [j] in the processor-local state
+ [(mps cpu)]. *)
Definition multiproc_service_on
(j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= service_in j (mps cpu).
@@ -62,8 +70,12 @@ Section Schedule.
{|
State := multiprocessor_state;
scheduled_on := multiproc_scheduled_on;
+ supply_on := multiproc_supply_on;
service_on := multiproc_service_on
|}.
+ Next Obligation.
+ by move => ? ? ?; apply: leq_sum => c _; exact: service_on_le_supply_on.
+ Qed.
Next Obligation. by move=> ? ? ?; apply: service_in_implies_scheduled_in. Qed.
(** From the instance [multiproc_state], we get the function [service_in].
@@ -72,8 +84,6 @@ Section Schedule.
processors of the multiprocessor. *)
Lemma multiproc_service_in_eq : forall (j : Job) (mps : multiprocessor_state),
service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu).
- Proof.
- reflexivity.
- Qed.
+ Proof. reflexivity. Qed.
End Schedule.
diff --git a/model/processor/spin.v b/model/processor/spin.v
index 14bf807e6dd76f0b8e371ce4daea193a2ab52759..ec68bf12c9229dfb3a0d17cf89723225374e537d 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -35,7 +35,20 @@ Section State.
| Progress j' => j' == j
end.
- (** In contrast, job [j] receives service only if the given state [s] is
+ (** If the processor is idle, we assume that the supply equals 1,
+ indicating that the processor is ready to perform work. If the
+ processor is in the state [Spin j], then the job does not make
+ any progress, so effectively the supply is equal to
+ 0. Finally, the processor being in the state [Progress j]
+ indicates that the processor carries out 1 unit of useful work. *)
+ Definition spin_supply_on (s : processor_state) (_ : unit) : work :=
+ match s with
+ | Idle => 1
+ | Spin j => 0
+ | Progress j => 1
+ end.
+
+ (** A job [j] receives service only if the given state [s] is
[Progress j]. *)
Definition spin_service_on (s : processor_state) (_ : unit) : work :=
match s with
@@ -50,9 +63,12 @@ Section State.
interface for abstract processor states. *)
Program Definition pstate_instance : ProcessorState Job :=
{|
- State := processor_state;
+ State := processor_state;
scheduled_on := spin_scheduled_on;
+ supply_on := spin_supply_on;
service_on := spin_service_on
|}.
+ Next Obligation. by move => j [] // s [] /=; case: eqP. Qed.
Next Obligation. by move=> j [] //= j' _ /negbTE ->. Qed.
+
End State.
diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index fef498707f97ff9cf4f423040ea93ef62063d055..817fdaa8834d0fb7e9b2e39b58784cb061ba995f 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -12,11 +12,14 @@ Section State.
(** Consider any type of jobs. *)
Variable Job: JobType.
- (** We define the state of a variable-speed processor at a given time to be
- one of two possible cases: either a specific job is scheduled and
- progresses with a specific speed, or the processor is idle. *)
+ (** We define the state of a variable-speed processor at a given
+ time to be one of two possible cases: either a specific job is
+ scheduled and progresses with a specific speed, or the processor
+ is idle. Here, [Idle k] denotes a scenario where the processor
+ could have generated [k] units of service, but there is no job
+ being scheduled at that time instant. *)
Inductive processor_state :=
- Idle
+ | Idle (speed : nat)
| Progress (j : Job) (speed : nat).
(** Next, we define the semantics of the variable-speed processor state. *)
@@ -25,32 +28,44 @@ Section State.
(** Consider any job [j]. *)
Variable j : Job.
- (** Job [j] is scheduled in a given state [s] if [s] is not idle and [j]
- matches the job recorded in [s]. *)
+ (** Job [j] is scheduled in a given state [s] if [s] is not idle
+ and [j] matches the job recorded in [s]. *)
Definition varspeed_scheduled_on (s : processor_state) (_ : unit) : bool :=
match s with
- | Idle => false
+ | Idle _ => false
| Progress j' _ => j' == j
end.
- (** If it is scheduled in state [s], job [j] receives service proportional
- to the speed recorded in the state. *)
+ (** The processor state [Idle k] indicates that the processor is
+ ready to produce [k] units of supply; however, no job is
+ scheduled. If the processor is in state [Progress j k], it
+ produces [k] unit of work at a given time instant. *)
+ Definition varspeed_supply_on (s : processor_state) (_ : unit) : work :=
+ match s with
+ | Idle k => k
+ | Progress j' k => k
+ end.
+
+ (** If it is scheduled in state [s], job [j] receives service
+ proportional to the speed recorded in the state. *)
Definition varspeed_service_on (s : processor_state) (_ : unit) : work :=
match s with
- | Idle => 0
- | Progress j' speed => if j' == j then speed else 0
+ | Idle _ => 0
+ | Progress j' speed => if j' == j then speed else 0
end.
End Service.
- (** Finally, we connect the above definitions to the generic Prosa interface
- for processor states. *)
+ (** Finally, we connect the above definitions to the generic Prosa
+ interface for processor states. *)
Program Definition pstate_instance : ProcessorState Job :=
{|
- State := processor_state;
+ State := processor_state;
scheduled_on := varspeed_scheduled_on;
+ supply_on := varspeed_supply_on;
service_on := varspeed_service_on
|}.
+ Next Obligation. by move=> j [] //= s n; case: eqP. Qed.
Next Obligation. by move=> j [] //= j' v _; case: ifP. Qed.
End State.