sequential.v

Require Export prosa.analysis.facts.behavior.all.[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.model.task.sequentiality.
Require Export prosa.analysis.definitions.readiness.
Require Export prosa.analysis.facts.model.task_arrivals.

Section ExecutionOrder.

  (** Consider any type of job associated with any type of tasks... *)
  Context {Job: JobType}.
  Context {Task: TaskType}.
  Context `{JobTask Job Task}.

  (** ... with arrival times and costs ... *)
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

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

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

  (** ... and any schedule of this arrival sequence ... *)
  Variable sched : schedule PState.

  (** ... in which the sequential tasks hypothesis holds. *)
  Hypothesis H_sequential_tasks: sequential_tasks arr_seq sched.

  (** A simple corollary of this hypothesis is that the scheduler
      executes a job with the earliest arrival time. *)
  Corollary scheduler_executes_job_with_earliest_arrival:
    forall j1 j2 t,
      arrives_in arr_seq j1 ->
      arrives_in arr_seq j2 ->
      same_task j1 j2 ->
      ~~ completed_by sched j2 t ->
      scheduled_at sched j1 t ->
      job_arrival j1 <= job_arrival j2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
forall (j1 j2 : Job) (t : instant),
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
same_task j1 j2 ->
~~ completed_by sched j2 t ->
scheduled_at sched j1 t ->
job_arrival j1 <= job_arrival j2
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
forall (j1 j2 : Job) (t : instant),
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
same_task j1 j2 ->
~~ completed_by sched j2 t ->
scheduled_at sched j1 t ->
job_arrival j1 <= job_arrival j2
    move=> j1 j2 t ARR1 ARR2 TSK NCOMPL SCHED.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
TSK: same_task j1 j2
NCOMPL: ~~ completed_by sched j2 t
SCHED: scheduled_at sched j1 t
job_arrival j1 <= job_arrival j2
    have {}TSK := eqbLR (same_task_sym _ _) TSK.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
NCOMPL: ~~ completed_by sched j2 t
SCHED: scheduled_at sched j1 t
TSK: same_task j2 j1
job_arrival j1 <= job_arrival j2
    have SEQ := H_sequential_tasks j2 j1 t ARR2 ARR1 TSK.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
NCOMPL: ~~ completed_by sched j2 t
SCHED: scheduled_at sched j1 t
TSK: same_task j2 j1
SEQ: job_arrival j2 < job_arrival j1 ->
scheduled_at sched j1 t ->
completed_by sched j2 t
job_arrival j1 <= job_arrival j2
    rewrite leqNgt; apply/negP => ARR.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
NCOMPL: ~~ completed_by sched j2 t
SCHED: scheduled_at sched j1 t
TSK: same_task j2 j1
SEQ: job_arrival j2 < job_arrival j1 ->
scheduled_at sched j1 t ->
completed_by sched j2 t
ARR: job_arrival j2 < job_arrival j1
False
    exact/(negP NCOMPL)/SEQ.
  Qed.

  (** Likewise, if we see an earlier-arrived incomplete job [j1] while another
      job [j2] is scheduled, then [j1] and [j2] must stem from different
      tasks. *)
  Corollary sequential_tasks_different_tasks :
    forall j1 j2 t,
      arrives_in arr_seq j1 ->
      arrives_in arr_seq j2 ->
      job_arrival j1 < job_arrival j2 ->
      ~~ completed_by sched j1 t ->
      scheduled_at sched j2 t ->
      ~~ same_task j1 j2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
forall (j1 j2 : Job) (t : instant),
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
~~ completed_by sched j1 t ->
scheduled_at sched j2 t -> ~~ same_task j1 j2
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
forall (j1 j2 : Job) (t : instant),
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
~~ completed_by sched j1 t ->
scheduled_at sched j2 t -> ~~ same_task j1 j2
    move=> j1 j2 t IN1 IN2 LT_ARR INCOMP SCHED.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
IN1: arrives_in arr_seq j1
IN2: arrives_in arr_seq j2
LT_ARR: job_arrival j1 < job_arrival j2
INCOMP: ~~ completed_by sched j1 t
SCHED: scheduled_at sched j2 t
~~ same_task j1 j2
    apply: contraL INCOMP => SAME.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
IN1: arrives_in arr_seq j1
IN2: arrives_in arr_seq j2
LT_ARR: job_arrival j1 < job_arrival j2
SCHED: scheduled_at sched j2 t
SAME: same_task j1 j2
~~ ~~ completed_by sched j1 t
    by apply/negPn/H_sequential_tasks; eauto.
  Qed.

End ExecutionOrder.


(** In the following section, we connect [sequential_readiness] with
    [sequential_tasks], showing that the latter follows from the former. *)
Section FromSequentialReadiness.

  (** Consider any type of job associated with any type of tasks ... *)
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

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

  (** ... and any arrival sequence with consistent arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

  (** If we have a sequential readiness model, ... *)
  Context {JR : JobReady Job PState}.
  Hypothesis H_sequential : sequential_readiness JR arr_seq.

  (** ... then in any valid schedule of the arrival sequence ... *)
  Variable sched : schedule PState.
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

  (** ... all tasks execute sequentially. *)
  Lemma sequential_tasks_from_readiness :
    sequential_tasks arr_seq sched.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
JR: JobReady Job PState
H_sequential: sequential_readiness JR arr_seq
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
sequential_tasks arr_seq sched
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
JR: JobReady Job PState
H_sequential: sequential_readiness JR arr_seq
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
sequential_tasks arr_seq sched
    move=> j j' t IN IN' SAME LT_ARR SCHED'.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
JR: JobReady Job PState
H_sequential: sequential_readiness JR arr_seq
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
j, j': Job
t: instant
IN: arrives_in arr_seq j
IN': arrives_in arr_seq j'
SAME: same_task j j'
LT_ARR: job_arrival j < job_arrival j'
SCHED': scheduled_at sched j' t
completed_by sched j t
    have /allP COMP: prior_jobs_complete arr_seq sched j' t by apply: H_sequential.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
JR: JobReady Job PState
H_sequential: sequential_readiness JR arr_seq
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
j, j': Job
t: instant
IN: arrives_in arr_seq j
IN': arrives_in arr_seq j'
SAME: same_task j j'
LT_ARR: job_arrival j < job_arrival j'
SCHED': scheduled_at sched j' t
COMP: {in task_arrivals_before arr_seq 
      (job_task j') 
      (job_arrival j'),
  forall x : Job, completed_by sched x t}
completed_by sched j t
    apply/COMP/job_in_task_arrivals_between => //.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
JR: JobReady Job PState
H_sequential: sequential_readiness JR arr_seq
sched: schedule PState
H_valid_schedule: valid_schedule sched arr_seq
j, j': Job
t: instant
IN: arrives_in arr_seq j
IN': arrives_in arr_seq j'
SAME: same_task j j'
LT_ARR: job_arrival j < job_arrival j'
SCHED': scheduled_at sched j' t
COMP: {in task_arrivals_before arr_seq 
      (job_task j') 
      (job_arrival j'),
  forall x : Job, completed_by sched x t}
job_task j = job_task j'
    by move: SAME => /eqP.
  Qed.

End FromSequentialReadiness.