Commit 14e6daee authored by Martin PORTALIER's avatar Martin PORTALIER

Update main_theorem.v

parent dc7d9d60
Pipeline #18960 failed with stages
in 38 seconds
......@@ -27,14 +27,29 @@ Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
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 on jobs arrival. *)
Hypothesis H_arrives_in : forall jb, arrives_in arr_seq jb.
Hypothesis H_sched_none : forall t, sched t = None -> arr_seq t = [::].
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_positive_cost : forall jb, 0 < job_cost jb.
Let higher_eq_priority := hep_task.
Let jl_hep := FP_to_JLFP Job Task.
Hypothesis H_reflexive : reflexive higher_eq_priority.
Hypothesis H_transitive : transitive higher_eq_priority.
Hypothesis H_reflexive : reflexive jl_hep.
Hypothesis H_transitive : transitive jl_hep.
Hypothesis H_fpp : respects_preemptive_priorities arr_seq sched.
(* Hypothesis on jobs from a same task. *)
Hypothesis H_same_task_same_priority : forall j1 j2,
same_task j1 j2 <-> jl_hep j1 j2 && jl_hep j2 j1.
Hypothesis H_sporadic : forall j j',
job_arrival j = job_arrival j' -> same_task j j' -> j = j'.
Variable tsk: Task.
Variable ts: list Task.
(* Variable delta: duration. *)
......@@ -53,8 +68,10 @@ Definition task_workload_bound_FP : nat :=
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
(* Let W tsk_other := task_workload_bound_FP tsk_other delta. *)
(* task_worload_bound *)
Definition formula (delta : duration) : nat :=
\sum_(x <- ts | is_hep_task x && (tsk != x)) (task_workload_bound_FP x delta) + task_cost tsk. (* task_worload_bound *)
\sum_(x <- ts | is_hep_task x && (tsk != x))
(task_workload_bound_FP x delta) + task_cost tsk.
Variable R : duration.
......@@ -64,28 +81,36 @@ Hypothesis H_implicit_deadline: task_deadline tsk = task_min_inter_arrival_time
Section exists_t2.
Let workload_bound :=
total_workload_bound_fp higher_eq_priority ts tsk.
Let workload_bound := formula.
(* total_workload_bound_fp higher_eq_priority ts tsk. *)
Lemma exits_t2 delta: delta > 0 ->
workload_bound delta = delta ->
forall j , arrives_in arr_seq j ->
job_task j = tsk ->
exists t2, job_arrival j < t2 /\ quiet_time arr_seq sched jl_hep j t2.
Lemma exists_t2 : forall delta,
delta > 0 -> workload_bound delta = delta
-> (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.
Theorem fpp_implicit_deadline :
task_response_time_bound arr_seq sched tsk R. (* numero 5 *)
(* tsk's response time is bounded by R *)
task_response_time_bound arr_seq sched tsk R.
Proof.
unfold task_response_time_bound.
move => j H_arrives H_job_task.
unfold job_response_time_bound. unfold completed_by.
unfold service. unfold service_during.
unfold service_at.
SearchAbout "arrival". unfold service_in.
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 => d.
set t1 := start_of_analyse_interval arr_seq sched jl_hep j.
unfold workload_of_jobs. unfold formula.
SearchAbout "big" "cond".
rewrite big_filter_cond big_filter. SearchAbout "big" "change".
Admitted.
End main.
\ 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