define preemptive work-conserving and priority-based schedules

Add model definitions for work-conserving and priority-based preemptive schedules.

restructuring/model/schedule/priority_based/preemptive.v

+From rt.restructuring.behavior Require Export schedule arrival_sequence.
+From rt.restructuring.model Require Export priorities.
+
+(* We now define what it means for a schedule to respect a priority *)
+(* We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same
+   and can be used through the conversions *)
+Section Priority.
+  Context {Job: JobType} {Task: TaskType}.
+  Context `{JobCost Job} `{JobArrival Job}.
+
+  Context `{JLDP_policy Job}.
+
+  Variable arr_seq : arrival_sequence Job.
+
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+  Variable sched : schedule PState.
+
+  Definition respects_preemptive_priorities :=
+    forall j j_hp t,
+      arrives_in arr_seq j ->
+      backlogged sched j t ->
+      scheduled_at sched j_hp t ->
+      hep_job_at t j_hp j.
+End Priority.

restructuring/model/schedule/priority_based/priorities.v

+From rt.restructuring.model Require Export task.
+From rt.util Require Export list.
+From mathcomp Require Export seq.
+
+(* Definitions of FP, JLFP and JLDP priority relations. *)
+
+(* In the following, "hep" means "higher or equal priority". We define an FP
+   policy as a relation among tasks, ... *)
+Class FP_policy (Task: TaskType) := hep_task : rel Task.
+
+(* ... a JLFP policy as a relation among jobs, a ... *)
+Class JLFP_policy (Job: JobType) := hep_job : rel Job.
+
+(* ... a JLDP policy as a relation among jobs that may vary over time. *)
+Class JLDP_policy (Job: JobType) := hep_job_at : instant -> rel Job.
+
+(* Since FP policies are also JLFP and JLDP policies, we define
+   conversions that express the generalization. *)
+Instance FP_to_JLFP (Job: JobType) (Task: TaskType)
+         `{JobTask Job Task} `{FP_policy Task} : JLFP_policy Job :=
+  fun j1 j2 => hep_task (job_task j1) (job_task j2).
+
+Instance JLFP_to_JLDP (Job: JobType) `{JLFP_policy Job} : JLDP_policy Job :=
+  fun _ j1 j2 => hep_job j1 j2.
+
+Section Priorities.
+  Context {Job: eqType}.
+
+  Section JLDP.
+    (* Consider any JLDP policy. *)
+    Context `{JLDP_policy Job}.
+
+    (* We define common properties of the policy. Note that these definitions
+       can also be used for JLFP and FP policies *)
+    Definition reflexive_priorities := forall t, reflexive (hep_job_at t).
+
+    Definition transitive_priorities := forall t, transitive (hep_job_at t).
+
+    Definition total_priorities := forall t, total (hep_job_at t).
+
+  End JLDP.
+
+  Section FP.
+    (* Consider any FP policy. *)
+    Context {Task : TaskType}.
+    Context `{FP_policy Task}.
+
+    (* We define whether the policy is antisymmetric over a taskset ts. *)
+    Definition antisymmetric_over_taskset (ts : seq Task) :=
+      antisymmetric_over_list hep_task ts.
+  End FP.
+End Priorities.
+

restructuring/model/schedule/tdma_facts.v → restructuring/model/schedule/tdma/tdma_facts.v

-From rt.restructuring.model Require Export schedule.tdma.
+From rt.restructuring.model Require Export tdma.
 From rt.util Require Import all.
 
 (** In this section, we define the properties of TDMA and prove some basic lemmas. *)

restructuring/model/schedule/work_conserving.v

+From rt.restructuring.behavior Require Export schedule arrival_sequence.
+
+(* In this file, we introduce a restrictive definition of work conserving
+   uniprocessor schedules. The definition is restrictive because it does not
+   allow for effects such as jitter or self-suspensions that affect whether a
+   job can be scheduled at a given point in time. A more general notion of work
+   conservation that is "readiness-aware", as well as a variant that covers
+   global scheduling, is TBD. *)
+
+Section WorkConserving.
+  (* Consider any type of job associated with any type of tasks... *)
+  Context {Job: JobType}.
+
+  (* ... with arrival times and costs ... *)
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (* ... and any kind of processor state model. *)
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Given an arrival sequence and a schedule ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Variable sched: schedule PState.
+
+  (* We say that a scheduler is work-conserving iff whenever a job j
+     is backlogged, the processor is always busy with another job. *)
+  Definition work_conserving :=
+    forall j t,
+      arrives_in arr_seq j ->
+      backlogged sched j t ->
+      exists j_other, scheduled_at sched j_other t.
+
+End WorkConserving.