Commit bff26f1c authored by jonathan julou's avatar jonathan julou

definitions defined

parent c6a57412
Pipeline #19174 passed with stages
in 5 minutes and 15 seconds
From rt.restructuring Require Export behavior.schedule model.task model.arrival.periodic_jitter analysis.schedulability.
From rt.util Require Import ssromega.
From rt.restructuring.model Require Export preemptive.
From rt.restructuring.model Require Export work_conserving.
Set Bullet Behavior "Strict Subproofs".
Section ArrivalsDefs.
Context {Jobs : JobType} {Tasks : TaskType}.
......@@ -6,35 +11,167 @@ Section ArrivalsDefs.
Variable arr_seq : arrival_sequence Jobs.
Definition valid_arrival_sequence_up_to_t (t : instant) := True.
Definition consistent_arrival_times_up_to_t (t : instant) :=
forall j t', t' <= t -> arrives_at arr_seq j t -> job_arrival j = t.
Definition arrival_sequence_uniq_up_to_t (t : instant) :=
forall t', t' <= t -> uniq (jobs_arriving_at arr_seq t).
Definition valid_arrival_sequence_up_to_t (t : instant) :=
consistent_arrival_times_up_to_t t /\ arrival_sequence_uniq_up_to_t t.
Lemma valid_arrival_sequence_eq : valid_arrival_sequence arr_seq <-> forall t, valid_arrival_sequence_up_to_t t.
Admitted.
Proof.
split.
- intros P t. unfold valid_arrival_sequence_up_to_t.
unfold valid_arrival_sequence in P. destruct P as [A B]. split.
+ unfold consistent_arrival_times_up_to_t. intros j t' Q R.
unfold consistent_arrival_times in A. apply A. exact R.
+ unfold arrival_sequence_uniq in B. unfold arrival_sequence_uniq_up_to_t.
intros t' hyp. apply B.
- intros P. unfold valid_arrival_sequence. unfold valid_arrival_sequence_up_to_t in P.
unfold consistent_arrival_times_up_to_t in P. unfold arrival_sequence_uniq_up_to_t in P.
split.
+ unfold arrival_sequence.consistent_arrival_times. intros j t Q.
assert (extract: (forall (j : Jobs) (t' : nat), t' <= t -> arrives_at arr_seq j t -> job_arrival j = t) /\ (forall t' : nat, t' <= t -> uniq (jobs_arriving_at arr_seq t)))
by (apply P). destruct extract as [A' B'].
apply A' with t. apply leqnn. exact Q.
+ unfold arrival_sequence_uniq. intros t.
assert (extract: (forall (j : Jobs) (t' : nat), t' <= t -> arrives_at arr_seq j t -> job_arrival j = t) /\ (forall t' : nat, t' <= t -> uniq (jobs_arriving_at arr_seq t)))
by (apply P). destruct extract as [A' B'].
apply B' with t. apply leqnn.
Qed.
End ArrivalsDefs.
Section ScheduleDefs.
Context {Jobs : JobType} {Tasks : TaskType}.
Context `{JobArrival Jobs} `{JobCost Jobs}.
Context `{JobArrival Jobs} `{JobCost Jobs} `{JobTask Jobs Tasks}.
Context (State : Type) `{ProcessorState Jobs State}.
Variable arr_seq : arrival_sequence Jobs.
Variable sched : schedule State.
Definition valid_schedule_up_to_t (t : instant) := True.
Lemma valid_schedule_eq : valid_schedule sched arr_seq <-> forall t, valid_schedule_up_to_t t.
Admitted.
Definition jobs_come_from_arrival_sequence_up_to_t (arr_seq : arrival_sequence Jobs) (t : instant) :=
forall t' j, t' <= t -> scheduled_at sched j t' -> arrives_in arr_seq j.
Definition jobs_must_arrive_to_execute_up_to_t (t : instant) :=
forall t' j, t' <= t -> scheduled_at sched j t' -> has_arrived j t'.
Definition completed_jobs_dont_execute_up_to_t (t : instant) :=
forall t' j, t' <= t -> service sched j t' <= job_cost j.
Definition valid_schedule_up_to_t (arr_seq : arrival_sequence Jobs) (t : instant):=
jobs_come_from_arrival_sequence_up_to_t arr_seq t /\
jobs_must_arrive_to_execute_up_to_t t /\
completed_jobs_dont_execute_up_to_t t.
Local Ltac decomp_arr_seq_prop t P:=
assert (extract: (forall (t' : nat) (j : Jobs),
t' <= t -> scheduled_at sched j t' -> arrives_in arr_seq j) /\
(forall (t' : nat) (j : Jobs),
t' <= t -> scheduled_at sched j t' -> has_arrived j t') /\
(forall (t' : nat) (j : Jobs),
t' <= t -> service sched j t' <= job_cost j))
by (apply P); destruct extract as [A' B']; destruct B' as [B' C'].
Lemma valid_schedule_eq : valid_schedule sched arr_seq <-> forall t, valid_schedule_up_to_t arr_seq t.
Proof.
split.
- intros P t. unfold valid_schedule_up_to_t.
unfold valid_schedule in P. destruct P as [A P]. destruct P as [B C].
split. 2:split.
+ unfold jobs_come_from_arrival_sequence_up_to_t. intros t' j Q R.
unfold jobs_come_from_arrival_sequence in A. apply A with t'. exact R.
+ unfold jobs_must_arrive_to_execute in B.
unfold jobs_must_arrive_to_execute_up_to_t.
intros t' j hyp. apply B.
+ unfold completed_jobs_dont_execute in C.
unfold completed_jobs_dont_execute_up_to_t.
intros t' j Q. apply C.
- intros P. unfold valid_schedule. unfold valid_schedule_up_to_t in P.
unfold jobs_come_from_arrival_sequence_up_to_t in P. unfold jobs_must_arrive_to_execute_up_to_t in P.
unfold completed_jobs_dont_execute_up_to_t in P.
split. 2:split.
+ unfold jobs_come_from_arrival_sequence. intros j t Q.
decomp_arr_seq_prop t P.
apply A' with t. apply leqnn. exact Q.
+ unfold jobs_must_arrive_to_execute. intros j t Q.
decomp_arr_seq_prop t P.
apply B'. apply leqnn. exact Q.
+ unfold completed_jobs_dont_execute. intros j t.
decomp_arr_seq_prop t P.
apply C'. apply leqnn.
Qed.
Variable ts : seq Tasks.
(* TODO : all_jobs_from_taskset in model.task? + up_to_t + equiv *)
Definition all_jobs_from_taskset := valid_arrival_sequence arr_seq /\ ts = nil.
Definition all_jobs_from_taskset_up_to_t (t : instant) := True.
(* TODO : respects_preemptive_priorities_up_to_t + equiv *)
(* TODO : work_conserving_up_to_t + equiv *)
(* DONE : all_jobs_from_taskset in model.task? + up_to_t + equiv *)
(*Definition all_jobs_from_taskset := valid_arrival_sequence arr_seq /\ ts = nil.*)
Definition all_jobs_from_taskset := forall (j : Jobs), job_task j \in ts.
Definition all_jobs_from_taskset_up_to_t (t : instant) := forall (j : Jobs),
job_arrival j <= t -> job_task j \in ts.
Lemma all_jobs_from_taskset_eq : all_jobs_from_taskset <-> forall t, all_jobs_from_taskset_up_to_t t.
Proof.
split.
- intros P t. unfold all_jobs_from_taskset in P.
unfold all_jobs_from_taskset_up_to_t. intros j Q.
apply P.
- intro P. unfold all_jobs_from_taskset_up_to_t in P.
unfold all_jobs_from_taskset. intro j.
apply P with (job_arrival j). apply leqnn.
Qed.
(* DONE : respects_preemptive_priorities_up_to_t + equiv *)
Context `{JLDP_policy Jobs}.
Definition respects_preemptive_priorities_up_to_t (t : instant) :=
forall j j_hp t', t' <= t ->
arrives_in arr_seq j ->
backlogged sched j t ->
scheduled_at sched j_hp t ->
hep_job_at t j_hp j.
Lemma respects_preemptive_priorities_eq : respects_preemptive_priorities arr_seq sched <-> forall t, respects_preemptive_priorities_up_to_t t.
Proof.
split.
- intros P t. unfold respects_preemptive_priorities in P.
unfold respects_preemptive_priorities_up_to_t. intros j j_hp t' Q.
apply P.
- intros P. unfold respects_preemptive_priorities_up_to_t in P.
unfold respects_preemptive_priorities. intros j j_hp t.
apply P with t. apply leqnn.
Qed.
(* DONE : work_conserving_up_to_t + equiv *)
Definition work_conserving_up_to_t t:=
forall j t', t' <= t ->
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other, scheduled_at sched j_other t.
Lemma work_conserving_eq : work_conserving arr_seq sched <-> forall t, work_conserving_up_to_t t.
Proof.
split.
- intros P t. unfold work_conserving in P.
unfold work_conserving_up_to_t. intros j j_hp t'.
apply P.
- intros P. unfold work_conserving_up_to_t in P.
unfold work_conserving. intros j t.
apply P with t. apply leqnn.
Qed.
End ScheduleDefs.
......@@ -49,12 +186,21 @@ Section Transformation.
Variable R : duration.
Hypothesis Hanalysis_correct :
Hypothesis H_analysis_correct :
forall arr_seq : arrival_sequence Jobs,
valid_arrival_sequence arr_seq ->
all_jobs_from_taskset arr_seq ts ->
all_jobs_from_taskset ts ->
forall sched : schedule State,
valid_schedule sched arr_seq (* etc *) ->
task_response_time_upper_bound arr_seq sched tsk R.
(*
Hypothesis response_time_analysis :
forall t tsk, tsk \in ts ->
forall tsk, tsk \in ts -> task_correct_temporal_step tsk t ->
(task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT tsk) tsk
/\
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk ).
*)
End Transformation.
\ 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