Require Export prosa.model.readiness.basic.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.definitions.readiness.
Require Export prosa.analysis.definitions.work_bearing_readiness.

Section LiuAndLaylandReadiness.

  (** We assume the basic (i.e., Liu & Layland)
      readiness model under which any pending job is ready. *)
  #[local] Existing Instance basic_ready_instance.

  (** Consider any kind of jobs ... *)
  Context {Job : JobType}.

  (** ... and any kind of processor state. *)
  Context {PState : ProcessorState Job}.

  (** Suppose jobs have an arrival time and a cost. *)
  Context `{JobArrival Job} `{JobCost Job}.

  (** The Liu & Layland readiness model is trivially non-clairvoyant. *)
  Fact basic_readiness_nonclairvoyance :
    nonclairvoyant_readiness basic_ready_instance.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
nonclairvoyant_readiness basic_ready_instance
  Proof.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
nonclairvoyant_readiness basic_ready_instance
    move=> sched sched' j h PREFIX t IN.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
sched, sched': schedule PState
j: Job
h: instant
PREFIX: identical_prefix sched sched' h
t: nat
IN: t <= h
job_ready sched j t = job_ready sched' j t
    rewrite /job_ready /basic_ready_instance.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
sched, sched': schedule PState
j: Job
h: instant
PREFIX: identical_prefix sched sched' h
t: nat
IN: t <= h
pending sched j t = pending sched' j t
    now apply (identical_prefix_pending _ _ h).
  Qed.

  (** Consider any job arrival sequence ... *)
  Variable arr_seq : arrival_sequence Job.

  (** ... and any schedule of these jobs. *)
  Variable sched : schedule PState.

  (** In the basic Liu & Layland model, a schedule satisfies that only ready
      jobs execute as long as jobs must arrive to execute and completed jobs
      don't execute, which we note with the following theorem. *)
  Lemma basic_readiness_compliance :
    jobs_must_arrive_to_execute sched ->
    completed_jobs_dont_execute sched ->
    jobs_must_be_ready_to_execute sched.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
jobs_must_arrive_to_execute sched ->
completed_jobs_dont_execute sched ->
jobs_must_be_ready_to_execute sched
  Proof.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
jobs_must_arrive_to_execute sched ->
completed_jobs_dont_execute sched ->
jobs_must_be_ready_to_execute sched
    move=> ARR COMP.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
jobs_must_be_ready_to_execute sched
    rewrite /jobs_must_be_ready_to_execute =>  j t SCHED.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t
job_ready sched j t
    rewrite /job_ready /basic_ready_instance /pending.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t
has_arrived j t && ~~ completed_by sched j t
    apply /andP; split.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t
has_arrived j t
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t
~~ completed_by sched j t
    -
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t
has_arrived j t by apply ARR.
    -
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t
~~ completed_by sched j t rewrite -less_service_than_cost_is_incomplete.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t
service sched j t < job_cost j
      by apply COMP.
  Qed.

  (** Consider a JLFP policy that indicates a reflexive
      higher-or-equal priority relation. *)
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.

  (** We show that the basic readiness model is a work-bearing
      readiness model. That is, at any time instant [t], if a job [j]
      is pending, then there exists a job (namely [j] itself) with
      higher-or-equal priority that is ready at time [t]. *)
  Fact basic_readiness_is_work_bearing_readiness :
    work_bearing_readiness arr_seq sched.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
work_bearing_readiness arr_seq sched
  Proof.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
work_bearing_readiness arr_seq sched
    intros j ? ARR PEND.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t: instant
ARR: arrives_in arr_seq j
PEND: pending sched j t
exists j_hp : Job,
  arrives_in arr_seq j_hp /\
  job_ready sched j_hp t /\ hep_job j_hp j
    exists j; repeat split => //.
  Qed.

End LiuAndLaylandReadiness.

(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
    will be able to apply it automatically. *)
Global Hint Resolve basic_readiness_is_work_bearing_readiness : basic_rt_facts.