gel.v

Require Import prosa.model.priority.gel.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 Import prosa.model.processor.ideal.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 Import prosa.model.schedule.priority_driven.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 Import prosa.model.task.sequentiality.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 Import prosa.analysis.facts.priority.sequential.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]

(** 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}.
  Context `{JobArrival Job}.

  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 :
      (Z.of_nat (job_arrival j') <=
         Z.of_nat (job_arrival j) +
           task_priority_point (job_task j) - task_priority_point (job_task j'))%Z.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
(Z.of_nat (job_arrival j') <=
 Z.of_nat (job_arrival j) +
 task_priority_point (job_task j) -
 task_priority_point (job_task j'))%Z
    Proof.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
(Z.of_nat (job_arrival j') <=
 Z.of_nat (job_arrival j) +
 task_priority_point (job_task j) -
 task_priority_point (job_task j'))%Z
      by move : H_j'_hep; rewrite /hep_job /GEL /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. Note that
        the function [Z.of_nat] is used to convert natural numbers
        to integers. *)
    Corollary hep_job_arrives_after_zero :
      (0 <= Z.of_nat (job_arrival j) +
             task_priority_point (job_task j) - task_priority_point (job_task j'))%Z.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
(0 <=
 Z.of_nat (job_arrival j) +
 task_priority_point (job_task j) -
 task_priority_point (job_task j'))%Z
    Proof.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
(0 <=
 Z.of_nat (job_arrival j) +
 task_priority_point (job_task j) -
 task_priority_point (job_task j'))%Z
      apply: (@Z.le_trans _ (Z.of_nat (job_arrival j'))); first by lia.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
j, j': Job
H_j'_hep: hep_job j' j
(Z.of_nat (job_arrival j') <=
 Z.of_nat (job_arrival j) +
 task_priority_point (job_task j) -
 task_priority_point (job_task j'))%Z
      by apply: 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.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
policy_respects_sequential_tasks
  Proof.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
policy_respects_sequential_tasks
    move =>  j1 j2 /eqP TSK ARR.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
j1, j2: Job
TSK: job_task j1 = job_task j2
ARR: job_arrival j1 <= job_arrival j2
hep_job j1 j2
    rewrite /hep_job /GEL /job_priority_point TSK.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
j1, j2: Job
TSK: job_task j1 = job_task j2
ARR: job_arrival j1 <= job_arrival j2
(Z.of_nat (job_arrival j1) +
 task_priority_point (job_task j2) <=?
 Z.of_nat (job_arrival j2) +
 task_priority_point (job_task j2))%Z
    by lia.
  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.

    (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
    Variable sched : schedule (ideal.processor_state Job).

    Context `{JobArrival Job} `{JobCost Job}.
    (** ... allow for any work-bearing notion of job readiness, ... *)
    Context `{@JobReady Job (ideal.processor_state Job) _ _}.
    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
H1: JobArrival Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
H2: JobArrival Job
H3: JobCost Job
H4: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H5: 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
H1: JobArrival Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
H2: JobArrival Job
H3: JobCost Job
H4: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H5: 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 /eqP SAME LT.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
H2: JobArrival Job
H3: JobCost Job
H4: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H5: 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: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
scheduled_at sched j2 t -> completed_by sched j1 t
      eapply early_hep_job_is_scheduled => //; rt_eauto => t'.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
H2: JobArrival Job
H3: JobCost Job
H4: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H5: 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: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
t': instant
hep_job_at t' j1 j2 && ~~ hep_job_at t' j2 j1
      rewrite /hep_job_at  /JLFP_to_JLDP /hep_job /GEL /job_priority_point SAME.Task: TaskType
Job: JobType
H: JobTask Job Task
H0: PriorityPoint Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
H2: JobArrival Job
H3: JobCost Job
H4: JobReady Job (processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H5: 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: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
t': instant
(Z.of_nat (job_arrival j1) +
 task_priority_point (job_task j2) <=?
 Z.of_nat (job_arrival j2) +
 task_priority_point (job_task j2))%Z &&
~~
(Z.of_nat (job_arrival j2) +
 task_priority_point (job_task j2) <=?
 Z.of_nat (job_arrival j1) +
 task_priority_point (job_task j2))%Z
      by lia.
    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.