Library prosa.model.processor.ideal
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect.
Require Export prosa.behavior.all.
The Ideal Uniprocessor Model
Consider any type of jobs.
We define the ideal "processor state" as an [option Job], which means
that it is either [Some j] (where [j] is a [Job]) or [None] (which we use
to indicate an idle instant).
Based on this definition, we say that a given job [j] is scheduled in a
given state [s] iff [s] is [Some j].
Similarly, we say that a given job [j] receives service in a given state
[s] iff [s] is [Some j].
Next, we connect the just-defined notion of an ideal processor state with
the generic interface for the processor-state abstraction in Prosa by
declaring a so-called instance of the [ProcessorState] typeclass.
As this is a uniprocessor model, cores are implicitly defined
as the [unit] type containing a single element as a placeholder.
scheduled_on j s (_ : unit) := ideal_scheduled_at j s;
service_in j s := ideal_service_in j s;
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2551)
Job : JobType
ideal_scheduled_at, ideal_service_in := fun j : Job => eq_op^~ (Some j)
: Job -> processor_state -> bool
j : Job
s : processor_state
H : ~~ [exists c, ideal_scheduled_at j s]
============================
ideal_service_in j s = 0
----------------------------------------------------------------------------- *)
rewrite /ideal_service_in /nat_of_bool.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2558)
Job : JobType
ideal_scheduled_at, ideal_service_in := fun j : Job => eq_op^~ (Some j)
: Job -> processor_state -> bool
j : Job
s : processor_state
H : ~~ [exists c, ideal_scheduled_at j s]
============================
(if s == Some j then 1 else 0) = 0
----------------------------------------------------------------------------- *)
case: ifP H =>//= SOME /existsP[].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2674)
Job : JobType
ideal_scheduled_at, ideal_service_in := fun j : Job => eq_op^~ (Some j)
: Job -> processor_state -> bool
j : Job
s : processor_state
SOME : s == Some j
============================
exists _ : unit_finType, ideal_scheduled_at j s
----------------------------------------------------------------------------- *)
by ∃ tt.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.
service_in j s := ideal_service_in j s;
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2551)
Job : JobType
ideal_scheduled_at, ideal_service_in := fun j : Job => eq_op^~ (Some j)
: Job -> processor_state -> bool
j : Job
s : processor_state
H : ~~ [exists c, ideal_scheduled_at j s]
============================
ideal_service_in j s = 0
----------------------------------------------------------------------------- *)
rewrite /ideal_service_in /nat_of_bool.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2558)
Job : JobType
ideal_scheduled_at, ideal_service_in := fun j : Job => eq_op^~ (Some j)
: Job -> processor_state -> bool
j : Job
s : processor_state
H : ~~ [exists c, ideal_scheduled_at j s]
============================
(if s == Some j then 1 else 0) = 0
----------------------------------------------------------------------------- *)
case: ifP H =>//= SOME /existsP[].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2674)
Job : JobType
ideal_scheduled_at, ideal_service_in := fun j : Job => eq_op^~ (Some j)
: Job -> processor_state -> bool
j : Job
s : processor_state
SOME : s == Some j
============================
exists _ : unit_finType, ideal_scheduled_at j s
----------------------------------------------------------------------------- *)
by ∃ tt.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.
Consider any type of jobs...
... and any ideal uniprocessor schedule of such jobs.
We say that the processor is idle at time t iff there is no job being scheduled.