Library prosa.analysis.facts.preemption.task.preemptive


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.preemption.job.preemptive.

Furthermore, we assume the fully non-preemptive task model.

Platform for Fully Preemptive Model

In this section, we prove that instantiation of functions [job_preemptable and task_max_nonpreemptive_segment] to the fully preemptive model indeed defines a valid preemption model with bounded non-preemptive regions.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any kind of processor state model, ...
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

... any job arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any given schedule.
  Variable sched : schedule PState.

We prove that [fully_preemptive_model] function defines a model with bounded non-preemptive regions.
  Lemma fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions:
    model_with_bounded_nonpreemptive_segments arr_seq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 634)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  ============================
  model_with_bounded_nonpreemptive_segments arr_seq

----------------------------------------------------------------------------- *)


  Proof.
    intros j ARR; split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 639)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  job_respects_max_nonpreemptive_segment j

subgoal 2 (ID 640) is:
 nonpreemptive_regions_have_bounded_length j

----------------------------------------------------------------------------- *)


    - case: (posnP (job_cost j)) ⇒ [ZERO|POS].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 663)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  ARR : arrives_in arr_seq j
  ZERO : job_cost j = 0
  ============================
  job_respects_max_nonpreemptive_segment j

subgoal 2 (ID 664) is:
 job_respects_max_nonpreemptive_segment j
subgoal 3 (ID 640) is:
 nonpreemptive_regions_have_bounded_length j

----------------------------------------------------------------------------- *)


      + by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_0.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 664)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  ARR : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  job_respects_max_nonpreemptive_segment j

subgoal 2 (ID 640) is:
 nonpreemptive_regions_have_bounded_length j

----------------------------------------------------------------------------- *)


      + by rewrite /job_respects_max_nonpreemptive_segment job_max_nps_is_ε.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 640)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  nonpreemptive_regions_have_bounded_length j

----------------------------------------------------------------------------- *)


    - intros t; t; split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 715)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  ARR : arrives_in arr_seq j
  t : duration
  H4 : 0 <= t <= job_cost j
  ============================
  t <= t <= t + (job_max_nonpreemptive_segment j - ε)

subgoal 2 (ID 716) is:
 job_preemptable j t

----------------------------------------------------------------------------- *)


      + by apply/andP; split; [ done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 716)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  ARR : arrives_in arr_seq j
  t : duration
  H4 : 0 <= t <= job_cost j
  ============================
  job_preemptable j t

----------------------------------------------------------------------------- *)


      + by done.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

Which together with lemma [valid_fully_preemptive_model] gives us the fact that [fully_preemptive_model] defined a valid preemption model with bounded non-preemptive regions.
  Corollary fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments:
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 643)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  ============================
  valid_model_with_bounded_nonpreemptive_segments arr_seq sched

----------------------------------------------------------------------------- *)


  Proof.
    split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 645)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  ============================
  valid_preemption_model arr_seq sched

subgoal 2 (ID 646) is:
 model_with_bounded_nonpreemptive_segments arr_seq

----------------------------------------------------------------------------- *)


    apply valid_fully_preemptive_model.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 646)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  PState : Type
  H3 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  ============================
  model_with_bounded_nonpreemptive_segments arr_seq

----------------------------------------------------------------------------- *)


    apply fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End FullyPreemptiveModel.

We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Hint Resolve
     valid_fully_preemptive_model
     fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions
     fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_facts.