add notion of supply to processor state

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.
 

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.
 

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.

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.

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.