port definitions for arrival curves

This is a port (+additions) of the definitions and semantics for arrival curves (model/arrival/curves.v). As a prerequisite, this includes definitions about activations of a task (model/task_arrivals.v).

Two additional definitions which were not found in the original library but will be useful to us in the future:

* in schedule.v : completes_at
* in task_arrivals.v : arrivals_come_from_taskset

restructuring/README.md

 This is a work-in-progress directory and part of the larger Prosa restructuring effort. As parts in Prosa are changed to comply with the “new style”, they are placed here.
 
-The behavior directory collects all definitions and basic properties of system behavior (i.e., trace-based semantics).
+The behavior directory collects all definitions and basic properties of system behavior (i.e., trace-based semantics). Changes here are sensitive since this is the part of the library that everyone is going to use, so changes here should be discussed early.
 
-The model directory collects all definitions and basic properties of system models (e.g., sporadic tasks, arrival curves, scheduling policies etc.)
+The model directory collects all definitions and basic properties of system models (e.g., sporadic tasks, arrival curves, scheduling policies etc.). One should port and validate a new system model before the corresponding analysis.
+
+The analysis directory collects all definitions of system properties (e.g., schedulability, response time etc.), analysis results and proofs. The stucture of this directory is not clear yet.
 
 # Remarks
 

restructuring/behavior/arrival_sequence.v

@@ -23,15 +23,15 @@ Section JobProperties.
   Variable arr_seq: arrival_sequence Job.
 
   (* First, we define the sequence of jobs arriving at time t. *)
-  Definition jobs_arriving_at (t : instant) := arr_seq t.
+  Definition arrivals_at (t : instant) := arr_seq t.
 
   (* Next, we say that job j arrives at a given time t iff it belongs to the
        corresponding sequence. *)
-  Definition arrives_at (j : Job) (t : instant) := j \in jobs_arriving_at t.
+  Definition arrives_at (j : Job) (t : instant) := j \in arrivals_at t.
 
   (* Similarly, we define whether job j arrives at some (unknown) time t, i.e.,
        whether it belongs to the arrival sequence. *)
-  Definition arrives_in (j : Job) := exists t, j \in jobs_arriving_at t.
+  Definition arrives_in (j : Job) := exists t, j \in arrivals_at t.
 
 End JobProperties.
 
@@ -53,7 +53,7 @@ Section ValidArrivalSequence.
 
   (* We say that the arrival sequence is a set iff it doesn't contain duplicate
      jobs at any given time. *)
-  Definition arrival_sequence_uniq := forall t, uniq (jobs_arriving_at arr_seq t).
+  Definition arrival_sequence_uniq := forall t, uniq (arrivals_at arr_seq t).
 
   (* We say that the arrival sequence is valid iff it is a set and arrival times
      are consistent *)
@@ -99,13 +99,13 @@ Section ArrivalSequencePrefix.
 
   (* By concatenation, we construct the list of jobs that arrived in the
      interval [t1, t2). *)
-  Definition jobs_arrived_between (t1 t2 : instant) :=
-    \cat_(t1 <= t < t2) jobs_arriving_at arr_seq t.
+  Definition arrivals_between (t1 t2 : instant) :=
+    \cat_(t1 <= t < t2) arrivals_at arr_seq t.
 
   (* Based on that, we define the list of jobs that arrived up to time t, ...*)
-  Definition jobs_arrived_up_to (t : instant) := jobs_arrived_between 0 t.+1.
+  Definition arrivals_up_to (t : instant) := arrivals_between 0 t.+1.
 
   (* ...and the list of jobs that arrived strictly before time t. *)
-  Definition jobs_arrived_before (t : instant) := jobs_arrived_between 0 t.
+  Definition arrivals_before (t : instant) := arrivals_between 0 t.
 
 End ArrivalSequencePrefix.

restructuring/behavior/facts/arrivals.v

@@ -11,17 +11,6 @@ Section ArrivalSequencePrefix.
   (* Consider any job arrival sequence. *)
   Variable arr_seq: arrival_sequence Job.
 
-  (* By concatenation, we construct the list of jobs that arrived in the
-     interval [t1, t2). *)
-  Definition jobs_arrived_between (t1 t2 : instant) :=
-    \cat_(t1 <= t < t2) jobs_arriving_at arr_seq t.
-
-  (* Based on that, we define the list of jobs that arrived up to time t, ...*)
-  Definition jobs_arrived_up_to (t : instant) := jobs_arrived_between 0 t.+1.
-
-  (* ...and the list of jobs that arrived strictly before time t. *)
-  Definition jobs_arrived_before (t : instant) := jobs_arrived_between 0 t.
-
   (* In this section, we prove some lemmas about arrival sequence prefixes. *)
   Section Lemmas.
 
@@ -30,42 +19,42 @@ Section ArrivalSequencePrefix.
 
       (* First, we show that the set of arriving jobs can be split
          into disjoint intervals. *)
-      Lemma job_arrived_between_cat:
+      Lemma arrivals_between_cat:
         forall t1 t t2,
           t1 <= t ->
           t <= t2 ->
-          jobs_arrived_between t1 t2 = jobs_arrived_between t1 t ++ jobs_arrived_between t t2.
+          arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
       Proof.
-        unfold jobs_arrived_between; intros t1 t t2 GE LE.
+        unfold arrivals_between; intros t1 t t2 GE LE.
           by rewrite (@big_cat_nat _ _ _ t).
       Qed.
 
       (* Second, the same observation applies to membership in the set of
          arrived jobs. *)
-      Lemma jobs_arrived_between_mem_cat:
+      Lemma arrivals_between_mem_cat:
         forall j t1 t t2,
           t1 <= t ->
           t <= t2 ->
-          j \in jobs_arrived_between t1 t2 =
-                (j \in jobs_arrived_between t1 t ++ jobs_arrived_between t t2).
+          j \in arrivals_between arr_seq t1 t2 =
+                (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
       Proof.
-          by intros j t1 t t2 GE LE; rewrite (job_arrived_between_cat _ t).
+          by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
       Qed.
 
       (* Third, we observe that we can grow the considered interval without
          "losing" any arrived jobs, i.e., membership in the set of arrived jobs
          is monotonic. *)
-      Lemma jobs_arrived_between_sub:
+      Lemma arrivals_between_sub:
         forall j t1 t1' t2 t2',
           t1' <= t1 ->
           t2 <= t2' ->
-          j \in jobs_arrived_between t1 t2 ->
-                j \in jobs_arrived_between t1' t2'.
+          j \in arrivals_between arr_seq t1 t2 ->
+          j \in arrivals_between arr_seq t1' t2'.
       Proof.
         intros j t1 t1' t2 t2' GE1 LE2 IN.
         move: (leq_total t1 t2) => /orP [BEFORE | AFTER];
-                                   last by rewrite /jobs_arrived_between big_geq // in IN.
-        rewrite /jobs_arrived_between.
+                                   last by rewrite /arrivals_between big_geq // in IN.
+        rewrite /arrivals_between.
         rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
         rewrite mem_cat; apply/orP; right.
         rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done].
@@ -85,8 +74,8 @@ Section ArrivalSequencePrefix.
          (jobs_arrived_before t), then it arrives in the arrival sequence. *)
       Lemma in_arrivals_implies_arrived:
         forall j t1 t2,
-          j \in jobs_arrived_between t1 t2 ->
-                arrives_in arr_seq j.
+          j \in arrivals_between arr_seq t1 t2 ->
+          arrives_in arr_seq j.
       Proof.
         rename H_consistent_arrival_times into CONS.
         intros j t1 t2 IN.
@@ -100,7 +89,7 @@ Section ArrivalSequencePrefix.
          t2. *)
       Lemma in_arrivals_implies_arrived_between:
         forall j t1 t2,
-          j \in jobs_arrived_between t1 t2 ->
+          j \in arrivals_between arr_seq t1 t2 ->
                 arrived_between j t1 t2.
       Proof.
         rename H_consistent_arrival_times into CONS.
@@ -114,11 +103,10 @@ Section ArrivalSequencePrefix.
            then it indeed arrives before time t. *)
       Lemma in_arrivals_implies_arrived_before:
         forall j t,
-          j \in jobs_arrived_before t ->
+          j \in arrivals_before arr_seq t ->
                 arrived_before j t.
       Proof.
         intros j t IN.
-        Fail suff: arrived_between j 0 t by rewrite /arrived_between /=.
         have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
           by rewrite /arrived_between /=.
       Qed.
@@ -129,7 +117,7 @@ Section ArrivalSequencePrefix.
         forall j t1 t2,
           arrives_in arr_seq j ->
           arrived_between j t1 t2 ->
-          j \in jobs_arrived_between t1 t2.
+          j \in arrivals_between arr_seq t1 t2.
       Proof.
         rename H_consistent_arrival_times into CONS.
         move => j t1 t2 [a_j ARRj] BEFORE.
@@ -141,10 +129,10 @@ Section ArrivalSequencePrefix.
          jobs, the same applies for any of its prefixes. *)
       Lemma arrivals_uniq :
         arrival_sequence_uniq arr_seq ->
-        forall t1 t2, uniq (jobs_arrived_between t1 t2).
+        forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
       Proof.
         rename H_consistent_arrival_times into CONS.
-        unfold jobs_arrived_up_to; intros SET t1 t2.
+        unfold arrivals_up_to; intros SET t1 t2.
         apply bigcat_nat_uniq; first by done.
         intros x t t' IN1 IN2.
           by apply CONS in IN1; apply CONS in IN2; subst.

restructuring/behavior/schedule.v

@@ -52,6 +52,10 @@ Section Schedule.
            service in the interval [0, t). *)
   Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
 
+  (* We say that job j completes at time t if it has completed by time t but
+     not by time t - 1 *)
+  Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
+
   (* We say that R is a response time bound of a job j if j has completed
      by R units after its arrival *)
   Definition job_response_time_bound (j : Job) (R : duration) :=

restructuring/model/arrival/arrival_curves.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Export arrival_sequence.
+From rt.restructuring.model Require Export task_arrivals.
+
+(* In this section, we define the notion of arrival curves, which
+   can be used to reason about the frequency of job arrivals. *)
+Section ArrivalCurves.
+
+  Context {Task: TaskType}.
+  Context {Job: JobType}.
+  Context `{JobTask Job Task}.
+
+  (* Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (* First, we define what constitutes an arrival bound for a task. *)
+  Section ArrivalCurves.
+
+    (* We say that num_arrivals is a valid arrival curve for task tsk iff *)
+    (* [num_arrivals] is a monotonic function that equals 0 for the empty *)
+    (* interval delta = 0. *)
+    Definition valid_arrival_curve (tsk: Task) (num_arrivals: duration -> nat) :=
+      num_arrivals 0 = 0 /\
+      monotone num_arrivals leq.
+
+    (* We say that max_arrivals is an upper arrival bound for tsk iff, for any interval [t1, t2),
+     [max_arrivals (t2 - t1)] bounds the number of jobs of tsk that arrive in that interval. *)
+    Definition respects_max_arrivals (tsk: Task) (max_arrivals: duration -> nat) :=
+      forall (t1 t2: instant),
+        t1 <= t2 ->
+        size (task_arrivals_between arr_seq tsk t1 t2) <= max_arrivals (t2 - t1).
+
+    (* We define in the same way lower arrival bounds *)
+    Definition respects_min_arrivals (tsk: Task) (min_arrivals: duration -> nat) :=
+      forall (t1 t2: instant),
+        t1 <= t2 ->
+        min_arrivals (t2 - t1) <= size (task_arrivals_between arr_seq tsk t1 t2).
+
+  End ArrivalCurves.
+
+  Section SeparationBound.
+
+    (* Then, we say that min_separation is a lower separation bound iff, for any number of jobs
+       of tsk, min_separation lower-bounds the minimum interval length in which that number
+       of jobs can be spawned. *)
+    Definition respects_min_separation tsk (min_separation: nat -> duration) :=
+      forall t1 t2,
+          t1 <= t2 ->
+          min_separation (size (task_arrivals_between arr_seq tsk t1 t2)) <= t2 - t1.
+
+    (* We define in the same way upper separation bounds *)
+    Definition respects_max_separation tsk (max_separation: nat -> duration):=
+      forall t1 t2,
+        t1 <= t2 ->
+        t2 - t1 <= max_separation (size (task_arrivals_between arr_seq tsk t1 t2)).
+
+  End SeparationBound.
+
+End ArrivalCurves.
+
+(* We define generic classes for arrival curves  *)
+Class MaxArrivals (Task: TaskType) := max_arrivals: Task -> duration -> nat.
+
+Class MinArrivals (Task: TaskType) := min_arrivals: Task -> duration -> nat.
+
+Class MaxSeparation (Task: TaskType) := max_separation: Task -> nat -> duration.
+
+Class MinSeparation (Task: TaskType) := min_separation: Task -> nat -> duration.
+
+Section ArrivalCurvesModel.
+
+  Context {Task: TaskType} {Job: JobType}.
+  Context `{JobTask Job Task}.
+
+  Context `{MaxArrivals Task} `{MinArrivals Task} `{MaxSeparation Task} `{MinSeparation Task}.
+
+  Variable ts: seq Task.
+
+  (* We say that arrivals is a valid arrival curve for a taskset if it is valid for any task
+     in the taskset *)
+  Definition valid_taskset_arrival_curve (arrivals : Task -> duration -> nat) :=
+    forall tsk,
+      tsk \in ts ->
+      valid_arrival_curve tsk (arrivals tsk).
+
+  Variable arr_seq: arrival_sequence Job.
+
+  (* We say that max_arrivals is an arrival bound for taskset ts *)
+  (* iff max_arrival is an arrival bound for any task from ts. *)
+  Definition taskset_respects_max_arrivals :=
+    forall (tsk: Task), tsk \in ts -> respects_max_arrivals arr_seq tsk (max_arrivals tsk).
+
+  Definition taskset_respects_min_arrivals :=
+    forall (tsk: Task), tsk \in ts -> respects_min_arrivals arr_seq tsk (min_arrivals tsk).
+
+  Definition taskset_respects_max_separation :=
+    forall (tsk: Task), tsk \in ts -> respects_max_separation arr_seq tsk (max_separation tsk).
+
+  Definition taskset_respects_min_separation :=
+    forall (tsk: Task), tsk \in ts -> respects_min_separation arr_seq tsk (min_separation tsk).
+
+End ArrivalCurvesModel.
\ No newline at end of file

restructuring/model/arrival/sporadic.v

@@ -2,43 +2,54 @@ From rt.restructuring.behavior Require Export arrival_sequence.
 From rt.restructuring.model Require Export task.
 
 Section TaskMinInterArrivalTime.
-  Context {T : TaskType}.
+  Context {Task : TaskType}.
 
   Variable (task_min_inter_arrival_time : duration).
 
   Definition valid_task_min_inter_arrival_time :=
     task_min_inter_arrival_time > 0.
+
+  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
+
+  Variable arr_seq : arrival_sequence Job.
+
+  Definition respects_sporadic_task_model (tsk : Task) (d : duration) :=
+    forall (j j': Job),
+      j <> j' -> (* Given two different jobs j and j' ... *)
+      arrives_in arr_seq j -> (* ...that belong to the arrival sequence... *)
+      arrives_in arr_seq j' ->
+      job_task j = tsk ->
+      job_task j' = tsk -> (* ... and that are spawned by the same task, ... *)
+      job_arrival j <= job_arrival j' -> (* ... if the arrival of j precedes the arrival of j' ...,  *)
+      (* then the arrival of j and the arrival of j' are separated by at least one period. *)
+      job_arrival j' >= job_arrival j + d.
+
 End TaskMinInterArrivalTime.
 
 (* Definition of a generic type of parameter for task
    minimum inter arrival times *)
 
-Class SporadicModel (T : TaskType) :=
-  task_min_inter_arrival_time : T -> duration.
+Class SporadicModel (Task : TaskType) :=
+  task_min_inter_arrival_time : Task -> duration.
 
 Section SporadicModel.
-  Context {T : TaskType} `{SporadicModel T}.
+  Context {Task : TaskType} `{SporadicModel Task}.
 
-  Variable ts : seq T.
+  Variable ts : seq Task.
 
   Definition valid_taskset_min_inter_arrival_times :=
-    forall tsk : T,
+    forall tsk : Task,
       tsk \in ts ->
       task_min_inter_arrival_time tsk > 0.
 
-  Context {J : JobType} `{JobTask J T} `{JobArrival J}.
+  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
 
-  Variable arr_seq : arrival_sequence J.
+  Variable arr_seq : arrival_sequence Job.
 
   (* Then, we define the sporadic task model as follows.*)
-  Definition respects_sporadic_task_model :=
-    forall (j j': J),
-      j <> j' -> (* Given two different jobs j and j' ... *)
-      arrives_in arr_seq j -> (* ...that belong to the arrival sequence... *)
-      arrives_in arr_seq j' ->
-      job_task j = job_task j' -> (* ... and that are spawned by the same task, ... *)
-      job_arrival j <= job_arrival j' -> (* ... if the arrival of j precedes the arrival of j' ...,  *)
-      (* then the arrival of j and the arrival of j' are separated by at least one period. *)
-      job_arrival j' >= job_arrival j + task_min_inter_arrival_time (job_task j).
+  Definition taskset_respects_sporadic_task_model :=
+    forall tsk,
+      tsk \in ts ->
+      respects_sporadic_task_model arr_seq tsk (task_min_inter_arrival_time tsk).
 
 End SporadicModel.

restructuring/model/task_arrivals.v

+From rt.restructuring.behavior Require Export arrival_sequence.
+From rt.restructuring.model Require Export task.
+
+(* In this file we provide basic definitions related to tasks on arrival sequences *)
+Section TaskArrivals.
+  Context {Job : JobType} {Task : TaskType}.
+
+  Context `{JobTask Job Task}.
+
+  (* Consider any job arrival sequence, *)
+  Variable arr_seq: arrival_sequence Job.
+
+  Section Definitions.
+    (* And a given task *)
+    Variable tsk : Task.
+
+    (* We define the sequence of jobs of tsk arriving at time t *)
+    Definition task_arrivals_at (t : instant) : seq Job :=
+      [seq j <- arrivals_at arr_seq t | job_task j == tsk].
+
+    (* By concatenation, we construct the list of jobs of tsk that arrived in the
+     interval [t1, t2). *)
+    Definition task_arrivals_between (t1 t2 : instant) :=
+      [seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
+
+    (* Based on that, we define the list of jobs of tsk that arrived up to time t, ...*)
+    Definition task_arrivals_up_to (t : instant) := task_arrivals_between 0 t.+1.
+
+    (* ...and the list of jobs of tsk that arrived strictly before time t. *)
+    Definition task_arrivals_before (t : instant) := task_arrivals_between 0 t.
+  End Definitions.
+
+  (* We define a predicate for arrival sequences for which jobs come from a taskset *)
+  Definition arrivals_come_from_taskset (ts : seq Task) :=
+    forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+End TaskArrivals.
\ No newline at end of file