Library prosa.analysis.facts.sporadic
The Sporadic Model
Consider sporadic tasks with an offset ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{SporadicModel Task}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{SporadicModel Task}.
... and any type of jobs associated with these tasks.
Consider any unique arrival sequence with consistent arrivals, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
... and any sporadic task tsk that is to be analyzed.
Variable tsk : Task.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Consider any two jobs from the arrival sequence that stem
from task tsk.
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
Variable j2 : Job.
Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
We first show that for any two jobs j1 and j2, j2 arrives after j1
provided job_index of j2 strictly exceeds the job_index of j1.
Lemma lower_index_implies_earlier_arrival:
job_index arr_seq j1 < job_index arr_seq j2 →
job_arrival j1 < job_arrival j2.
End SporadicModelIndexLemmas.
job_index arr_seq j1 < job_index arr_seq j2 →
job_arrival j1 < job_arrival j2.
End SporadicModelIndexLemmas.
Consider sporadic tasks with an offset ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{SporadicModel Task}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{SporadicModel Task}.
... and any type of jobs associated with these tasks.
Consider any unique arrival sequence with consistent arrivals, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
... and any sporadic task tsk that is to be analyzed.
Variable tsk : Task.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Consider any two jobs from the arrival sequence that stem
from task tsk.
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
Variable j2 : Job.
Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
We observe that distinct jobs cannot have equal arrival times.
We prove a stronger version of the above lemma by showing
that jobs j1 and j2 are equal if and only if they arrive at the
same time.
Lemma same_jobs_iff_same_arr:
j1 = j2 ↔
job_arrival j1 = job_arrival j2.
End DifferentJobsImplyDifferentArrivalTimes.
j1 = j2 ↔
job_arrival j1 = job_arrival j2.
End DifferentJobsImplyDifferentArrivalTimes.
In this section we prove a few properties regarding task arrivals
in context of the sporadic task model.
Consider sporadic tasks with an offset ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{SporadicModel Task}.
Context `{TaskMaxInterArrival Task}.
Context `{TaskOffset Task}.
Context `{SporadicModel Task}.
Context `{TaskMaxInterArrival Task}.
... and any type of jobs associated with these tasks.
Consider any unique arrival sequence with consistent arrivals, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
... and any sporadic task tsk to be analyzed.
Assume all tasks have valid minimum inter-arrival times, valid offsets, and respect the
sporadic task model.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Consider any two jobs from the arrival sequence that stem
from task tsk.
Variable j1 j2 : Job.
Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
We show that a sporadic task with valid min inter-arrival time cannot
have more than one job arriving at any time.
Lemma size_task_arrivals_at_leq_one:
(∃ j,
size (task_arrivals_at_job_arrival arr_seq j) > 1 ∧
respects_sporadic_task_model arr_seq (job_task j) ∧
valid_task_min_inter_arrival_time (job_task j)) →
False.
(∃ j,
size (task_arrivals_at_job_arrival arr_seq j) > 1 ∧
respects_sporadic_task_model arr_seq (job_task j) ∧
valid_task_min_inter_arrival_time (job_task j)) →
False.
We show that no jobs of the task tsk other than j1 arrive at
the same time as j1, and thus the task arrivals at job arrival j1
consists only of job j1.
We show that no jobs of the task tsk other than j1 arrive at
the same time as j1, and thus the task arrivals at job arrival j1
consists only of job j1.
We show that a job j1 is the first job that arrives
in task arrivals at job_arrival j1 by showing that the
index of job j1 in task_arrivals_at_job_arrival arr_seq j1 is 0.
We observe that for any job j the arrival time of prev_job j is
strictly less than the arrival time of j in context of periodic tasks.
Lemma prev_job_arr_lt:
job_index arr_seq j1 > 0 →
job_arrival (prev_job arr_seq j1) < job_arrival j1.
job_index arr_seq j1 > 0 →
job_arrival (prev_job arr_seq j1) < job_arrival j1.
We show that task arrivals at job_arrival j1 is the
same as task arrivals that arrive between job_arrival j1
and job_arrival j1 + 1.
Lemma task_arrivals_at_as_task_arrivals_between:
task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1.
task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1.
We show that the task arrivals up to the previous job j1 concatenated with
the sequence ::j1 (the sequence containing only the job j1) is same as
task arrivals up to job_arrival j1.