Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
From mathcomp Require Import div.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Require Export prosa.util.seqset. Require Export prosa.util.rel. (** Throughout this file, we assume ideal uniprocessor schedules. *) Require prosa.model.processor.ideal. (** * 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... *) 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 := forall 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. (** ** 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. *) 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. (** ** TDMA Schedule Validity *) 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... *) Variable arr_seq : arrival_sequence Job. (** ..., any uniprocessor ideal schedule ... *) Variable sched : schedule (ideal.processor_state 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 \/ exists 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:= forall (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.