Library rt.restructuring.model.schedule.tdma.tdma
In this section, we define the TDMA policy.
Section TDMAPolicy.
(* The TDMA policy is based on two properties.
(1) Each task has a fixed, reserved time slot for execution;
(2) These time slots are ordered in sequence to form a TDMA cycle, which repeats along the timeline.
An example of TDMA schedule is illustrated in the following.
______________________________
| s1 | s2 |s3| s1 | s2 |s3|...
--------------------------------------------->
0 t
*)
Variable Task: eqType.
(* With each task, we associate the duration of the corresponding TDMA slot. *)
Definition TDMA_slot := Task → duration.
(* 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) *)
Definition TDMA_slot_order := rel Task.
End TDMAPolicy.
Class TDMAPolicy (T : TaskType) :=
{ task_time_slot : TDMA_slot T;
slot_order : TDMA_slot_order T }.
(* First, we define the properties of a valid TDMA policy. *)
Section ValidTDMAPolicy.
Context {Task : eqType}.
(* Consider any task set ts... *)
Variable ts : {set Task}.
(* ...and a TDMA policy. *)
Context `{TDMAPolicy Task}.
(* Time slot order must be transitive... *)
Definition transitive_slot_order := transitive slot_order.
(* ..., totally ordered over the task set... *)
Definition total_slot_order :=
total_over_list slot_order ts.
(* ... and antisymmetric over task set. *)
Definition antisymmetric_slot_order :=
antisymmetric_over_list slot_order ts.
(* 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.
(* The TDMA policy is based on two properties.
(1) Each task has a fixed, reserved time slot for execution;
(2) These time slots are ordered in sequence to form a TDMA cycle, which repeats along the timeline.
An example of TDMA schedule is illustrated in the following.
______________________________
| s1 | s2 |s3| s1 | s2 |s3|...
--------------------------------------------->
0 t
*)
Variable Task: eqType.
(* With each task, we associate the duration of the corresponding TDMA slot. *)
Definition TDMA_slot := Task → duration.
(* 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) *)
Definition TDMA_slot_order := rel Task.
End TDMAPolicy.
Class TDMAPolicy (T : TaskType) :=
{ task_time_slot : TDMA_slot T;
slot_order : TDMA_slot_order T }.
(* First, we define the properties of a valid TDMA policy. *)
Section ValidTDMAPolicy.
Context {Task : eqType}.
(* Consider any task set ts... *)
Variable ts : {set Task}.
(* ...and a TDMA policy. *)
Context `{TDMAPolicy Task}.
(* Time slot order must be transitive... *)
Definition transitive_slot_order := transitive slot_order.
(* ..., totally ordered over the task set... *)
Definition total_slot_order :=
total_over_list slot_order ts.
(* ... and antisymmetric over task set. *)
Definition antisymmetric_slot_order :=
antisymmetric_over_list slot_order ts.
(* 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.
In this section, we define functions on a TDMA policy
Section TDMADefinitions.
Context {Task : eqType}.
(* Consider any task set ts... *)
Variable ts : {set Task}.
(* ...and a TDMA policy. *)
Context `{TDMAPolicy Task}.
(* We define the TDMA cycle as the sum of all the tasks' time slots *)
Definition TDMA_cycle:=
\sum_(tsk <- ts) task_time_slot tsk.
(* 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.
(* 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.
Section TDMASchedule.
Context {Task : TaskType} {Job : JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobReady Job (option Job)} `{JobTask Job Task}.
(* Consider any job arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
(* ..., any uniprocessor ideal schedule ... *)
Variable sched : schedule (option Job).
(* ... and any sporadic task set. *)
Variable ts: {set Task}.
Context `{TDMAPolicy Task}.
(* In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time t. *)
Definition job_in_time_slot (job:Job) (t:instant):=
task_in_time_slot ts (job_task job) 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... *)
Definition sched_implies_in_slot j t:=
scheduled_at sched j t → job_in_time_slot j t.
(* 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.
Context {Task : eqType}.
(* Consider any task set ts... *)
Variable ts : {set Task}.
(* ...and a TDMA policy. *)
Context `{TDMAPolicy Task}.
(* We define the TDMA cycle as the sum of all the tasks' time slots *)
Definition TDMA_cycle:=
\sum_(tsk <- ts) task_time_slot tsk.
(* 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.
(* 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.
Section TDMASchedule.
Context {Task : TaskType} {Job : JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobReady Job (option Job)} `{JobTask Job Task}.
(* Consider any job arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
(* ..., any uniprocessor ideal schedule ... *)
Variable sched : schedule (option Job).
(* ... and any sporadic task set. *)
Variable ts: {set Task}.
Context `{TDMAPolicy Task}.
(* In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time t. *)
Definition job_in_time_slot (job:Job) (t:instant):=
task_in_time_slot ts (job_task job) 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... *)
Definition sched_implies_in_slot j t:=
scheduled_at sched j t → job_in_time_slot j t.
(* 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.