Library rt.restructuring.model.schedule.tdma.tdma
From rt.restructuring.behavior Require Export schedule.ideal.
From rt.restructuring.model Require Export task.
From rt.util Require Export seqset list.
From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
From rt.restructuring.model Require Export task.
From rt.util Require Export seqset list.
From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
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.