Library prosa.model.readiness.jitter


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.behavior.all.

Require Import prosa.util.nat.

Job Model Parameter for Jobs Exhibiting Release Jitter

If a job exhibits release jitter, it is not immediately available for execution upon arrival, and can be scheduled only after its release, which occurs some (bounded) time after its arrival. We model this with the [job_jitter] parameter, which maps each job to its jitter duration.

Class JobJitter (Job : JobType) := job_jitter : Job duration.

Readiness of Jobs with Release Jitter

Based on the job model's jitter parameter, we define the readiness predicate for jogs with release jitter (and no self-suspensions).
Consider any kind of jobs...
  Context {Job : JobType}.

... and any kind of processor state.
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

Suppose jobs have an arrival time, a cost, and exhibit release jitter.
  Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.

We say that a job is released at a time [t] after its arrival if the job's release jitter has passed.
  Definition is_released (j : Job) (t : instant) := job_arrival j + job_jitter j t.

Based on the predicate [is_released], it is easy to state the notion of readiness for jobs subject to release jitter: a job is ready only if it is released and not yet complete.
  Global Program Instance jitter_ready_instance : JobReady Job PState :=
    {
      job_ready sched j t := is_released j t && ~~ completed_by sched j t
    }.
  Next Obligation.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 313)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H0 : JobArrival Job
  H1 : JobCost Job
  H2 : JobJitter Job
  sched : schedule PState
  j : Job
  t : instant
  H3 : is_released j t && ~~ completed_by sched j t
  ============================
  pending sched j t

----------------------------------------------------------------------------- *)


    move: H3 ⇒ /andP [REL UNFINISHED].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 370)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H0 : JobArrival Job
  H1 : JobCost Job
  H2 : JobJitter Job
  sched : schedule PState
  j : Job
  t : instant
  REL : is_released j t
  UNFINISHED : ~~ completed_by sched j t
  ============================
  pending sched j t

----------------------------------------------------------------------------- *)


    rewrite /pending.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 377)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H0 : JobArrival Job
  H1 : JobCost Job
  H2 : JobJitter Job
  sched : schedule PState
  j : Job
  t : instant
  REL : is_released j t
  UNFINISHED : ~~ completed_by sched j t
  ============================
  has_arrived j t && ~~ completed_by sched j t

----------------------------------------------------------------------------- *)


apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 401)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H0 : JobArrival Job
  H1 : JobCost Job
  H2 : JobJitter Job
  sched : schedule PState
  j : Job
  t : instant
  REL : is_released j t
  UNFINISHED : ~~ completed_by sched j t
  ============================
  has_arrived j t /\ ~~ completed_by sched j t

----------------------------------------------------------------------------- *)


split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 403)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H0 : JobArrival Job
  H1 : JobCost Job
  H2 : JobJitter Job
  sched : schedule PState
  j : Job
  t : instant
  REL : is_released j t
  UNFINISHED : ~~ completed_by sched j t
  ============================
  has_arrived j t

----------------------------------------------------------------------------- *)


    move: REL.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 428)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H0 : JobArrival Job
  H1 : JobCost Job
  H2 : JobJitter Job
  sched : schedule PState
  j : Job
  t : instant
  UNFINISHED : ~~ completed_by sched j t
  ============================
  is_released j t -> has_arrived j t

----------------------------------------------------------------------------- *)


rewrite /is_released /has_arrived.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 434)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H0 : JobArrival Job
  H1 : JobCost Job
  H2 : JobJitter Job
  sched : schedule PState
  j : Job
  t : instant
  UNFINISHED : ~~ completed_by sched j t
  ============================
  job_arrival j + job_jitter j <= t -> job_arrival j <= t

----------------------------------------------------------------------------- *)


    by apply leq_addk.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Defined.

End ReadinessOfJitteryJobs.