Require Import prosa.util.int.
[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]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default]
Notation "_ - _" was already used in scope
distn_scope. [notation-overridden,parsing,default]
Require Import prosa.model.priority.gel.
[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 Import prosa.model.schedule.priority_driven.
Require Import prosa.analysis.facts.model.sequential.
Require Import prosa.analysis.facts.priority.sequential.

(** In this file we state and prove some basic facts
    about the GEL scheduling policy. *)
Section GELBasicFacts.

  (** Consider any type of tasks and jobs. *)
  Context `{Task : TaskType} {Job : JobType}
    `{JobTask Job Task} `{PriorityPoint Task} {Arrival : JobArrival Job}.

  (** Under GEL, [hep_job] is a statement about absolute priority points. *)
  Fact hep_job_priority_point :
    forall j j',
      hep_job j j' = ((job_arrival j)%:R + task_priority_point (job_task j)
                      <= (job_arrival j')%:R + task_priority_point (job_task j'))%R.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
forall j j' : Job,
hep_job j j' =
((job_arrival j)%:R + task_priority_point (job_task j) <=
 (job_arrival j')%:R +
 task_priority_point (job_task j'))%R
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
forall j j' : Job,
hep_job j j' =
((job_arrival j)%:R + task_priority_point (job_task j) <=
 (job_arrival j')%:R +
 task_priority_point (job_task j'))%R by move=> j j'; rewrite /hep_job/GEL/job_priority_point. Qed.

  (** If we are looking at two jobs of the same task, then [hep_job] is a
      statement about their respective arrival times. *)
  Fact hep_job_arrival_gel :
    forall j j',
      same_task j j' ->
      hep_job j j' = (job_arrival j <= job_arrival j').
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
forall j j' : Job,
same_task j j' ->
hep_job j j' = (job_arrival j <= job_arrival j')
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
forall j j' : Job,
same_task j j' ->
hep_job j j' = (job_arrival j <= job_arrival j')
    move=> j j' /eqP SAME.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
j, j': Job
SAME: job_task j = job_task j'
hep_job j j' = (job_arrival j <= job_arrival j')
    by rewrite hep_job_priority_point SAME; lia.
  Qed.

  Section HEPJobArrival.
    (** Consider a job [j]... *)
    Variable j : Job.

    (** ... and a higher or equal priority job [j']. *)
    Variable j' : Job.
    Hypothesis H_j'_hep : hep_job j' j.

    (** The arrival time of [j'] is bounded as follows. *)
    Lemma hep_job_arrives_before :
      ((job_arrival j')%:R <=
         (job_arrival j)%:R +
           task_priority_point (job_task j) - task_priority_point (job_task j'))%R.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
((job_arrival j')%:R <=
 (job_arrival j)%:R + task_priority_point (job_task j) -
 task_priority_point (job_task j'))%R
    Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
((job_arrival j')%:R <=
 (job_arrival j)%:R + task_priority_point (job_task j) -
 task_priority_point (job_task j'))%R by move : H_j'_hep; rewrite hep_job_priority_point; lia. Qed.

    (** Using the above lemma, we prove that for any
        higher-or-equal priority job [j'], the term
        [job_arrival j +  task_priority_point (job_task j) -
        task_priority_point (job_task j')] is positive.  *)
    Corollary hep_job_arrives_after_zero :
      (0 <= (job_arrival j)%:R +
             task_priority_point (job_task j) - task_priority_point (job_task j'))%R.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
(0 <=
 (job_arrival j)%:R + task_priority_point (job_task j) -
 task_priority_point (job_task j'))%R
    Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
(0 <=
 (job_arrival j)%:R + task_priority_point (job_task j) -
 task_priority_point (job_task j'))%R exact: le_trans hep_job_arrives_before. Qed.

  End HEPJobArrival.

  (** Next, we prove that the GEL policy respects sequential tasks. *)
  Lemma GEL_respects_sequential_tasks:
    policy_respects_sequential_tasks (GEL Job Task).
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
policy_respects_sequential_tasks (GEL Job Task)
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
policy_respects_sequential_tasks (GEL Job Task) by move =>  j1 j2 TSK ARR; rewrite hep_job_arrival_gel. Qed.

  (** In this section, we prove that in a schedule following
      the GEL policy, tasks are always sequential. *)
  Section SequentialTasks.

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

    (** Allow for any uniprocessor model. *)
    Context {PState : ProcessorState Job}.
    Hypothesis H_uniproc : uniprocessor_model PState.

    (** Next, consider any schedule of the arrival sequence, ... *)
    Variable sched : schedule PState.

    Context `{JobCost Job}.
    Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

    (** ... allow for any work-bearing notion of job readiness, ... *)
    Context `{@JobReady Job PState _ Arrival}.
    Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

    (** ... and assume that the schedule is valid. *)
    Hypothesis H_sched_valid : valid_schedule sched arr_seq.

    (** In addition, we assume the existence of a function mapping jobs
        to their preemption points ... *)
    Context `{JobPreemptable Job}.

    (** ... and assume that it defines a valid preemption model. *)
    Hypothesis H_valid_preemption_model:
      valid_preemption_model arr_seq sched.

    (** Next, we assume that the schedule respects the scheduling policy at every preemption point. *)
    Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (GEL Job Task).

    (** To prove sequentiality, we use the lemma
        [early_hep_job_is_scheduled]. Clearly, under the GEL priority
        policy, jobs satisfy the conditions described by the lemma
        (i.e., given two jobs [j1] and [j2] from the same task, if [j1]
        arrives earlier than [j2], then [j1] always has a higher
        priority than job [j2], and hence completes before [j2]);
        therefore GEL implies the [sequential_tasks] property. *)
    Lemma GEL_implies_sequential_tasks:
      sequential_tasks arr_seq sched.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
H_uniproc: uniprocessor_model PState
sched: schedule PState
H1: JobCost Job
H_valid_arrivals: valid_arrival_sequence arr_seq
H2: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H3: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (GEL Job Task)
sequential_tasks arr_seq sched
    Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
H_uniproc: uniprocessor_model PState
sched: schedule PState
H1: JobCost Job
H_valid_arrivals: valid_arrival_sequence arr_seq
H2: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H3: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (GEL Job Task)
sequential_tasks arr_seq sched
      move => j1 j2 t ARR1 ARR2 SAME LT.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
H_uniproc: uniprocessor_model PState
sched: schedule PState
H1: JobCost Job
H_valid_arrivals: valid_arrival_sequence arr_seq
H2: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H3: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (GEL Job Task)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
scheduled_at sched j2 t -> completed_by sched j1 t
      apply: early_hep_job_is_scheduled => //.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
H_uniproc: uniprocessor_model PState
sched: schedule PState
H1: JobCost Job
H_valid_arrivals: valid_arrival_sequence arr_seq
H2: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H3: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (GEL Job Task)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
always_higher_priority j1 j2
      rewrite always_higher_priority_jlfp !hep_job_arrival_gel //.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
H_uniproc: uniprocessor_model PState
sched: schedule PState
H1: JobCost Job
H_valid_arrivals: valid_arrival_sequence arr_seq
H2: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H3: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (GEL Job Task)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
(job_arrival j1 <= job_arrival j2) &&
~~ (job_arrival j2 <= job_arrival j1)
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
H_uniproc: uniprocessor_model PState
sched: schedule PState
H1: JobCost Job
H_valid_arrivals: valid_arrival_sequence arr_seq
H2: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H3: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (GEL Job Task)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
same_task j2 j1
      -
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
H_uniproc: uniprocessor_model PState
sched: schedule PState
H1: JobCost Job
H_valid_arrivals: valid_arrival_sequence arr_seq
H2: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H3: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (GEL Job Task)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
(job_arrival j1 <= job_arrival j2) &&
~~ (job_arrival j2 <= job_arrival j1) by rewrite -ltnNge; apply/andP; split => //.
      -
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
Arrival: JobArrival Job
arr_seq: arrival_sequence Job
PState: ProcessorState Job
H_uniproc: uniprocessor_model PState
sched: schedule PState
H1: JobCost Job
H_valid_arrivals: valid_arrival_sequence arr_seq
H2: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H3: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (GEL Job Task)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: same_task j1 j2
LT: job_arrival j1 < job_arrival j2
same_task j2 j1 by rewrite same_task_sym.
    Qed.

  End SequentialTasks.

End GELBasicFacts.

(** We add the following lemma to the basic facts database. *)
Global Hint Resolve
GEL_respects_sequential_tasks
  : basic_rt_facts.