From 4b53a2df0c070d65210b0c8a98cde1d059fbf906 Mon Sep 17 00:00:00 2001 From: Sergei Bozhko Date: Wed, 23 Oct 2019 15:07:37 +0200 Subject: [PATCH] Add add instances of rtc_threshold --- .../preemption/rtc_threshold/floating.v | 45 ++++++ .../preemption/rtc_threshold/limited.v | 146 ++++++++++++++++++ .../preemption/rtc_threshold/nonpreemptive.v | 85 ++++++++++ .../preemption/rtc_threshold/preemptive.v | 44 ++++++ .../rtc_threshold/instance/floating.v | 24 +++ .../rtc_threshold/instance/limited.v | 27 ++++ .../rtc_threshold/instance/nonpreemptive.v | 25 +++ .../rtc_threshold/instance/preemptive.v | 22 +++ 8 files changed, 418 insertions(+) create mode 100644 restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v create mode 100644 restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v create mode 100644 restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v create mode 100644 restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v create mode 100644 restructuring/model/preemption/rtc_threshold/instance/floating.v create mode 100644 restructuring/model/preemption/rtc_threshold/instance/limited.v create mode 100644 restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v create mode 100644 restructuring/model/preemption/rtc_threshold/instance/preemptive.v diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v new file mode 100644 index 0000000..cf3a4ca --- /dev/null +++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v @@ -0,0 +1,45 @@ +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. diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v new file mode 100644 index 0000000..18291e8 --- /dev/null +++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v @@ -0,0 +1,146 @@ +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. diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v new file mode 100644 index 0000000..14bc347 --- /dev/null +++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v @@ -0,0 +1,85 @@ +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. diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v new file mode 100644 index 0000000..2c03df2 --- /dev/null +++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v @@ -0,0 +1,44 @@ +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. diff --git a/restructuring/model/preemption/rtc_threshold/instance/floating.v b/restructuring/model/preemption/rtc_threshold/instance/floating.v new file mode 100644 index 0000000..6a171b9 --- /dev/null +++ b/restructuring/model/preemption/rtc_threshold/instance/floating.v @@ -0,0 +1,24 @@ +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. diff --git a/restructuring/model/preemption/rtc_threshold/instance/limited.v b/restructuring/model/preemption/rtc_threshold/instance/limited.v new file mode 100644 index 0000000..0d43a8c --- /dev/null +++ b/restructuring/model/preemption/rtc_threshold/instance/limited.v @@ -0,0 +1,27 @@ +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. diff --git a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v b/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v new file mode 100644 index 0000000..5a9a722 --- /dev/null +++ b/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v @@ -0,0 +1,25 @@ +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. diff --git a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v b/restructuring/model/preemption/rtc_threshold/instance/preemptive.v new file mode 100644 index 0000000..adaf096 --- /dev/null +++ b/restructuring/model/preemption/rtc_threshold/instance/preemptive.v @@ -0,0 +1,22 @@ +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. -- GitLab