preemptive.v

Require Export prosa.model.task.preemption.parameters.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.model.preemption.fully_preemptive.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]

(** * Preemptions in Fully Preemptive Model *)
(** In this section, we prove that instantiation of predicate
    [job_preemptable] to the fully preemptive model indeed defines
    a valid preemption model. *)
Section FullyPreemptiveModel.

  (** We assume that jobs are fully preemptive. *)
  #[local] Existing Instance fully_preemptive_job_model.

  (**  Consider any type of jobs. *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

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

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

  (** ... and any given schedule. *)
  Variable sched : schedule PState.

  (** Then, we prove that fully_preemptive_model is a valid preemption model. *)
  Lemma valid_fully_preemptive_model:
    valid_preemption_model arr_seq sched.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
valid_preemption_model arr_seq sched
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
valid_preemption_model arr_seq sched
      by intros j ARR; repeat split; intros t CONTR.
  Qed.

  (** We also prove that under the fully preemptive model
      [job_max_nonpreemptive_segment j] is equal to 0, when [job_cost
      j = 0] ... *)
  Lemma job_max_nps_is_0:
    forall j,
      job_cost j = 0 -> 
      job_max_nonpreemptive_segment j = 0.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
forall j : Job,
job_cost j = 0 -> job_max_nonpreemptive_segment j = 0
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
forall j : Job,
job_cost j = 0 -> job_max_nonpreemptive_segment j = 0
    intros.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
H1: job_cost j = 0
job_max_nonpreemptive_segment j = 0
    rewrite /job_max_nonpreemptive_segment /lengths_of_segments
            /job_preemption_points.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
H1: job_cost j = 0
max0
  (distances
     [seq ρ <- range 0 (job_cost j)
        | job_preemptable j ρ]) = 0 
      by rewrite H1; compute.
  Qed.

  (** ... or ε when [job_cost j > 0]. *)  
  Lemma job_max_nps_is_ε:
    forall j,
      job_cost j > 0 -> 
      job_max_nonpreemptive_segment j = ε.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
forall j : Job,
0 < job_cost j -> job_max_nonpreemptive_segment j = ε
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
forall j : Job,
0 < job_cost j -> job_max_nonpreemptive_segment j = ε
    intros ? POS.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
job_max_nonpreemptive_segment j = ε
    rewrite /job_max_nonpreemptive_segment /lengths_of_segments
            /job_preemption_points.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
max0
  (distances
     [seq ρ <- range 0 (job_cost j)
        | job_preemptable j ρ]) = ε
    rewrite /job_preemptable /fully_preemptive_job_model.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
max0
  (distances [seq _ <- range 0 (job_cost j) | true]) =
ε
    rewrite filter_predT.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
max0 (distances (range 0 (job_cost j))) = ε
    apply max0_of_uniform_set.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < size (distances (range 0 (job_cost j)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε
    -Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < size (distances (range 0 (job_cost j)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε rewrite /range /index_iota subn0.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < size (distances (iota 0 (job_cost j).+1))
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε
      rewrite [size _]pred_Sn -[in X in _ <= X]addn1 -size_of_seq_of_distances size_iota.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < (job_cost j).+1.-1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
1 < (job_cost j).+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε
      +Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < (job_cost j).+1.-1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
1 < (job_cost j).+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε by rewrite -pred_Sn.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
1 < (job_cost j).+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε
      +Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
1 < (job_cost j).+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε by rewrite ltnS.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε
    -Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType,
x \in distances (range 0 (job_cost j)) -> x = ε by apply distances_of_iota_ε.
  Qed.    
  
End FullyPreemptiveModel.
Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.