basic.v

Require Import prosa.model.readiness.basic.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.behavior.completion.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.definitions.readiness.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.definitions.work_bearing_readiness.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]

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
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 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
    -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_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_priorities.

  (** 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
H1: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
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
H1: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
work_bearing_readiness arr_seq sched
    intros ? ? ARR PEND.Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
H1: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
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 => //.Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
H1: JLFP_policy Job
H_priority_is_reflexive: reflexive_priorities
j: Job
t: instant
ARR: arrives_in arr_seq j
PEND: pending sched j t
hep_job j j
    by eapply (H_priority_is_reflexive 0).
  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.