Add add instances of rtc_threshold

restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring Require Import job task.
+From rt.restructuring.model.preemption Require Import
+     job.parameters task.parameters rtc_threshold.valid_rtct
+     job.instance.limited task.instance.floating rtc_threshold.instance.floating.
+From rt.restructuring.analysis.basic_facts.preemption Require Import
+     job.limited task.floating rtc_threshold.job_preemptable.
+
+(** * 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. *)
+Section TaskRTCThresholdFloatingNonPreemptiveRegions.
+
+  (** 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. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (** Then, we prove that [task_run_to_completion_threshold] function
+      defines a valid task's run to completion threshold. *)   
+  Lemma floating_preemptive_valid_task_run_to_completion_threshold:
+    forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.
+  Proof.
+    intros; split.
+    - by rewrite /task_run_to_completion_threshold_le_task_cost.
+    - intros j ARR TSK.
+      apply leq_trans with (job_cost j); eauto 2 with basic_facts.
+        by rewrite-TSK; apply H_job_cost_le_task_cost.
+  Qed.
+  
+End TaskRTCThresholdFloatingNonPreemptiveRegions.
+Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.

restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring Require Import model.job model.task.
+From rt.restructuring.model.preemption Require Import
+     rtc_threshold.valid_rtct valid_schedule
+     job.parameters task.parameters
+     job.instance.limited task.instance.limited rtc_threshold.instance.limited.
+From rt.restructuring.analysis.basic_facts.preemption Require Import
+     job.limited task.limited rtc_threshold.job_preemptable.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we prove that instantiation of function [task run
+    to completion threshold] to the model with limited preemptions
+    indeed defines a valid run-to-completion threshold function. *)
+Section TaskRTCThresholdLimitedPreemptions.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskPreemptionPoints Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobPreemptionPoints 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 uniprocessor schedule of this arrival sequence ... *)
+  Variable sched : schedule (ideal.processor_state Job).
+  Hypothesis H_valid_schedule_with_limited_preemptions:
+    valid_schedule_with_limited_preemptions arr_seq 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.
+
+  (** Consider an arbitrary task set ts. *)
+  Variable ts : seq Task.
+  
+  (** Assume that a job cost cannot be larger than a task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (** Consider the model with fixed preemption points. I.e., each task
+      is divided into a number of non-preemptive segments by inserting
+      statically predefined preemption points. *)
+  Hypothesis H_valid_fixed_preemption_points_model:
+    valid_fixed_preemption_points_model arr_seq ts.
+
+  (** And consider any task from task set ts with positive cost. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts. 
+  Hypothesis H_positive_cost : 0 < task_cost tsk.
+
+  (** We start by proving an auxiliary lemma. Note that since [tsk]
+      has a positive cost, [task_preemption_points tsk] contains [0]
+      and [task_cost tsk]. Thus, [2 <= size (task_preemption_points tsk)]. *)
+  Remark number_of_preemption_points_in_task_at_least_two: 2 <= size (task_preemption_points tsk).
+  Proof.
+    move: (H_valid_fixed_preemption_points_model) => [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
+    have Fact2: 0 < size (task_preemption_points tsk).
+    { apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
+      move: (END _ H_tsk_in_ts) => EQ.
+      move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
+        by intros; move: (H_positive_cost); rewrite EQ ltnn. 
+    } 
+    have EQ: 2 = size [::0; task_cost tsk]; first by done. 
+    rewrite EQ; clear EQ.
+    apply subseq_leq_size.
+    rewrite !cons_uniq.
+    { apply/andP; split.
+      rewrite in_cons negb_or; apply/andP; split; last by done.
+      rewrite neq_ltn; apply/orP; left; eauto 2.
+      apply/andP; split; by done. } 
+    intros t EQ; move: EQ; rewrite !in_cons.
+    move => /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
+    { rewrite EQ; clear EQ.
+      move: (BEG _ H_tsk_in_ts) => EQ.
+      rewrite -EQ; clear EQ.
+      rewrite /first0 -nth0. 
+      apply/(nthP 0).
+      exists 0; by done.
+    }
+    { rewrite EQ; clear EQ.
+      move: (END _ H_tsk_in_ts) => EQ.
+      rewrite -EQ; clear EQ.
+      rewrite /last0 -nth_last.
+      apply/(nthP 0).
+      exists ((size (task_preemption_points tsk)).-1); last by done. 
+        by rewrite -(leq_add2r 1) !addn1 prednK //.
+    }
+  Qed.
+    
+  (** Then, we prove that [task_run_to_completion_threshold] function
+      defines a valid task's run to completion threshold. *)   
+  Lemma limited_valid_task_run_to_completion_threshold:
+    valid_task_run_to_completion_threshold arr_seq tsk.
+  Proof.
+    split; first by rewrite /task_run_to_completion_threshold_le_task_cost leq_subr.
+    intros ? ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) => [LJ LT].
+    move: (LJ) (LT) => [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
+    rewrite /job_run_to_completion_threshold /task_run_to_completion_threshold /limited_preemptions
+            /job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
+    case: (posnP (job_cost j)) => [Z|POS]; first by rewrite Z; compute.
+    have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
+      by eapply job_last_nonpreemptive_segment_positive; eauto using valid_fixed_preemption_points_model_lemma.
+    have T_RTCT__pos : 0 < task_last_nonpr_segment tsk.
+    { unfold lengths_of_task_segments_bound_length_of_job_segments, task_last_nonpr_segment in *.
+      rewrite last0_nth; apply T6; eauto 2.
+      have F: 1 <= size (distances (task_preemption_points tsk)).
+      { apply leq_trans with (size (task_preemption_points tsk) - 1). 
+        - have F := number_of_preemption_points_in_task_at_least_two; ssromega.
+        - rewrite [in X in X - 1]size_of_seq_of_distances; [ssromega | apply number_of_preemption_points_in_task_at_least_two].
+      } ssromega.
+    }    
+    have J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
+      by eapply job_last_nonpreemptive_segment_le_job_cost; eauto using valid_fixed_preemption_points_model_lemma.
+    have T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk.
+    { unfold task_last_nonpr_segment. rewrite -COST__task //.
+      eapply leq_trans; last by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
+        by apply last_of_seq_le_max_of_seq.
+    } 
+    rewrite subnBA // subnBA // -addnBAC // -addnBAC // !addn1 ltnS.
+    erewrite job_parameters_last_np_to_job_limited; eauto 2.
+    rewrite distances_positive_undup //; last by apply SORT__job. 
+    have -> : job_cost j = last0 (undup (job_preemption_points j)) by rewrite last0_undup; [rewrite -COST__job | apply SORT__job].
+    rewrite last_seq_minus_last_distance_seq; last by apply nondecreasing_sequence_undup, SORT__job. 
+    apply leq_trans with( nth 0 (job_preemption_points j) ((size (job_preemption_points j)).-2)); first by apply undup_nth_le; eauto 2.
+    have -> : task_cost tsk = last0 (task_preemption_points tsk) by rewrite COST__task. 
+    rewrite last_seq_minus_last_distance_seq; last by apply SORT__task.
+    rewrite -TSK__j.
+    rewrite T4; last by done.
+    apply domination_of_distances_implies_domination_of_seq; try eauto 2.
+    - erewrite zero_is_first_element; eauto.
+    - eapply number_of_preemption_points_at_least_two; eauto 2. 
+    - by rewrite TSK__j; eapply number_of_preemption_points_in_task_at_least_two.  
+    - by apply SORT__task; rewrite TSK__j.
+  Qed.
+  
+End TaskRTCThresholdLimitedPreemptions.
+Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.

restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v

+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:
+    forall j,
+      job_cost j = 0 -> 
+      job_run_to_completion_threshold j = 0.
+  Proof.
+    intros.
+    apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
+    unfold job_run_to_completion_threshold.
+      by rewrite H3; compute.
+  Qed.
+  
+  (** ... and ε otherwise. *)
+  Fact job_rtc_threshold_is_ε:
+    forall j,
+      job_cost j > 0 ->
+      arrives_in arr_seq j ->
+      job_run_to_completion_threshold j = ε.
+  Proof.
+    intros ? ARRj POSj; unfold ε in *.
+    unfold job_run_to_completion_threshold.
+    rewrite job_last_nps_is_job_cost.
+      by rewrite subKn.
+  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.
+  Proof.
+    intros; split.
+    - by unfold task_run_to_completion_threshold_le_task_cost.
+    - intros j ARR TSK.
+      rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.
+      edestruct (posnP (job_cost j)) as [ZERO|POS].
+      + by rewrite job_rtc_threshold_is_0.
+      + by erewrite job_rtc_threshold_is_ε; eauto 2. 
+  Qed.
+    
+End TaskRTCThresholdFullyNonPreemptive.
+Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.

restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring.model Require Import job task.
+From rt.restructuring.model.preemption Require Import rtc_threshold.valid_rtct
+     job.instance.preemptive task.instance.preemptive rtc_threshold.instance.preemptive.
+From rt.restructuring.analysis.basic_facts.preemption Require Import 
+     rtc_threshold.job_preemptable.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we prove that instantiation of function [task run
+    to completion threshold] to the fully preemptive model
+    indeed defines a valid run-to-completion threshold function. *)
+Section TaskRTCThresholdFullyPreemptiveModel.
+
+  (** 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}.
+  
+  (** Next, consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and assume that a job cost cannot be larger than a task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (** Then, we prove that [task_run_to_completion_threshold] function
+      defines a valid task's run to completion threshold. *)     
+  Lemma fully_preemptive_valid_task_run_to_completion_threshold:
+    forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.
+  Proof.
+    intros; split.
+    - by rewrite /task_run_to_completion_threshold_le_task_cost.
+    - intros j ARR TSK.
+      apply leq_trans with (job_cost j); eauto 2 with basic_facts.
+        by rewrite-TSK; apply H_job_cost_le_task_cost.
+  Qed.
+    
+End TaskRTCThresholdFullyPreemptiveModel.
+Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_facts.

restructuring/model/preemption/rtc_threshold/instance/floating.v

+From rt.util Require Export all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring Require Import model.job model.task.
+From rt.restructuring.model.preemption Require Import task.parameters.
+
+(** * 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. *)
+Section TaskRTCThresholdFloatingNonPreemptiveRegions.
+
+  (** Consider any type of tasks.*)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  
+  (** In the model with floating non-preemptive regions, task has to
+      static information about the placement of preemption
+      points. Thus, the only safe task's run to completion threshold
+      is [task cost]. *)
+  Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
+    { 
+      task_run_to_completion_threshold (tsk : Task) := task_cost tsk
+    }.
+
+End TaskRTCThresholdFloatingNonPreemptiveRegions.

restructuring/model/preemption/rtc_threshold/instance/limited.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring Require Import model.job model.task.
+From rt.restructuring.model.preemption Require Import task.parameters.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+    threshold] for the limited preemptions model. *)
+Section TaskRTCThresholdLimitedPreemptions.
+  
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskPreemptionPoints Task}.
+    
+  (** In the model with limited preemptions, no job can be preempted after
+      a job reaches its last non-preemptive segment. Thus, we can
+      set task's run to completion threshold to [task_cost tsk -
+      (task_last_nonpr_seg tsk - ε)] which is always greater than
+      [job_cost j - (job_last_nonpr_seg j - ε)]. *)
+  Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
+    { 
+      task_run_to_completion_threshold (tsk : Task) :=
+        task_cost tsk - (task_last_nonpr_segment tsk - ε)
+    }.
+  
+End TaskRTCThresholdLimitedPreemptions.

restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring Require Import model.job model.task.
+From rt.restructuring.model.preemption Require Import task.parameters.
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+    threshold] for the fully non-preemptive model. *)
+Section TaskRTCThresholdFullyNonPreemptive.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}. 
+  Context `{TaskCost Task}.
+    
+  (** In fully non-preemptive model no job can be preempted until its
+      completion. Thus, we can set task's run to completion threshold
+      to ε. *)
+  Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
+    { 
+      task_run_to_completion_threshold (tsk : Task) := ε
+    }.
+
+End TaskRTCThresholdFullyNonPreemptive.

restructuring/model/preemption/rtc_threshold/instance/preemptive.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring Require Import model.job model.task.
+From rt.restructuring.model.preemption Require Import task.parameters.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+   threshold] for the fully preemptive model. *)
+Section TaskRTCThresholdFullyPreemptiveModel.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (** In the fully preemptive model any job can be preempted at any time. Thus, 
+       the only safe task's run to completion threshold is [task cost]. *)
+  Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
+    { 
+      task_run_to_completion_threshold (tsk : Task) := task_cost tsk
+    }.
+    
+End TaskRTCThresholdFullyPreemptiveModel.