Library rt.restructuring.model.processor.ideal
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect.
From rt.restructuring.behavior Require Export all.
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: JobType.
Definition processor_state := option Job.
Global Program Instance pstate_instance : ProcessorState Job (option Job) :=
{
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) := s == Some j;
service_in j s := s == Some j;
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 297)
Job : JobType
j : Job
s : option Job
H : ~~ [exists c, s == Some j]
============================
(s == Some j) = 0
----------------------------------------------------------------------------- *)
rewrite /nat_of_bool.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
Job : JobType
j : Job
s : option Job
H : ~~ [exists c, s == Some j]
============================
(if s == Some j then 1 else 0) = 0
----------------------------------------------------------------------------- *)
case: ifP H=>//=_/existsP[].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 421)
Job : JobType
j : Job
s : option Job
============================
exists _ : unit_finType, true
----------------------------------------------------------------------------- *)
by ∃ tt.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.
service_in j s := s == Some j;
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 297)
Job : JobType
j : Job
s : option Job
H : ~~ [exists c, s == Some j]
============================
(s == Some j) = 0
----------------------------------------------------------------------------- *)
rewrite /nat_of_bool.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
Job : JobType
j : Job
s : option Job
H : ~~ [exists c, s == Some j]
============================
(if s == Some j then 1 else 0) = 0
----------------------------------------------------------------------------- *)
case: ifP H=>//=_/existsP[].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 421)
Job : JobType
j : Job
s : option Job
============================
exists _ : unit_finType, true
----------------------------------------------------------------------------- *)
by ∃ tt.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.
In this section we define the notion of idleness for ideal uni-processor.
Consider any type of job.
Consider any arrival sequence...
... and any ideal uniprocessor schedule of this arrival sequence.
We say that the processor is idle at time t iff there is no job being scheduled.