Library rt.restructuring.model.readiness.jitter


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

Welcome to Coq 8.10.1 (October 2019)

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

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

From rt.util Require Import nat.

We define the readiness indicator function for models with release jitter (and no self-suspensions).
Definition of a generic type of release jitter parameter.
Class JobJitter (Job : JobType) := job_jitter : Job → duration.

Section ReadinessOfJitteryJobs.
Consider any kind of jobs...
  Context {Job : JobType}.

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

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

We say that a job is released at a time 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.

A job that experiences jitter is ready only when the jitter-induced delay has passed after its arrival and if it is 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 65)
  
  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 122)
  
  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 129)
  
  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 153)
  
  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 155)
  
  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 180)
  
  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 186)
  
  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.