From rt.restructuring.model Require Export task task_cost arrival.sporadic priority_based.priorities
priority_based.preemptive workload.
From rt.restructuring.analysis Require Export
schedulability.
From rt.restructuring.analysis.fpp_implicit_deadline Require Export
workload_bound_fp intermediate.
From rt.restructuring.behavior.schedule Require Export ideal.
From mathcomp Require Import seq.
From rt.util Require Import div_mod sum tactics ssromega.
Section main.
Context (Task: TaskType).
Context `{TaskDeadline Task}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{SporadicModel Task} `{TaskCost Task}.
Context `{FP_policy Task }.
(* Let ts be any task set with valid task parameters. *)
Variable ts: list Task.
Hypothesis H_valid_task_parameters: forall tsk, tsk \in ts ->
(task_cost tsk) > 0 /\ (task_min_inter_arrival_time tsk) > 0
/\ (task_deadline tsk) > 0 /\ (task_cost tsk) <= (task_deadline tsk)
/\ (task_cost tsk) <= (task_min_inter_arrival_time tsk)
/\ task_deadline tsk <= task_min_inter_arrival_time tsk.
(* Let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Hypothesis H_uniq: uniq ts.
(* Suppose that the task deadlines are implicit. *)
Hypothesis H_implicit_deadline: forall tsk',
task_deadline tsk' = task_min_inter_arrival_time tsk'.
(* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
(* Suppose that the task model is sporadic. *)
Hypothesis H_sporadic_tasks: respects_sporadic_task_model arr_seq.
(* All jobs considered are in arr_seq: they arrive at the instant 'job_arrival jb' *)
Hypothesis H_arrives_in : forall jb, arrives_in arr_seq jb.
(* Consider any schedule with valid parameters such as work conserving or seqential arrival. *)
Variable sched : schedule (processor_state Job).
Hypothesis H_valid_sched : valid_schedule sched arr_seq.
Hypothesis H_work_conserving: work_conserving arr_seq sched.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_sched_none : forall t, sched t = None -> arr_seq t = [::].
(* Assume that all jobs come from the task set ...*)
Hypothesis H_all_jobs_from_taskset: forall j,
arrives_in arr_seq j -> job_task j \in ts.
(* ...and have valid parameters. *)
Hypothesis H_valid_job_parameters: forall j,
arrives_in arr_seq j -> job_cost j > 0 /\
job_cost j <= task_cost (job_task j)/\ job_cost j <= job_deadline j
/\ job_deadline j = task_deadline (job_task j).
(* Assume any fixed-priority policy with valid properties... *)
Let higher_eq_priority := hep_task.
Let jl_hep := (fun j1 j2 => higher_eq_priority (job_task j1) (job_task j2)).
Hypothesis H_fpp : respects_preemptive_priorities arr_seq sched.
(* ...which is an order relation. *)
Hypothesis H_reflexive : reflexive higher_eq_priority /\ reflexive jl_hep.
Hypothesis H_antisymmetric: antisymmetric higher_eq_priority.
Hypothesis H_transitive : transitive jl_hep.
(* Definition of the task workload bound. *)
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Definition formula (delta : duration) : nat :=
\sum_(x <- ts | is_hep_task x && (x != tsk))
(task_workload_bound_FP x delta) + task_cost tsk.
(* Suppose that the task workload bound has a fixpoint R lower than the task deadline. *)
Variable R : duration.
Hypothesis H_valid_R : formula R = R /\ R > 0 /\ R <= task_deadline tsk.
(* In this section we prove that all jobs terminate.
Then we can define the exact instant t2 when it happens. *)
Section exists_t2.
Let workload_bound := formula.
Lemma exists_t2 : forall delta,
delta > 0 -> workload_bound delta = delta
-> delta <= task_deadline tsk
-> (forall j, arrives_in arr_seq j -> job_task j = tsk ->
exists t2, job_arrival j < t2 /\ completes_at sched j t2).
Proof.
Admitted.
End exists_t2.
(* In this section we prove that the fixpoint R of the workload
is a bound for the task reponse time of tsk. *)
Section Fixpoint_bound.
(* Lemma about rewrite the formula and the workload_bound. *)
Lemma rwt_formula: forall r,
0 < r -> r <= task_deadline tsk
-> formula r = \sum_(x <- ts | higher_eq_priority x tsk)
task_workload_bound_FP x r.
Proof.
move => r H_pos H_inf. unfold task_workload_bound_FP.
rewrite big_mkcond (bigD1_seq tsk)/=; auto.
have ->: higher_eq_priority tsk tsk by apply H_reflexive.
rewrite addnC -big_mkcondl/=. unfold formula.
unfold task_workload_bound_FP. unfold max_jobs. rewrite ceil_eq1.
rewrite mul1n. auto. easy. apply leq_trans with (n:=task_deadline tsk).
easy. apply H_valid_task_parameters; auto.
Qed.
(* Main theorem of this section. *)
Theorem fpp_implicit_deadline :
task_response_time_bound arr_seq sched tsk R.
Proof.
unfold task_response_time_bound.
move => j H_arrives H_job_task.
have [t2 H_t2]: exists t2, job_arrival j < t2 /\ completes_at sched j t2.
apply exists_t2 with (delta:=R); easy.
apply resp_time_bound with (arr_seq0:=arr_seq)
(higher_eq_priority0:=jl_hep) (end_of_analyse_interval:=t2)
(workload_bound:=formula); try easy.
move => j0; apply H_valid_job_parameters; auto.
move => jb. apply H_valid_task_parameters. apply H_all_jobs_from_taskset; auto.
move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
unfold jl_hep in H_and. apply H_antisymmetric. auto.
set t1 := start_of_analyse_interval arr_seq sched jl_hep j.
unfold workload_of_jobs.
apply leq_trans with (n:=\sum_(j0 <- jobs_arrived_between arr_seq t1 (t1 + R) |
higher_eq_priority (job_task j0) (job_task j)) job_cost j0).
apply inf_workload; auto.
move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
unfold jl_hep in H_and. apply H_antisymmetric. auto. have H_fix: formula R = R by easy. rewrite H_fix.
apply fp_workload_bound_holds with (ts0:=ts); auto.
rewrite -{1}H_fix. rewrite rwt_formula; try easy. rewrite H_job_task; auto.
Qed.
End Fixpoint_bound.
(* In this section we prove that the bound is reached.
In other words, there exists a job j and an arrival sequence such that
its reponse time is equal to the fixpoint R. *)
Section Reached_bound.
(* Suppose that R is the smallest fixpoint. *)
Hypothesis H_smallest_fixpoint:
forall r, formula r = r -> R <= r.
(* Suppose that all jobs cost are maximised. *)
Hypothesis H_task_cost: forall jb,
job_cost jb = task_cost (job_task jb).
(* Suppose that as soon as it is possible, there exists a jobs that arrives.
In others words, the arrival sequence model is periodic. *)
Hypothesis H_periodic: forall j1 t,
j1 \in jobs_arriving_at arr_seq t -> exists j2,
j2 \in jobs_arriving_at arr_seq (t + task_min_inter_arrival_time (job_task j1))
/\ same_task j1 j2.
(* Consider a job j from the task tsk. *)
Variable j: Job.
Hypothesis H_job_task: job_task j = tsk.
(* Suppose that all job from a highest priority than j
arrive exactly at the same time of j. *)
Hypothesis H_all_arrives:
forall tsk', higher_eq_priority tsk' tsk
-> exists jb, jb \in jobs_arriving_at arr_seq (job_arrival j)
/\ job_task jb = tsk'.
(* Suppose that the system is schedulable:
all jobs terminate before their deadline. *)
Hypothesis H_is_schedulable: forall jb,
completed_by sched jb (job_arrival jb + (job_deadline jb)).
(* Main theorem of this section:
the job j completes exactly at the instant (job_arrival j) + R. *)
Theorem max_bound_reach:
completes_at sched j ((job_arrival j) + R).
Proof.
have [t2 H_t2]: exists t2, job_arrival j < t2 /\ completes_at sched j t2.
apply exists_t2 with (delta:=R); easy.
set t1 := start_of_analyse_interval arr_seq sched jl_hep j.
have H_t1: t1 = start_of_analyse_interval arr_seq sched jl_hep j by auto.
have H_start_interval_arrival: t1 = job_arrival j. rewrite H_t1.
rewrite -> start_interval_arrival with (task_hep:=higher_eq_priority)
(workload_bound:=formula) (r:=R); try easy.
move => tsk' H_hp. apply H_all_arrives. rewrite -H_job_task. auto.
move => jb. have ->: job_deadline jb = task_deadline (job_task jb).
apply H_valid_job_parameters; auto. apply H_implicit_deadline.
have H_arr_inf: job_arrival j < t2 by easy.
have H_main: t2 - (job_arrival j) = R. {
rewrite -H_start_interval_arrival. apply /eqP. rewrite eqn_leq.
apply vlib__leq_split.
apply len_inf_r with (workload_bound:=formula); try easy.
move => j0; apply H_valid_job_parameters; auto.
move => jb. apply H_valid_task_parameters. apply H_all_jobs_from_taskset; auto.
move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
unfold jl_hep in H_and. apply H_antisymmetric. auto. unfold workload_of_jobs.
apply leq_trans with (n:=\sum_(j0 <- jobs_arrived_between arr_seq t1 (t1 + R) |
higher_eq_priority (job_task j0) (job_task j)) job_cost j0).
apply inf_workload; auto.
move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
unfold jl_hep in H_and. apply H_antisymmetric. auto. have H_fix: formula R = R by easy. rewrite H_fix.
apply fp_workload_bound_holds with (ts0:=ts); auto.
rewrite -{1}H_fix. rewrite rwt_formula; try easy. rewrite H_job_task; auto.
apply H_smallest_fixpoint. rewrite rwt_formula.
rewrite H_start_interval_arrival. unfold task_workload_bound_FP.
rewrite <- pre_workload_reach with (r:=(t2 - job_arrival j)) (j0:=j) (ts0:=ts)
(arr_seq0:=arr_seq) (higher_eq_priority0:=higher_eq_priority) (tsk0:=tsk)
(R0:=R); try easy.
rewrite rwt_hp_workload.
rewrite -H_start_interval_arrival. apply esym.
rewrite {1}service_eq_nat_len; try easy. rewrite serv_eq_workload; try easy.
rewrite -> rewrite_workload with (task_hep:=higher_eq_priority)
(workload_bound:=formula) (r:=R) (arr_seq0:=arr_seq) (end_of_analyse_interval:=t2)
(j0:=j) (higher_eq_priority0:=jl_hep) (sched0:=sched); try easy.
rewrite -H_t1. unfold jl_hep. rewrite H_job_task; auto.
move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
unfold jl_hep in H_and. apply H_antisymmetric. auto.
rewrite H_job_task; auto. move => jb.
have ->: job_deadline jb = task_deadline (job_task jb).
apply H_valid_job_parameters; auto. apply H_implicit_deadline.
move => jb. apply H_valid_task_parameters. apply H_all_jobs_from_taskset; auto.
move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
unfold jl_hep in H_and. apply H_antisymmetric. auto.
move => jb. apply H_valid_job_parameters; auto.
have {1}<-: formula R = R by easy. rewrite rwt_formula; try easy.
ssromega. rewrite H_start_interval_arrival.
have H_tmp: job_arrival j < t2 by easy. ssromega.
have H_inf1: t2 <= t1 + task_deadline tsk.
have H_comp: completes_at sched j t2 by easy.
case E: (job_arrival j + job_deadline j < t2). apply lt_leq1 in E.
unfold completes_at in H_comp. move /andP in H_comp.
have H_no_comp: ~~ completed_by sched j t2.-1 by easy.
apply decr_no_completed with (t:=job_arrival j + job_deadline j) in H_no_comp; auto.
have H_contr: completed_by sched j (job_arrival j + job_deadline j)
by apply H_is_schedulable. move /negP in H_no_comp. auto.
apply leq_ltn_trans with (n:=job_arrival j); auto.
have E': t2 <= job_arrival j + job_deadline j. ssromega.
rewrite H_start_interval_arrival. rewrite -H_job_task.
have <-: job_deadline j = task_deadline (job_task j).
apply H_valid_job_parameters; auto. easy. ssromega. }
have <-: t2 = job_arrival j + R by ssromega. easy.
Qed.
End Reached_bound.
End main.