Library prosa.analysis.facts.preemption.rtc_threshold.floating


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Export prosa.analysis.facts.preemption.task.floating.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.

Furthermore, we assume the task model with floating non-preemptive regions.

Task's Run to Completion Threshold

In this section, we instantiate function [task run to completion threshold] for the model with floating 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 `{JobCost Job}.
  Context `{JobPreemptable Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Assume that a job cost cannot be larger than a task cost.
Then, we prove that [task_rtct] function defines a valid task's run to completion threshold.
  Lemma floating_preemptive_valid_task_run_to_completion_threshold:
     tsk, valid_task_run_to_completion_threshold arr_seq tsk.

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

1 subgoal (ID 947)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  H2 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  ============================
  forall tsk : Task, valid_task_run_to_completion_threshold arr_seq tsk

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


  Proof.
    intros; split.

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

2 subgoals (ID 950)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  H2 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  tsk : Task
  ============================
  task_rtc_bounded_by_cost tsk

subgoal 2 (ID 951) is:
 job_respects_task_rtc arr_seq tsk

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


    - by rewrite /task_rtc_bounded_by_cost.

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

1 subgoal (ID 951)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  H2 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  tsk : Task
  ============================
  job_respects_task_rtc arr_seq tsk

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


    - intros j ARR TSK.

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

1 subgoal (ID 962)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  H2 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  tsk : Task
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  job_rtct j <= task_rtct tsk

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


      apply leq_trans with (job_cost j); eauto 2 with basic_facts.

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

1 subgoal (ID 966)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  H2 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
  tsk : Task
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  job_cost j <= task_rtct tsk

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


        by rewrite-TSK; apply H_valid_job_cost.

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

No more subgoals.

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


  Qed.

End TaskRTCThresholdFloatingNonPreemptiveRegions.
Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.