Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive


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

Welcome to Coq 8.10.1 (October 2019)

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

From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model Require Import job task schedule.nonpreemptive.
From rt.restructuring.model.preemption Require Import
     valid_model job.parameters task.parameters rtc_threshold.valid_rtct
     job.instance.nonpreemptive task.instance.nonpreemptive rtc_threshold.instance.nonpreemptive.
From rt.restructuring.analysis.basic_facts.preemption Require Import job.nonpreemptive.

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Task's Run to Completion Threshold

In this section, we prove that instantiation of function [task run to completion threshold] to the fully non-preemptive model indeed defines a valid run-to-completion threshold function.
Section TaskRTCThresholdFullyNonPreemptive.

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 arrival sequence with consistent arrivals.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Next, consider any ideal non-preemptive uniprocessor schedule of this arrival sequence ...
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched.

... where jobs do not execute before their arrival or after completion.
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

First we prove that if the cost of a job j is equal to 0, then [job_run_to_completion_threshold j = 0] ...
  Fact job_rtc_threshold_is_0:
    ∀ j,
      job_cost j = 0 →
      job_run_to_completion_threshold j = 0.

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

1 subgoal (ID 195)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ============================
  forall j : Job, job_cost j = 0 -> job_run_to_completion_threshold j = 0

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

  Proof.
    intros.

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

1 subgoal (ID 197)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  j : Job
  H3 : job_cost j = 0
  ============================
  job_run_to_completion_threshold j = 0

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

    apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.

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

1 subgoal (ID 282)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  j : Job
  H3 : job_cost j = 0
  ============================
  job_run_to_completion_threshold j <= 0

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

    unfold job_run_to_completion_threshold.

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

1 subgoal (ID 285)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  j : Job
  H3 : job_cost j = 0
  ============================
  job_cost j - (job_last_nonpreemptive_segment j - ε) <= 0

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

      by rewrite H3; compute.

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

No more subgoals.

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

  Qed.

... and ε otherwise.
  Fact job_rtc_threshold_is_ε:
    ∀ j,
      job_cost j > 0 →
      arrives_in arr_seq j →
      job_run_to_completion_threshold j = ε.

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

1 subgoal (ID 207)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  ============================
  forall j : Job,
  0 < job_cost j ->
  arrives_in arr_seq j -> job_run_to_completion_threshold j = ε

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

  Proof.
    intros ? ARRj POSj; unfold ε in ×.

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

1 subgoal (ID 212)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  j : Job
  ARRj : 0 < job_cost j
  POSj : arrives_in arr_seq j
  ============================
  job_run_to_completion_threshold j = 1

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

    unfold job_run_to_completion_threshold.

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

1 subgoal (ID 214)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  j : Job
  ARRj : 0 < job_cost j
  POSj : arrives_in arr_seq j
  ============================
  job_cost j - (job_last_nonpreemptive_segment j - ε) = 1

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

    rewrite job_last_nps_is_job_cost.

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

1 subgoal (ID 221)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  j : Job
  ARRj : 0 < job_cost j
  POSj : arrives_in arr_seq j
  ============================
  job_cost j - (job_cost j - ε) = 1

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

      by rewrite subKn.

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

No more subgoals.

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

  Qed.

Consider a task with a positive cost.
  Variable tsk : Task.
  Hypothesis H_positive_cost : 0 < task_cost tsk.

Then, we prove that [task_run_to_completion_threshold] function defines a valid task's run to completion threshold.
  Lemma fully_nonpreemptive_valid_task_run_to_completion_threshold:
    valid_task_run_to_completion_threshold arr_seq tsk.

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

1 subgoal (ID 218)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  tsk : Task
  H_positive_cost : 0 < task_cost tsk
  ============================
  valid_task_run_to_completion_threshold arr_seq tsk

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

  Proof.
    intros; split.

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

2 subgoals (ID 220)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  tsk : Task
  H_positive_cost : 0 < task_cost tsk
  ============================
  task_run_to_completion_threshold_le_task_cost tsk

subgoal 2 (ID 221) is:
 task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
   arr_seq tsk

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

    - by unfold task_run_to_completion_threshold_le_task_cost.

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

1 subgoal (ID 221)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  tsk : Task
  H_positive_cost : 0 < task_cost tsk
  ============================
  task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
    arr_seq tsk

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

    - intros j ARR TSK.

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

1 subgoal (ID 227)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  tsk : Task
  H_positive_cost : 0 < task_cost tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk

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

      rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.

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

1 subgoal (ID 237)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  tsk : Task
  H_positive_cost : 0 < task_cost tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  job_run_to_completion_threshold j <= ε

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

      edestruct (posnP (job_cost j)) as [ZERO|POS].

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

2 subgoals (ID 262)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  tsk : Task
  H_positive_cost : 0 < task_cost tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ZERO : job_cost j = 0
  ============================
  job_run_to_completion_threshold j <= ε

subgoal 2 (ID 263) is:
 job_run_to_completion_threshold j <= ε

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

      + by rewrite job_rtc_threshold_is_0.

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

1 subgoal (ID 263)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : is_nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  tsk : Task
  H_positive_cost : 0 < task_cost tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  POS : 0 < job_cost j
  ============================
  job_run_to_completion_threshold j <= ε

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

      + by erewrite job_rtc_threshold_is_ε; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

  Qed.

End TaskRTCThresholdFullyNonPreemptive.
Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.