Library prosa.model.schedule.tdma

Require Export prosa.model.task.concept.
Require Export prosa.util.seqset.
Require Export prosa.util.rel.

TDMA Scheduling

The TDMA scheduling 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

Task Parameter for TDMA Scheduling

We define the TDMA policy as follows.
Section TDMAPolicy.

  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.

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

TDMA Policy Validity

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...
..., totally ordered over the task set...
  Definition total_slot_order :=
    total_over_list slot_order ts.

... and antisymmetric over task set.
A valid time slot must be positive

TDMA Cycles, Sots, and Offsets

In this section, we define key TDMA concepts.
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.
The following function tests whether a task is in its time slot at instant t.

TDMA Schedule Validity

Section TDMASchedule.

  Context {Task : TaskType} {Job : JobType}.

  Context {PState : ProcessorState Job}.
  Context {ja : JobArrival Job} {jc : JobCost Job}.
  Context {jr : @JobReady Job PState jc ja} `{JobTask Job Task}.

Consider any job arrival sequence...
  Variable arr_seq : arrival_sequence Job.

..., any schedule ...
  Variable sched : schedule PState.

... 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...
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.