Commit 4b5a2ff6 authored by Vedant Chavda's avatar Vedant Chavda

restructure periodic files

parent 9e5687dd
Pipeline #29008 failed with stages
in 15 minutes and 31 seconds
Require Export prosa.model.task.arrival.periodic.
Require Export prosa.analysis.facts.job_index.
Require Export prosa.analysis.facts.periodic_index.
Require Export prosa.analysis.facts.periodic_respects_TMIA.
(** In this module, we'll show a few properties of periodic tasks. *)
Section PeriodicModel.
......
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.model.task.arrival.task_max_inter_arrival.
Require Export prosa.model.task.offset.
Require Export prosa.analysis.facts.job_index.
Require Export prosa.model.task.arrival.periodic.
Require Export prosa.analysis.facts.periodic_index.
(** ** Treating Periodic Tasks as Sporadic Tasks *)
(** Since the periodic-arrivals assumption is stricter than the
sporadic-arrivals assumption (i.e., any periodic arrival sequence is also a
valid sporadic arrivals sequence), it is sometimes convenient to apply
analyses for sporadic tasks to periodic tasks. We therefore provide an
automatic "conversion" of periodic tasks to sporadic tasks, i.e., we tell
Coq that it may use a periodic task's [task_period] parameter also as the
task's minimum inter-arrival time [task_min_inter_arrival_time]
parameter. *)
Section PeriodicTasksAsSporadicTasks.
(** Any type of periodic tasks from a task set ... *)
Context {Task : TaskType} `{PeriodicModel Task}.
Variable ts : TaskSet Task.
(** ... and their corresponding jobs from a consistent
and unique arrival sequence ... *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals : forall arr_seq, consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq : forall (arr_seq : arrival_sequence Job), arrival_sequence_uniq arr_seq.
Hypothesis H_valid_periods : valid_periods_in_taskset ts.
Hypothesis H_periodic_taskset : taskset_respects_periodic_task_model ts arr_seq.
(** ... may be interpreted as a type of sporadic tasks by using each task's
period as its minimum inter-arrival time ... *)
Global Instance periodic_as_sporadic : SporadicModel Task :=
{
task_min_inter_arrival_time := task_period
}.
(** ... such that the model interpretation is valid, both w.r.t. the minimum
inter-arrival time parameter ... *)
Remark valid_period_is_valid_inter_arrival_time:
forall tsk, tsk \in ts -> valid_task_min_inter_arrival_time tsk.
Proof. trivial. Qed.
(** ... and the separation of job arrivals. *)
Remark periodic_task_respects_sporadic_task_model:
forall tsk, tsk \in ts ->
respects_sporadic_task_model arr_seq tsk.
Proof.
intros tsk TSK_IN. rewrite /respects_sporadic_task_model.
intros j1 j2 NEQ ARR ARR' TSK TSK' ARR_LT.
rewrite /task_min_inter_arrival_time /periodic_as_sporadic.
have PERIOD_MULTIPLE: exists n, n > 0 /\ job_arrival j2 = job_arrival j1 + (n * task_period tsk).
{ rewrite -TSK. rewrite -TSK' in TSK.
assert (job_task j1 = tsk) as TSKJ1; first by rewrite -TSK in TSK' => //.
now apply job_sep_periodic with (tsk0 := job_task j1) (arr_seq0 := arr_seq)
(ts0 := ts) => //; first by rewrite -TSKJ1 in TSK_IN => //.
}
move: PERIOD_MULTIPLE => [n [GT0 ->]]. rewrite addnC.
replace (job_arrival j1 + n * task_period tsk) with (n * task_period tsk + job_arrival j1); last by ssromega.
rewrite leq_add2r.
by apply leq_pmull.
Qed.
(** For convenience, we state these obvious correspondences also at the level
of entire task sets. *)
Remark valid_periods_are_valid_inter_arrival_times:
valid_taskset_inter_arrival_times ts.
Proof. trivial. Qed.
Remark periodic_task_sets_respect_sporadic_task_model:
taskset_respects_sporadic_task_model ts arr_seq.
Proof.
intros tsk TSK_IN.
apply periodic_task_respects_sporadic_task_model => //.
Qed.
End PeriodicTasksAsSporadicTasks.
This diff is collapsed.
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.model.task.arrival.task_max_inter_arrival.
Require Export prosa.model.task.offset.
Require Export prosa.analysis.facts.job_index.
Require Export prosa.model.task.arrival.periodic.
Require Export prosa.analysis.facts.periodic_index.
(** ** Periodic Task Model respects the Task Max Inter Arrival model. *)
(** In this section, we show that the periodic task model
respects the task max inter arrival model (i.e. consecutive jobs
of a task are separated at most by a certain duration specified by
the [task_max_inter_arrival_time] parameter). *)
Section PeriodicTasksRespectMaxInterArrivalModel.
(** Consider any type of periodic tasks from a task set [ts], ... *)
Context {Task : TaskType} `{PeriodicModel Task}.
Variable ts : TaskSet Task.
(** ... any type of jobs associated with the tasks, ... *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
(** ... and any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** By using each task's period as its maximum inter arrival time, ... *)
Global Instance max_inter_eq_period : TaskMaxInterArrival Task :=
{
task_max_inter_arrival_time := task_period
}.
(** ... we observe that for any task [tsk],
[task_max_inter_arrival_time tsk] is positive, ... *)
Remark valid_period_is_valid_max_inter_arrival_time:
forall tsk, valid_period tsk -> positive_task_max_inter_arrival_time tsk.
Proof. trivial. Qed.
(** ... and show that the periodic model respects the task max inter arrival model. *)
Remark periodic_model_respects_max_inter_arrival_model:
forall tsk,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
valid_task_max_inter_arrival_time arr_seq tsk.
Proof.
intros tsk VALID_PERIOD PERIODIC.
rewrite /valid_task_max_inter_arrival_time.
split; first by apply VALID_PERIOD => //.
intros j ARR TSK IND.
rewrite /respects_periodic_task_model in PERIODIC. specialize (PERIODIC j). feed_n 3 PERIODIC => //.
destruct PERIODIC as [j' [ARR' [IND' [TSK' ARRJ']]]].
exists j'. repeat split => //.
+ assert (job_index arr_seq j' <> job_index arr_seq j) as UNEQ_IND; first by ssromega.
case: (boolP (j == j')) => [/eqP EQ|NEQ]; last by move : NEQ => /eqP => //.
assert (job_index arr_seq j' = job_index arr_seq j) as EQ_IND; first by apply f_equal => //.
exfalso.
by ssromega.
+ assert (task_period tsk > 0) as NZ_PERIOD; first by apply VALID_PERIOD.
rewrite /max_inter_eq_period /task_max_inter_arrival_time ARRJ'.
now ssromega.
Qed.
End PeriodicTasksRespectMaxInterArrivalModel.
......@@ -59,7 +59,7 @@ Section ValidPeriodicTaskModel.
End ValidPeriodicTaskModel.
Section PeriodicModelLemmas.
(*Section PeriodicModelLemmas.
(** Consider periodic tasks with an offset ... *)
Context {Task : TaskType}.
......@@ -290,9 +290,9 @@ Section PeriodicModelLemmas.
now ssromega.
Qed.
End PeriodicModelLemmas.
End PeriodicModelLemmas.*)
(** ** Treating Periodic Tasks as Sporadic Tasks *)
(*(** ** Treating Periodic Tasks as Sporadic Tasks *)
(** Since the periodic-arrivals assumption is stricter than the
sporadic-arrivals assumption (i.e., any periodic arrival sequence is also a
......@@ -421,4 +421,4 @@ Section PeriodicTasksRespectMaxInterArrivalModel.
now ssromega.
Qed.
End PeriodicTasksRespectMaxInterArrivalModel.
End PeriodicTasksRespectMaxInterArrivalModel.*)
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