Commit 8f16ef34 authored by Sergey Bozhko's avatar Sergey Bozhko

Add non-seq aRTA

parent 57d356ee
Pipeline #19741 passed with stages
in 5 minutes and 50 seconds
This diff is collapsed.
This diff is collapsed.
From rt.util Require Import epsilon tactics.
From rt.restructuring.model Require Import task.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Reduction of the serach space for Abstract RTA *)
(** In this file, we prove that in order to calculate the worst-case response time
it is sufficient to consider only values of A that lie in the search space defined below. *)
Section AbstractRTAReduction.
(* The response-time analysis we are presenting in this series of documents is based on searching
over all possible values of A, the relative arrival time of the job respective to the beginning
of the busy interval. However, to obtain a practically useful response-time bound, we need to
constrain the search space of values of A. In this section, we define an approach to
reduce the search space. *)
Context {Task : TaskType}.
(* First, we provide a constructive notion of equivalent functions. *)
Section EquivalentFunctions.
(* Consider an arbitrary type T... *)
Context {T : eqType}.
(* ...and two function from nat to T. *)
Variables f1 f2 : nat -> T.
(* Let B be an arbitrary constant. *)
Variable B : nat.
(* Then we say that f1 and f2 are equivalent at values less than B iff
for any natural number x less than B [f1 x] is equal to [f2 x]. *)
Definition are_equivalent_at_values_less_than :=
forall x, x < B -> f1 x = f2 x.
(* And vice versa, we say that f1 and f2 are not equivalent at values
less than B iff there exists a natural number x less than B such
that [f1 x] is not equal to [f2 x]. *)
Definition are_not_equivalent_at_values_less_than :=
exists x, x < B /\ f1 x <> f2 x.
End EquivalentFunctions.
(* Let tsk be any task that is to be analyzed *)
Variable tsk : Task.
(* To ensure that the analysis procedure terminates, we assume an upper bound B on
the values of A that must be checked. The existence of B follows from the assumption
that the system is not overloaded (i.e., it has bounded utilization). *)
Variable B : duration.
(* Instead of searching for the maximum interference of each individual job, we
assume a per-task interference bound function [IBF(tsk, A, x)] that is parameterized
by the relative arrival time A of a potential job (see abstract_RTA.definitions.v file). *)
Variable interference_bound_function : Task -> duration -> duration -> duration.
(* Recall the definition of ε, which defines the neighborhood of a point in the timeline.
Note that epsilon = 1 under discrete time. *)
(* To ensure that the search converges more quickly, we only check values of A in the interval
[0, B) for which the interference bound function changes, i.e., every point x in which
interference_bound_function (A - ε, x) is not equal to interference_bound_function (A, x). *)
Definition is_in_search_space A :=
A = 0 \/
0 < A < B /\ are_not_equivalent_at_values_less_than
(interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.
(* In this section we prove that for every A there exists a smaller A_sp
in the search space such that interference_bound_function(A_sp,x) is
equal to interference_bound_function(A, x). *)
Section ExistenceOfRepresentative.
(* Let A be any constant less than B. *)
Variable A : duration.
Hypothesis H_A_less_than_B : A < B.
(* We prove that there exists a constant A_sp such that:
(a) A_sp is no greater than A, (b) interference_bound_function(A_sp, x) is
equal to interference_bound_function(A, x) and (c) A_sp is in the search space.
In other words, either A is already inside the search space, or we can go
to the "left" until we reach A_sp, which will be inside the search space. *)
Lemma representative_exists:
exists A_sp,
A_sp <= A /\
are_equivalent_at_values_less_than (interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp.
induction A as [|n].
- exists 0; repeat split.
by rewrite /is_in_search_space; left.
- have ALT:
all (fun t => interference_bound_function tsk n t == interference_bound_function tsk n.+1 t) (iota 0 B)
\/ has (fun t => interference_bound_function tsk n t != interference_bound_function tsk n.+1 t) (iota 0 B).
{ apply/orP.
rewrite -[_ || _]Bool.negb_involutive Bool.negb_orb.
apply/negP; intros CONTR.
move: CONTR => /andP [NALL /negP NHAS]; apply: NHAS.
by rewrite -has_predC /predC in NALL.
feed IHn; first by apply ltn_trans with n.+1.
move: IHn => [ASP [NEQ [EQ SP]]].
move: ALT => [/allP ALT| /hasP ALT].
{ exists ASP; repeat split; try done.
{ by apply leq_trans with n. }
{ intros x LT.
move: (ALT x) => T. feed T; first by rewrite mem_iota; apply/andP; split.
move: T => /eqP T.
by rewrite -T EQ.
{ exists n.+1; repeat split; try done.
rewrite /is_in_search_space; right.
split; first by apply/andP; split.
move: ALT => [y IN N].
exists y.
move: IN; rewrite mem_iota add0n. move => /andP [_ LT].
split; first by done.
rewrite subn1 -pred_Sn.
intros CONTR; move: N => /negP N; apply: N.
by rewrite CONTR.
End ExistenceOfRepresentative.
(* In this section we prove that any solution of the response-time recurrence for
a given point A_sp in the search space also gives a solution for any point
A that shares the same interference bound. *)
Section FixpointSolutionForAnotherA.
(* Suppose A_sp + F_sp is a "small" solution (i.e. less than B) of the response-time recurrence. *)
Variables A_sp F_sp : duration.
Hypothesis H_less_than : A_sp + F_sp < B.
Hypothesis H_fixpoint : A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).
(* Next, let A be any point such that: (a) A_sp <= A <= A_sp + F_sp and
(b) interference_bound_function(A, x) is equal to
interference_bound_function(A_sp, x) for all x less than B. *)
Variable A : duration.
Hypothesis H_bounds_for_A : A_sp <= A <= A_sp + F_sp.
Hypothesis H_equivalent :
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B.
(* We prove that there exists a consant F such that [A + F] is equal to [A_sp + F_sp]
and [A + F] is a solution for the response-time recurrence for A. *)
Lemma solution_for_A_exists:
exists F,
A_sp + F_sp = A + F /\
F <= F_sp /\
A + F = interference_bound_function tsk A (A + F).
move: H_bounds_for_A => /andP [NEQ1 NEQ2].
set (X := A_sp + F_sp) in *.
exists (X - A); split; last split.
- by rewrite subnKC.
- by rewrite leq_subLR /X leq_add2r.
- by rewrite subnKC // H_equivalent.
End FixpointSolutionForAnotherA.
End AbstractRTAReduction.
From rt.util Require Import epsilon sum tactics search_arg.
From rt.restructuring.behavior Require Import job schedule.
From rt.restructuring.analysis.basic_facts Require Import completion.
From rt.restructuring.model Require Import job task preemption.preemption_model.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** * Run-to-completion threshold *)
(** In this file, we provide definition and properties
of run-to-completion-threshold-compilant schedules. *)
Section RunToCompletionThreshold.
(* 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}.
(* In addition, we assume existence of a function
maping jobs to theirs preemption points ... *)
Context `{JobPreemptable Job}.
(* ...and a function mapping tasks to theirs
run-to-completion threshold. *)
Context `{TaskRunToCompletionThreshold Task}.
(* Consider any kind of processor state model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(* ... any job arrival sequence, ... *)
Variable arr_seq: arrival_sequence Job.
(* ... and any given schedule. *)
Variable sched: schedule PState.
(* In this section we define the notion of a run-to-completion threshold for a job. *)
Section JobRunToCompletionThreshold.
(* We define the notion of job's run-to-completion threshold: run-to-completion threshold
is the amount of service after which a job cannot be preempted until its completion. *)
Definition runs_to_completion_from (j : Job) (ρ : duration) :=
all (fun (δ : duration) => ~~ job_preemptable j δ) (index_iota ρ (job_cost j)).
(* Note that a run-to-completion threshold exists for any job. *)
Lemma eventually_runs_to_completion:
forall (j : Job), exists (ρ : duration), runs_to_completion_from j ρ.
intros; exists (job_cost j).
intros t; rewrite mem_index_iota; move => /andP [GE LT]; exfalso.
by move: GE; rewrite leqNgt; move => /negP GE; apply: GE.
(* We define run-to-completion threshold of a job as the minimal progress
the job should reach to become non-preemptive until completion. *)
Definition job_run_to_completion_threshold (j : Job) : duration :=
ex_minn (eventually_runs_to_completion j).
(* In this section we prove a few simple lemmas
about run-to-completion threshold for a job. *)
Section Lemmas.
(* Assume that the preemption model is valid. *)
Hypothesis H_valid_preemption_model:
valid_preemption_model arr_seq sched.
(* Consider an arbitrary job j from the arrival sequence. *)
Variable j : Job.
Hypothesis H_j_in_arrival_seq : arrives_in arr_seq j.
(* First, we prove that a job cannot be preempted
during execution of the last segment. *)
Lemma job_cannot_be_preempted_within_last_segment:
forall (ρ : duration),
job_run_to_completion_threshold j <= ρ < job_cost j ->
~~ job_preemptable j ρ.
move => ρ /andP [GE LT].
pattern (job_run_to_completion_threshold j) in GE; apply prop_on_ex_minn in GE.
move: GE => [n [LE [RUNS MIN]]].
move: RUNS => /allP RUNS.
by apply RUNS; rewrite mem_index_iota; apply/andP; split.
(* We prove that the run-to-completion threshold is positive for any job. I.e., in order
to become non-preemptive a job must receive at least one unit of service. *)
Lemma job_run_to_completion_threshold_positive:
job_cost_positive j ->
0 < job_run_to_completion_threshold j.
intros COST.
rewrite lt0n; apply/neqP; intros F.
pattern (job_run_to_completion_threshold j) in F;
apply prop_on_ex_minn in F; move: F => [n [EQ [RUNS _]]]; subst n.
move: RUNS => /allP F; specialize (F 0); feed F.
{ rewrite mem_iota; apply/andP; split; auto.
rewrite subn0 add0n //. }
move: F => /negP F; apply: F.
by apply H_valid_preemption_model.
(* Next we show that the run-to-completion threshold
is at most the cost of a job. *)
Lemma job_run_to_completion_threshold_le_job_cost:
job_cost_positive j ->
job_run_to_completion_threshold j <= job_cost j.
intros COST.
apply ex_minn_le_ex.
intros t; rewrite mem_index_iota; move => /andP [GE LT]; exfalso.
by move: GE; rewrite leqNgt; move => /negP GE; apply: GE.
(* In order to get a consistent schedule, the scheduler should respect
the notion of run-to-completion threshold. We assume that, after
a job reaches its run-to-completion threshold, it cannot be preempted
until its completion. *)
Lemma job_nonpreemptive_after_run_to_completion_threshold:
forall t t',
t <= t' ->
job_run_to_completion_threshold j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t'.
intros ? ? LE TH COM.
apply H_valid_preemption_model; first by done.
apply job_cannot_be_preempted_within_last_segment; apply/andP; split.
- by apply leq_trans with (service sched j t); last apply service_monotonic.
- by rewrite ltnNge.
End Lemmas.
End JobRunToCompletionThreshold.
(* Since a task model may not provide exact information about preemption point of
a task run-to-completion, task's run-to-completion threshold cannot be defined in
terms of preemption points of a task (unlike job's run-to-completion threshold).
Therefore, one can assume the existence of a function that maps a task to
its run-to-completion threshold. In this section we define the notion
of a valid run-to-completion threshold of a task. *)
Section ValidTaskRunToCompletionThreshold.
(* A task's run-to-completion threshold should be at most the cost of the task. *)
Definition task_run_to_completion_threshold_le_task_cost tsk :=
task_run_to_completion_threshold tsk <= task_cost tsk.
(* We say that the run-to-completion threshold of a task tsk
bounds the job run-to-completionthreshold iff for any job j
of task tsk the job run-to-completion threshold is less than
or equal to the task run-to-completion threshold. *)
Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
forall j,
arrives_in arr_seq j ->
job_task j = tsk ->
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk.
(* We say that task_run_to_completion_threshold is a valid task run-to-completion
threshold for a task tsk iff [task_run_to_completion_threshold tsk] is (1) no
bigger than tsk's cost, (2) for any job of task tsk job_run_to_completion_threshold
is bounded by task_run_to_completion_threshold. *)
Definition valid_task_run_to_completion_threshold tsk :=
task_run_to_completion_threshold_le_task_cost tsk /\
task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk.
End ValidTaskRunToCompletionThreshold.
End RunToCompletionThreshold.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment