Library prosa.model.schedule.tdma
From mathcomp Require Import div.
Require Export prosa.model.task.concept.
Require Export prosa.util.seqset.
Require Export prosa.util.rel.
Require Export prosa.model.task.concept.
Require Export prosa.util.seqset.
Require Export prosa.util.rel.
Throughout this file, we assume ideal uniprocessor schedules.
TDMA Scheduling
_______________________________
| s1 | s2 |s3| s1 | s2 |s3|...
--------------------------------------------->
0 t
Task Parameter for TDMA Scheduling
With each task, we associate the duration of the corresponding TDMA slot.
Moreover, within each TDMA cycle, task slots are ordered according to
some relation (i.e, slot_order slot1 slot2 means that slot1 comes
before slot2 in a TDMA cycle).
We introduce slots and the slot order as task parameters.
Class TDMAPolicy (T : TaskType) :=
{
task_time_slot : TDMA_slot T;
slot_order : TDMA_slot_order T
}.
{
task_time_slot : TDMA_slot T;
slot_order : TDMA_slot_order T
}.
Consider any task set ts...
...and a TDMA policy.
Time slot order must be transitive...
..., totally ordered over the task set...
... and antisymmetric over task set.
A valid time slot must be positive
Definition valid_time_slot :=
∀ tsk, tsk \in ts → task_time_slot tsk > 0.
Definition valid_TDMAPolicy :=
transitive_slot_order ∧ total_slot_order ∧ antisymmetric_slot_order ∧ valid_time_slot.
End ValidTDMAPolicy.
∀ tsk, tsk \in ts → task_time_slot tsk > 0.
Definition valid_TDMAPolicy :=
transitive_slot_order ∧ total_slot_order ∧ antisymmetric_slot_order ∧ valid_time_slot.
End ValidTDMAPolicy.
Consider any task set ts...
...and a TDMA policy.
We define the TDMA cycle as the sum of all the tasks' time slots
We define the function returning the slot offset for each task: i.e., the
distance between the start of the TDMA cycle and the start of the task
time slot.
Definition task_slot_offset (tsk : Task) :=
\sum_(prev_task <- ts | slot_order prev_task tsk && (prev_task != tsk)) task_time_slot prev_task.
\sum_(prev_task <- ts | slot_order prev_task tsk && (prev_task != tsk)) task_time_slot prev_task.
The following function tests whether a task is in its time slot at
instant t.
Definition task_in_time_slot (tsk : Task) (t:instant):=
((t + TDMA_cycle - (task_slot_offset tsk)%% TDMA_cycle) %% TDMA_cycle)
< (task_time_slot tsk).
End TDMADefinitions.
((t + TDMA_cycle - (task_slot_offset tsk)%% TDMA_cycle) %% TDMA_cycle)
< (task_time_slot tsk).
End TDMADefinitions.
Section TDMASchedule.
Context {Task : TaskType} {Job : JobType}.
Context {ja : JobArrival Job} {jc : JobCost Job}.
Context {jr : JobReady Job (ideal.processor_state Job)} `{JobTask Job Task}.
Consider any job arrival sequence...
..., any uniprocessor ideal schedule ...
... and any sporadic task set.
In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time t.
We say that a TDMA policy is respected by the schedule iff
1. when a job is scheduled at time t, then the corresponding task
is also in its own time slot...
2. when a job is backlogged at time t, the corresponding task
isn't in its own time slot or another previous job of the same task is scheduled
Definition backlogged_implies_not_in_slot_or_other_job_sched j t:=
backlogged sched j t →
¬ job_in_time_slot j t ∨
∃ j_other, arrives_in arr_seq j_other∧
job_arrival j_other < job_arrival j∧
job_task j = job_task j_other∧
scheduled_at sched j_other t.
Definition respects_TDMA_policy:=
∀ (j:Job) (t:instant),
arrives_in arr_seq j →
sched_implies_in_slot j t ∧
backlogged_implies_not_in_slot_or_other_job_sched j t.
End TDMASchedule.
backlogged sched j t →
¬ job_in_time_slot j t ∨
∃ j_other, arrives_in arr_seq j_other∧
job_arrival j_other < job_arrival j∧
job_task j = job_task j_other∧
scheduled_at sched j_other t.
Definition respects_TDMA_policy:=
∀ (j:Job) (t:instant),
arrives_in arr_seq j →
sched_implies_in_slot j t ∧
backlogged_implies_not_in_slot_or_other_job_sched j t.
End TDMASchedule.