Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.task.arrival.periodic.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** ** 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 ... *)
Context {Task : TaskType} `{PeriodicModel Task}.
(** ... and their corresponding jobs from a consistent arrival sequence with
non-duplicate arrivals ... *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence 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 , valid_period tsk -> valid_task_min_inter_arrival_time tsk.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall tsk : Task,
valid_period tsk ->
valid_task_min_inter_arrival_time tsk
Proof .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall tsk : Task,
valid_period tsk ->
valid_task_min_inter_arrival_time tsk
trivial . Qed .
(** ... and the separation of job arrivals. *)
Remark periodic_task_respects_sporadic_task_model :
forall tsk , valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
respects_sporadic_task_model arr_seq tsk.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall tsk : Task,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
respects_sporadic_task_model arr_seq tsk
Proof .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall tsk : Task,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
respects_sporadic_task_model arr_seq tsk
intros tsk VALID_PERIOD H_PERIODIC j1 j2 NEQ ARR ARR' TSK TSK' ARR_LT.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk H_PERIODIC : respects_periodic_task_model arr_seq tsk j1, j2 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
rewrite /task_min_inter_arrival_time /periodic_as_sporadic.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk H_PERIODIC : respects_periodic_task_model arr_seq tsk j1, j2 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2
job_arrival j1 + task_period tsk <= job_arrival j2
have IND_LT : job_index arr_seq j1 < job_index arr_seq j2.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk H_PERIODIC : respects_periodic_task_model arr_seq tsk j1, j2 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2
job_index arr_seq j1 < job_index arr_seq j2
{ Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk H_PERIODIC : respects_periodic_task_model arr_seq tsk j1, j2 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2
job_index arr_seq j1 < job_index arr_seq j2
rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto ; last by rewrite TSK.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk H_PERIODIC : respects_periodic_task_model arr_seq tsk j1, j2 : Job ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2 NEQ : job_index arr_seq j1 <> job_index arr_seq j2
job_index arr_seq j1 < job_index arr_seq j2
move_neq_up IND_LTE; move_neq_down ARR_LT. Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk H_PERIODIC : respects_periodic_task_model arr_seq tsk j1, j2 : Job ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk NEQ : job_index arr_seq j1 <> job_index arr_seq j2 IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
job_arrival j2 < job_arrival j1
specialize (H_PERIODIC j1); feed_n 3 H_PERIODIC => //; try by lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j1 : Job H_PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j1 - 1 /\
job_task j' = tsk /\
job_arrival j1 =
job_arrival j' + task_period tskj2 : Job ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk NEQ : job_index arr_seq j1 <> job_index arr_seq j2 IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
job_arrival j2 < job_arrival j1
move : H_PERIODIC => [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j1, j2 : Job ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk NEQ : job_index arr_seq j1 <> job_index arr_seq j2 IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1 pj : Job ARR_PJ : arrives_in arr_seq pj IND_PJ : job_index arr_seq pj =
job_index arr_seq j1 - 1 TSK_PJ : job_task pj = tsk PJ_ARR : job_arrival j1 =
job_arrival pj + task_period tsk
job_arrival j2 < job_arrival j1
have JB_IND_LTE : job_index arr_seq j2 <= job_index arr_seq pj by lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j1, j2 : Job ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk NEQ : job_index arr_seq j1 <> job_index arr_seq j2 IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1 pj : Job ARR_PJ : arrives_in arr_seq pj IND_PJ : job_index arr_seq pj =
job_index arr_seq j1 - 1 TSK_PJ : job_task pj = tsk PJ_ARR : job_arrival j1 =
job_arrival pj + task_period tsk JB_IND_LTE : job_index arr_seq j2 <=
job_index arr_seq pj
job_arrival j2 < job_arrival j1
apply index_lte_implies_arrival_lte in JB_IND_LTE => //; try by rewrite TSK_PJ.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j1, j2 : Job ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk NEQ : job_index arr_seq j1 <> job_index arr_seq j2 IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1 pj : Job ARR_PJ : arrives_in arr_seq pj IND_PJ : job_index arr_seq pj =
job_index arr_seq j1 - 1 TSK_PJ : job_task pj = tsk PJ_ARR : job_arrival j1 =
job_arrival pj + task_period tsk JB_IND_LTE : job_arrival j2 <= job_arrival pj
job_arrival j2 < job_arrival j1
rewrite PJ_ARR.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j1, j2 : Job ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk NEQ : job_index arr_seq j1 <> job_index arr_seq j2 IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1 pj : Job ARR_PJ : arrives_in arr_seq pj IND_PJ : job_index arr_seq pj =
job_index arr_seq j1 - 1 TSK_PJ : job_task pj = tsk PJ_ARR : job_arrival j1 =
job_arrival pj + task_period tsk JB_IND_LTE : job_arrival j2 <= job_arrival pj
job_arrival j2 < job_arrival pj + task_period tsk
have POS_PERIOD : task_period tsk > 0 by auto .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j1, j2 : Job ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk NEQ : job_index arr_seq j1 <> job_index arr_seq j2 IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1 pj : Job ARR_PJ : arrives_in arr_seq pj IND_PJ : job_index arr_seq pj =
job_index arr_seq j1 - 1 TSK_PJ : job_task pj = tsk PJ_ARR : job_arrival j1 =
job_arrival pj + task_period tsk JB_IND_LTE : job_arrival j2 <= job_arrival pj POS_PERIOD : 0 < task_period tsk
job_arrival j2 < job_arrival pj + task_period tsk
by lia . } Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk H_PERIODIC : respects_periodic_task_model arr_seq tsk j1, j2 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2 IND_LT : job_index arr_seq j1 < job_index arr_seq j2
job_arrival j1 + task_period tsk <= job_arrival j2
specialize (H_PERIODIC j2); feed_n 3 H_PERIODIC => //; try by lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j2 : Job H_PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - 1 /\
job_task j' = tsk /\
job_arrival j2 =
job_arrival j' + task_period tskj1 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2 IND_LT : job_index arr_seq j1 < job_index arr_seq j2
job_arrival j1 + task_period tsk <= job_arrival j2
move : H_PERIODIC => [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j2, j1 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2 IND_LT : job_index arr_seq j1 < job_index arr_seq j2 pj : Job ARR_PJ : arrives_in arr_seq pj IND_PJ : job_index arr_seq pj =
job_index arr_seq j2 - 1 TSK_PJ : job_task pj = tsk PJ_ARR : job_arrival j2 =
job_arrival pj + task_period tsk
job_arrival j1 + task_period tsk <= job_arrival j2
have JB_IND_LTE : job_index arr_seq j1 <= job_index arr_seq pj by lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j2, j1 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2 IND_LT : job_index arr_seq j1 < job_index arr_seq j2 pj : Job ARR_PJ : arrives_in arr_seq pj IND_PJ : job_index arr_seq pj =
job_index arr_seq j2 - 1 TSK_PJ : job_task pj = tsk PJ_ARR : job_arrival j2 =
job_arrival pj + task_period tsk JB_IND_LTE : job_index arr_seq j1 <=
job_index arr_seq pj
job_arrival j1 + task_period tsk <= job_arrival j2
apply index_lte_implies_arrival_lte in JB_IND_LTE => //; try by rewrite TSK_PJ.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task VALID_PERIOD : valid_period tsk j2, j1 : Job NEQ : j1 <> j2 ARR : arrives_in arr_seq j1 ARR' : arrives_in arr_seq j2 TSK : job_task j1 = tsk TSK' : job_task j2 = tsk ARR_LT : job_arrival j1 <= job_arrival j2 IND_LT : job_index arr_seq j1 < job_index arr_seq j2 pj : Job ARR_PJ : arrives_in arr_seq pj IND_PJ : job_index arr_seq pj =
job_index arr_seq j2 - 1 TSK_PJ : job_task pj = tsk PJ_ARR : job_arrival j2 =
job_arrival pj + task_period tsk JB_IND_LTE : job_arrival j1 <= job_arrival pj
job_arrival j1 + task_period tsk <= job_arrival j2
by rewrite PJ_ARR; lia .
Qed .
(** For convenience, we state these obvious correspondences also at the level
of entire task sets. *)
(** First, we show that all tasks in a task set with valid periods
also have valid min inter-arrival times. *)
Remark valid_periods_are_valid_inter_arrival_times :
forall ts , valid_periods ts -> valid_taskset_inter_arrival_times ts.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall ts : TaskSet Task,
valid_periods ts ->
valid_taskset_inter_arrival_times ts
Proof .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall ts : TaskSet Task,
valid_periods ts ->
valid_taskset_inter_arrival_times ts
trivial . Qed .
(** Second, we show that each task in a periodic task set respects
the sporadic task model. *)
Remark periodic_task_sets_respect_sporadic_task_model :
forall ts ,
valid_periods ts ->
taskset_respects_periodic_task_model arr_seq ts ->
taskset_respects_sporadic_task_model ts arr_seq.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall ts : TaskSet Task,
valid_periods ts ->
taskset_respects_periodic_task_model arr_seq ts ->
taskset_respects_sporadic_task_model ts arr_seq
Proof .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall ts : TaskSet Task,
valid_periods ts ->
taskset_respects_periodic_task_model arr_seq ts ->
taskset_respects_sporadic_task_model ts arr_seq
intros ts VALID_PERIODS H_PERIODIC tsk TSK_IN.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : TaskSet Task VALID_PERIODS : valid_periods ts H_PERIODIC : taskset_respects_periodic_task_model
arr_seq ts tsk : Task TSK_IN : tsk \in ts
respects_sporadic_task_model arr_seq tsk
specialize (H_PERIODIC tsk TSK_IN).Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : TaskSet Task VALID_PERIODS : valid_periods ts tsk : Task H_PERIODIC : respects_periodic_task_model arr_seq tsk TSK_IN : tsk \in ts
respects_sporadic_task_model arr_seq tsk
exact : periodic_task_respects_sporadic_task_model.
Qed .
End PeriodicTasksAsSporadicTasks .
(** We add the lemmas into the "Hint Database" basic_rt_facts so that
they become available for proof automation. *)
Global Hint Resolve
periodic_task_respects_sporadic_task_model
valid_period_is_valid_inter_arrival_time
valid_periods_are_valid_inter_arrival_times
periodic_task_sets_respect_sporadic_task_model
: basic_rt_facts.