diff --git a/analysis/facts/priority/fifo.v b/analysis/facts/priority/fifo.v index 90c92de7194b1f6ab9f5e06cd1e5b4aa7d9b4bec..632ac5d59bbf7525266131831455d60b2e9b78b6 100644 --- a/analysis/facts/priority/fifo.v +++ b/analysis/facts/priority/fifo.v @@ -7,6 +7,7 @@ Require Export prosa.analysis.definitions.priority_inversion. Require Export prosa.analysis.facts.priority.sequential. Require Export prosa.analysis.facts.readiness.basic. Require Export prosa.analysis.facts.preemption.job.nonpreemptive. +Require Export prosa.analysis.abstract.ideal_jlfp_rta. (** In this section, we prove some fundamental properties of the FIFO policy. *) Section BasicLemmas. @@ -29,11 +30,11 @@ Section BasicLemmas. (** Suppose jobs have preemption points ... *) Context `{JobPreemptable Job}. - + (** ...and that the preemption model is valid. *) Hypothesis H_valid_preemption_model : - valid_preemption_model arr_seq sched. - + valid_preemption_model arr_seq sched. + (** Assume that the schedule respects the FIFO scheduling policy whenever jobs are preemptable. *) Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job). @@ -51,7 +52,60 @@ Section BasicLemmas. apply: NCOMPL; eapply early_hep_job_is_scheduled; rt_eauto. by intros t'; apply/andP; split; unfold hep_job_at, JLFP_to_JLDP, hep_job, FIFO; lia. Qed. - + + (** In this section, we prove the cumulative priority inversion for any task + is bounded by [0]. *) + Section PriorityInversionBounded. + + (** Consider any kind of tasks. *) + Context `{Task : TaskType} `{JobTask Job Task}. + + (** Consider a task [tsk]. *) + Variable tsk : Task. + + (** Assume the arrival times are consistent. *) + Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq. + + (** Assume that the schedule follows the FIFO policy at preemption time. *) + Hypothesis H_respects_policy_at_preemption_point : + respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job). + + (** Assume the schedule is valid. *) + Hypothesis H_valid_schedule : valid_schedule sched arr_seq. + + (** Assume there are no duplicates in the arrival sequence. *) + Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq. + + (** Then we prove that the amount of priority inversion is bounded by 0. *) + Lemma FIFO_implies_no_pi : + priority_inversion_is_bounded_by_constant arr_seq sched tsk 0. + Proof. + move=> j ARRIN TASK POS t1 t2 BUSY. + rewrite /priority_inversion.cumulative_priority_inversion. + have -> : \sum_(t1 <= t < t2) priority_inversion_dec arr_seq sched j t = 0; + last by done. + rewrite big_nat_eq0 => t /andP[T1 T2]. + apply /eqP; rewrite eqb0. + apply /negP => /priority_inversion_P INV. + feed_n 3 INV; rt_eauto. + move: INV => [NSCHED [j__lp /andP [SCHED LP]]]. + move: LP; rewrite /hep_job /FIFO -ltnNge => LT. + have COMPL: completed_by sched j t. + { apply: early_hep_job_is_scheduled; rt_eauto. + move=> t'; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FIFO -ltnNge. + by apply/andP; split; first apply ltnW. } + move : BUSY => [LE [QT [NQT /andP[ARR1 ARR2]]]]. + move: T1; rewrite leq_eqVlt => /orP [/eqP EQ | GT]. + { subst t; apply completed_implies_scheduled_before in COMPL; rt_eauto. + by case: COMPL => [t' [/andP [ARR3 LT__temp] SCHED__temp]]; lia. } + { apply: NQT; first (apply/andP; split; [exact GT | lia]). + intros ? ARR HEP ARRB; rewrite /hep_job /FIFO in HEP. + eapply early_hep_job_is_scheduled; rt_eauto; first by lia. + by move => t'; apply/andP; split; rewrite /hep_job_at /FIFO /JLFP_to_JLDP /hep_job //=; lia. } + Qed. + + End PriorityInversionBounded. + (** We prove that in a FIFO-compliant schedule, if a job [j] is scheduled, then all jobs with higher priority than [j] have been completed. *) @@ -87,6 +141,10 @@ Section BasicLemmas. by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. Qed. + (** We also note that the [FIFO] policy respects sequential tasks. *) + Fact fifo_respects_sequential_tasks : policy_respects_sequential_tasks. + Proof. by move => j1 j2 SAME ARRLE; rewrite /hep_job /FIFO. Qed. + End SequentialTasks. (** Finally, let us further assume that there are no needless @@ -121,7 +179,7 @@ Section BasicLemmas. apply H_no_superfluous_preemptions; last by done. by repeat (apply /andP ; split; try by done). } - rewrite /hep_job /fifo.FIFO -ltnNge in HEP. + rewrite /hep_job /fifo.FIFO -ltnNge in HEP. eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try rt_eauto. - apply scheduled_implies_not_completed in INTER; rt_eauto. by eapply (incompletion_monotonic sched s t.-1 t) in INTER; [move: INTER => /negP|lia]. @@ -136,3 +194,9 @@ Section BasicLemmas. Qed. End BasicLemmas. + +(** We add the following lemmas to the basic facts database *) +Global Hint Resolve + fifo_respects_sequential_tasks + tasks_execute_sequentially + : basic_rt_facts. diff --git a/results/fifo/rta.v b/results/fifo/rta.v index f0f2a37438022e75ce671ba3c95d155c5655c063..0dce3c2bd43629e6c56898322ba52c91fe9d3e1b 100644 --- a/results/fifo/rta.v +++ b/results/fifo/rta.v @@ -5,6 +5,7 @@ Require Import prosa.model.priority.fifo. Require Import prosa.analysis.facts.priority.fifo. Require Import prosa.analysis.abstract.ideal_jlfp_rta. Require Export prosa.analysis.facts.busy_interval.carry_in. +Require Export prosa.analysis.facts.busy_interval.ideal.inequalities. (** * Abstract RTA for FIFO-schedulers *) (** In this module we instantiate the Abstract Response-Time analysis @@ -48,13 +49,13 @@ Section AbstractRTAforFIFOwithArrivalCurves. Variable sched : schedule (ideal.processor_state Job). Hypothesis H_valid_schedule : valid_schedule sched arr_seq. - (** Note that we differentiate between abstract and + (** Note that we differentiate between abstract and classical notions of work-conserving schedules. *) Let work_conserving_ab := definitions.work_conserving arr_seq sched. Let work_conserving_cl := work_conserving.work_conserving arr_seq sched. - (** We assume that the schedule is a work-conserving schedule - in the _classical_ sense, and later prove that the hypothesis + (** We assume that the schedule is a work-conserving schedule + in the _classical_ sense, and later prove that the hypothesis about abstract work-conservation also holds. *) Hypothesis H_work_conserving : work_conserving_cl. @@ -67,8 +68,8 @@ Section AbstractRTAforFIFOwithArrivalCurves. (** Next, we assume that all jobs come from the task set. *) Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts. - (** Let max_arrivals be a family of valid arrival curves, i.e., for any task [tsk] in [ts] - [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) a monotonic function + (** Let max_arrivals be a family of valid arrival curves, i.e., for any task [tsk] in [ts] + [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *) Context `{MaxArrivals Task}. Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals. @@ -87,15 +88,15 @@ Section AbstractRTAforFIFOwithArrivalCurves. Hypothesis H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold arr_seq tsk. (** We also assume that the schedule respects the policy defined by the preemption model. *) - Hypothesis H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job). + Hypothesis H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job). (** We introduce [rbf] as an abbreviation of the task request bound function, which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a given task [T]. *) Let rbf := task_request_bound_function. - (** Next, we introduce [task_rbf] as an abbreviation + (** Next, we introduce [task_rbf] as an abbreviation of the task request bound function of task [tsk]. *) - Let task_rbf := rbf tsk. + Let task_rbf := rbf tsk. (** For simplicity, let's define some local names. *) Let response_time_bounded_by := task_response_time_bound arr_seq sched. @@ -109,8 +110,8 @@ Section AbstractRTAforFIFOwithArrivalCurves. (** To reduce the time complexity of the analysis, we introduce the notion of search space for FIFO. Intuitively, this corresponds to all "interesting" arrival offsets that the job under analysis might have with regard to the beginning of its busy-window. *) - - (** In the case of FIFO, the final search space is the set of offsets less than [L] + + (** In the case of FIFO, the final search space is the set of offsets less than [L] such that there exists a task [tsko] from [ts] such that [rbf tsko (A) ≠rbf tsko (A + ε)]. *) Definition is_in_search_space (A : duration) := (A < L) && has (fun tsko => rbf tsko (A) != rbf tsko ( A + ε )) ts. @@ -120,29 +121,29 @@ Section AbstractRTAforFIFOwithArrivalCurves. in the search space, there exists a corresponding solution [F] such that [R >= F]. *) Variable R : duration. - Hypothesis H_R_is_maximum: + Hypothesis H_R_is_maximum: forall (A : duration), - is_in_search_space A -> + is_in_search_space A -> exists (F : nat), A + F >= \sum_(tsko <- ts) rbf tsko (A + ε) /\ F <= R. - (** To use the theorem [uniprocessor_response_time_bound] from the Abstract RTA module, + (** To use the theorem [uniprocessor_response_time_bound] from the Abstract RTA module, we need to specify functions that concretely define the abstract concepts interference, interfering workload, and [IBF]. *) - + (** ** Instantiation of Interference *) - (** We say that job [j] incurs interference at time [t] iff it cannot execute due to + (** We say that job [j] incurs interference at time [t] iff it cannot execute due to a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion. *) Let interference (j : Job) (t : instant) := ideal_jlfp_rta.interference arr_seq sched j t. (** ** Instantiation of Interfering Workload *) - (** The interfering workload, in turn, is defined as the sum of the priority inversion + (** The interfering workload, in turn, is defined as the sum of the priority inversion function and interfering workload of jobs with higher or equal priority. *) Let interfering_workload (j : Job) (t : instant) := ideal_jlfp_rta.interfering_workload arr_seq sched j t. - (** Finally, we define the interference bound function ([IBF]). [IBF] bounds the cumulative - interference incurred by a job. For FIFO, we define [IBF] as the sum of [RBF] for all tasks + (** Finally, we define the interference bound function ([IBF]). [IBF] bounds the cumulative + interference incurred by a job. For FIFO, we define [IBF] as the sum of [RBF] for all tasks in the interval [A + ε] minus the WCET of [tsk]. *) Let IBF tsk (A R : duration) := (\sum_(tsko <- ts) rbf tsko (A + ε)) - task_cost tsk. @@ -151,14 +152,14 @@ Section AbstractRTAforFIFOwithArrivalCurves. Section FillingOutHypothesesOfAbstractRTATheorem. (** In this section, we prove that, under FIFO scheduling, the cumulative priority inversion experienced - by a job [j] in any interval within its busy window is always [0]. We later use this fact to prove the bound on + by a job [j] in any interval within its busy window is always [0]. We later use this fact to prove the bound on the cumulative interference. *) Section PriorityInversion. (** Consider any job [j] of the task under consideration [tsk]. *) Variable j : Job. Hypothesis H_j_arrives : arrives_in arr_seq j. - Hypothesis H_job_of_tsk : job_task j = tsk. + Hypothesis H_job_of_tsk : job_of_task tsk j. (** Assume that the job has a positive cost. *) Hypothesis H_job_cost_positive: job_cost_positive j. @@ -172,32 +173,19 @@ Section AbstractRTAforFIFOwithArrivalCurves. Variable Δ : duration. Hypothesis H_Δ_in_busy : t1 + Δ < t2. - (** We prove that the cumulative priority inversion in the interval <<[t1, t1 + Δ)>> is [0]. *) - Lemma cumulative_priority_inversion_is_bounded: + (** We prove that the cumulative priority inversion in the interval + <<[t1, t1 + Δ)>> is [0]. *) + Lemma no_priority_inversion : cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ) = 0. Proof. - apply big_nat_eq0 => t /andP [T1 T2]; apply /eqP; rewrite eqb0. - apply/negP; intros T; move: T => /priority_inversion_P INV. - feed_n 3 INV; rt_eauto. - case: INV => [NSCHED [j__lp /andP [SCHED LP]]]. - move: LP; rewrite /hep_job /FIFO -ltnNge => LT. - have COMPL := early_hep_job_is_scheduled - _ _ _ _ H_valid_schedule _ H_respects_policy_at_preemption_point _ _ _ LT _ _ SCHED. - feed_n 5 COMPL; rt_eauto. - { by intros ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FIFO -ltnNge; apply/andP; split; first apply ltnW. } - move: (H_busy_interval) => [[/andP [ARR1 ARR2] [_ NQT]] _]. - move: T1; rewrite leq_eqVlt => /orP [/eqP EQ | GT]. - { subst t; apply completed_implies_scheduled_before in COMPL; rt_eauto. - by case: COMPL => [t' [/andP [ARR3 LT__temp] SCHED__temp]]; lia. - } - { apply: NQT; first (apply/andP; split; [exact GT | lia]). - apply quiet_time_cl_implies_quiet_time_ab; rt_eauto. - { by intros ? ? _ LE; unfold hep_job, FIFO. } - clear ARR2 ARR1 T2 H_Δ_in_busy Δ GT. - intros ? ARR HEP ARRB; rewrite /hep_job /FIFO in HEP. - eapply early_hep_job_is_scheduled; rt_eauto; first by lia. - by move => t'; apply/andP; split; rewrite /hep_job_at /FIFO /JLFP_to_JLDP /hep_job //=; lia. - } + apply /eqP; rewrite -leqn0. + pose zf : nat -> nat := (fun=> 0). + have: cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ) <= zf (job_arrival j - t1); + last by apply. + apply: cumulative_priority_inversion_is_bounded; rt_eauto. + have -> : priority_inversion_is_bounded_by arr_seq sched tsk zf + = priority_inversion_is_bounded_by_constant arr_seq sched tsk 0; + by try apply: FIFO_implies_no_pi; rt_eauto. Qed. End PriorityInversion. @@ -209,11 +197,11 @@ Section AbstractRTAforFIFOwithArrivalCurves. move => t1 t2 Δ j ARRj TSKj BUSY IN_BUSY NCOMPL. rewrite /cumul_interference cumulative_interference_split; rt_eauto. have JPOS: job_cost_positive j by rewrite -ltnNge in NCOMPL; unfold job_cost_positive; lia. - move: (BUSY) => [ [ /andP [LE GT] [QUIETt1 _ ] ] [QUIETt2 EQNs]]. - have CPIB := cumulative_priority_inversion_is_bounded j ARRj JPOS t1 t2. + move: (BUSY) => [ [ /andP [LE GT] [QUIETt1 _ ] ] [QUIETt2 EQNs]]. + have CPIB := no_priority_inversion j ARRj TSKj _ t1 t2. rewrite /cumulative_priority_inversion in CPIB; rewrite /ideal_jlfp_rta.cumulative_priority_inversion CPIB //= add0n. rewrite (cumulative_i_ohep_eq_service_of_ohep arr_seq) //=; - try by (try rewrite instantiated_quiet_time_equivalent_quiet_time); rt_eauto. + try by (try rewrite instantiated_quiet_time_equivalent_quiet_time); rt_eauto. eapply leq_trans; first by apply service_of_jobs_le_workload; rt_eauto. rewrite (leqRW (workload_equal_subset _ _ _ _ _ _ _)); rt_eauto. specialize (workload_minus_job_cost j) => ->. @@ -228,9 +216,9 @@ Section AbstractRTAforFIFOwithArrivalCurves. rewrite addnBA. { rewrite leq_sub2r //; eapply leq_trans. - apply sum_over_partitions_le => j' inJOBS. - by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS). + by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS). - rewrite (big_rem tsk) //= addnC leq_add //; last by rewrite subnKC. - rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=. + rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=. apply leq_sum => tsk' _; rewrite andbC //=. destruct (tsk' \in rem (T:=Task) tsk ts) eqn:IN; last by []. apply rem_in in IN. @@ -240,11 +228,11 @@ Section AbstractRTAforFIFOwithArrivalCurves. rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=. - by rewrite TSKj; apply leq_addr. - by apply job_in_arrivals_between => //; apply /andP; split; [| rewrite subnKC; [rewrite addn1 |]]. } - apply: arrivals_uniq => //. + apply: arrivals_uniq => //. apply: job_in_arrivals_between => //. by apply /andP; split; [ | rewrite addn1]. Qed. - + (** Finally, we show that there exists a solution for the response-time equation. *) Section SolutionOfResponseTimeReccurenceExists. @@ -253,20 +241,20 @@ Section AbstractRTAforFIFOwithArrivalCurves. Hypothesis H_j_arrives : arrives_in arr_seq j. Hypothesis H_job_of_tsk : job_of_task tsk j. Hypothesis H_positive_cost : 0 < task_cost tsk. - + (** Next, consider any [A] from the search space (in the abstract sense). *) Variable A : nat. Hypothesis H_A_is_in_abstract_search_space: search_space.is_in_search_space tsk L IBF A. - (** We prove that [A] is also in the concrete search space. In other words, + (** We prove that [A] is also in the concrete search space. In other words, we prove that the abstract search space is a subset of the concrete search space. *) Lemma A_is_in_concrete_search_space: is_in_search_space A. Proof. move: H_A_is_in_abstract_search_space => [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]]. unfold is_in_search_space. - { subst A. + { subst A. apply/andP; split; [by done |]. apply /hasP. exists tsk; first by done. rewrite neq_ltn;apply/orP; left. @@ -283,7 +271,7 @@ Section AbstractRTAforFIFOwithArrivalCurves. apply eq_big_seq => //= task IN. by move: (EQ2 task IN) => /negPn /eqP. } Qed. - + (** Then, there exists a solution for the response-time recurrence (in the abstract sense). *) Corollary exists_solution_for_abstract_response_time_recurrence: exists (F : nat), @@ -293,7 +281,7 @@ Section AbstractRTAforFIFOwithArrivalCurves. move : H_R_is_maximum => ABC. move: (H_valid_arrival_curve _ H_tsk_in_ts) => VARR. move: (H_is_arrival_curve _ H_tsk_in_ts) => RESP. - move : H_job_of_tsk => /eqP EQj. + move : H_job_of_tsk => /eqP EQj. specialize (ABC 0); feed ABC. { apply /andP; split; [by done| apply /hasP; exists tsk; first by done]. rewrite /task_rbf /rbf task_rbf_0_zero //= (add0n ε) neq_ltn. @@ -308,7 +296,7 @@ Section AbstractRTAforFIFOwithArrivalCurves. apply (task_cost_le_sum_rbf _ H_arrival_times_are_consistent _ VARR RESP j) => //. by rewrite addn1. - destruct H_valid_run_to_completion_threshold as [TASKvalid JOBvalid]. - by apply TASKvalid. + by apply TASKvalid. - rewrite addnBA; first by rewrite leq_sub2r // leq_add2l. have GE: task_cost tsk <= R; last by lia. rewrite !add0n in LE1. @@ -320,28 +308,27 @@ Section AbstractRTAforFIFOwithArrivalCurves. apply leq_trans with (task_cost tsk); first by lia. eapply task_cost_le_sum_rbf; rt_eauto. } Qed. - + End SolutionOfResponseTimeReccurenceExists. End FillingOutHypothesesOfAbstractRTATheorem. (** ** Final Theorem *) - (** Based on the properties established above, we apply the abstract analysis + (** Based on the properties established above, we apply the abstract analysis framework to infer that [R] is a response-time bound for [tsk]. *) Theorem uniprocessor_response_time_bound_FIFO: response_time_bounded_by tsk R. Proof. intros js ARRs TSKs. move: (posnP (@job_cost _ Cost js)) => [ZERO|POS]. - { by rewrite /job_response_time_bound /completed_by ZERO. } + { by rewrite /job_response_time_bound /completed_by ZERO. } ( try ( eapply uniprocessor_response_time_bound with (interference0 := interference) (interfering_workload0 := interfering_workload) (interference_bound_function := fun tsk A R => IBF tsk A R) (L0 := L) ) || eapply uniprocessor_response_time_bound with (interference := interference) (interfering_workload := interfering_workload) (interference_bound_function := fun tsk A R => IBF tsk A R) (L := L)); rt_eauto. - - by eapply instantiated_i_and_w_are_coherent_with_schedule; rt_eauto; last - by move => j1 j2 SAME ARR. + - by eapply instantiated_i_and_w_are_coherent_with_schedule; rt_eauto. - by eapply instantiated_busy_intervals_are_bounded; rt_eauto. - by apply instantiated_interference_is_bounded. - eapply (exists_solution_for_abstract_response_time_recurrence js) => //=. @@ -349,5 +336,5 @@ Section AbstractRTAforFIFOwithArrivalCurves. move: TSKs; rewrite /job_of_task => /eqP <-. by eapply H_valid_job_cost. Qed. - -End AbstractRTAforFIFOwithArrivalCurves. + +End AbstractRTAforFIFOwithArrivalCurves.