behavior/README.md

-The behavior directory/module collects all definitions and theories about system behavior (i.e., trace-based semantics).
-
-Any aspects related to system *modeling* (e.g., sporadic tasks, arrival curves, etc.) do *not* belong here and should go into the *model* directory/module instead. 
-
-This is a work-in-progress directory and part of the larger Prosa restructuring effort. As parts in Prosa a changed to comply with the “new style”, they are placed here. 
-
-

behavior/facts/all.v

-Require Export rt.behavior.facts.service.
-Require Export rt.behavior.facts.completion.
-Require Export rt.behavior.facts.ideal_schedule.
-Require Export rt.behavior.facts.sequential.
-Require Export rt.behavior.facts.arrivals.

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 model directory collects all definitions and basic properties of system models (e.g., sporadic tasks, arrival curves, scheduling policies etc.)
+
+# Remarks
+
+We have chosen and applied some renaming rules for sections and definitions, cf. arrival_sequence.v and sporadic.v. Basically, we try to consistenly use `Valid*` , `*Properties` for section names about a concept `*` and `respects_*`, `valid_*` for definitions about a system model `*`.

behavior/arrival/arrival_sequence.v → restructuring/behavior/arrival/arrival_sequence.v

 From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
-From rt.behavior Require Export time job.
+From rt.restructuring.behavior Require Export time job.
 From rt.util Require Import notation.
 
 (* Definitions and properties of job arrival sequences. *)
 
 (* We begin by defining a job arrival sequence. *)
-Section ArrivalSequenceDef.
+Section ArrivalSequence.
 
   (* Given any job type with decidable equality, ... *)
   Variable Job: JobType.
@@ -13,7 +13,7 @@ Section ArrivalSequenceDef.
   (* ..., an arrival sequence is a mapping from any time to a (finite) sequence of jobs. *)
   Definition arrival_sequence := instant -> seq Job.
 
-End ArrivalSequenceDef.
+End ArrivalSequence.
 
 (* Next, we define properties of jobs in a given arrival sequence. *)
 Section JobProperties.
@@ -39,8 +39,8 @@ End JobProperties.
 
 Class JobArrival (J : JobType) := job_arrival : J -> instant.
 
-(* Next, we define properties of a valid arrival sequence. *)
-Section ArrivalSequenceProperties.
+(* Next, we define valid arrival sequences. *)
+Section ValidArrivalSequence.
 
   (* Assume that job arrival times are known. *)
   Context {Job: JobType}.
@@ -51,18 +51,23 @@ Section ArrivalSequenceProperties.
 
   (* We say that arrival times are consistent if any job that arrives in the
      sequence has the corresponding arrival time. *)
-  Definition arrival_times_are_consistent :=
+  Definition consistent_arrival_times :=
     forall j t,
       arrives_at arr_seq j t -> job_arrival j = t.
 
   (* We say that the arrival sequence is a set iff it doesn't contain duplicate
      jobs at any given time. *)
-  Definition arrival_sequence_is_a_set := forall t, uniq (jobs_arriving_at arr_seq t).
+  Definition arrival_sequence_uniq := forall t, uniq (jobs_arriving_at arr_seq t).
 
-End ArrivalSequenceProperties.
+  (* We say that the arrival sequence is valid iff it is a set and arrival times
+     are consistent *)
+  Definition valid_arrival_sequence :=
+    consistent_arrival_times /\ arrival_sequence_uniq.
+
+End ValidArrivalSequence.
 
 (* Next, we define properties of job arrival times. *)
-Section PropertiesOfArrivalTime.
+Section ArrivalTimeProperties.
 
   (* Assume that job arrival times are known. *)
   Context {Job: JobType}.
@@ -83,7 +88,7 @@ Section PropertiesOfArrivalTime.
      some time t with t1 <= t < t2. *)
   Definition arrived_between (t1 t2 : instant) := t1 <= job_arrival j < t2.
 
-End PropertiesOfArrivalTime.
+End ArrivalTimeProperties.
 
 (* In this section, we define arrival sequence prefixes, which are useful to
    define (computable) properties over sets of jobs in the schedule. *)

restructuring/behavior/facts/all.v

+Require Export rt.restructuring.behavior.facts.service.
+Require Export rt.restructuring.behavior.facts.completion.
+Require Export rt.restructuring.behavior.facts.ideal_schedule.
+Require Export rt.restructuring.behavior.facts.sequential.
+Require Export rt.restructuring.behavior.facts.arrivals.

behavior/facts/arrivals.v → restructuring/behavior/facts/arrivals.v

-From rt.behavior.arrival Require Export arrival_sequence.
+From rt.restructuring.behavior.arrival Require Export arrival_sequence.
 From rt.util Require Import all.
 
-
 (* In this section, we establish useful facts about arrival sequence prefixes. *)
 Section ArrivalSequencePrefix.
 
@@ -79,8 +78,8 @@ Section ArrivalSequencePrefix.
     Section ArrivalTimes.
 
       (* Assume that job arrival times are consistent. *)
-      Hypothesis H_arrival_times_are_consistent:
-        arrival_times_are_consistent arr_seq.
+      Hypothesis H_consistent_arrival_times:
+        consistent_arrival_times arr_seq.
 
       (* First, we prove that if a job belongs to the prefix
          (jobs_arrived_before t), then it arrives in the arrival sequence. *)
@@ -89,7 +88,7 @@ Section ArrivalSequencePrefix.
           j \in jobs_arrived_between t1 t2 ->
                 arrives_in arr_seq j.
       Proof.
-        rename H_arrival_times_are_consistent into CONS.
+        rename H_consistent_arrival_times into CONS.
         intros j t1 t2 IN.
         apply mem_bigcat_nat_exists in IN.
         move: IN => [arr [IN _]].
@@ -104,7 +103,7 @@ Section ArrivalSequencePrefix.
           j \in jobs_arrived_between t1 t2 ->
                 arrived_between j t1 t2.
       Proof.
-        rename H_arrival_times_are_consistent into CONS.
+        rename H_consistent_arrival_times into CONS.
         intros j t1 t2 IN.
         apply mem_bigcat_nat_exists in IN.
         move: IN => [t0 [IN /= LT]].
@@ -121,7 +120,7 @@ Section ArrivalSequencePrefix.
         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 /=.
+          by rewrite /arrived_between /=.
       Qed.
 
       (* Similarly, we prove that if a job from the arrival sequence arrives
@@ -132,7 +131,7 @@ Section ArrivalSequencePrefix.
           arrived_between j t1 t2 ->
           j \in jobs_arrived_between t1 t2.
       Proof.
-        rename H_arrival_times_are_consistent into CONS.
+        rename H_consistent_arrival_times into CONS.
         move => j t1 t2 [a_j ARRj] BEFORE.
         have SAME := ARRj; apply CONS in SAME; subst a_j.
           by apply mem_bigcat_nat with (j := (job_arrival j)).
@@ -141,10 +140,10 @@ Section ArrivalSequencePrefix.
       (* Next, we prove that if the arrival sequence doesn't contain duplicate
          jobs, the same applies for any of its prefixes. *)
       Lemma arrivals_uniq :
-        arrival_sequence_is_a_set arr_seq ->
+        arrival_sequence_uniq arr_seq ->
         forall t1 t2, uniq (jobs_arrived_between t1 t2).
       Proof.
-        rename H_arrival_times_are_consistent into CONS.
+        rename H_consistent_arrival_times into CONS.
         unfold jobs_arrived_up_to; intros SET t1 t2.
         apply bigcat_nat_uniq; first by done.
         intros x t t' IN1 IN2.

behavior/facts/completion.v → restructuring/behavior/facts/completion.v

-From rt.behavior.schedule Require Export schedule.
-From rt.behavior.facts Require Export service.
+From rt.restructuring.behavior.schedule Require Export schedule.
+From rt.restructuring.behavior.facts Require Export service.
 
 (** In this file, we establish basic facts about job completions. *)
 
-
 Section CompletionFacts.
   (* Consider any job type,...*)
   Context {Job: JobType}.
@@ -28,7 +27,7 @@ Section CompletionFacts.
   Proof.
     move => t t' LE. rewrite /completed_by /service => COMP.
     apply leq_trans with (n := service_during sched j 0 t); auto.
-    by apply service_monotonic.
+      by apply service_monotonic.
   Qed.
 
   (* We observe that being incomplete is the same as not having received
@@ -66,7 +65,7 @@ Section CompletionFacts.
     move=> t SERVICE.
     rewrite subn_gt0 /service /service_during.
     apply leq_trans with (\sum_(0 <= t0 < t.+1) service_at sched j t0);
-      last by rewrite H_completed_jobs.
+    last by rewrite H_completed_jobs.
       by rewrite big_nat_recr //= -addn1 leq_add2l.
   Qed.
 
@@ -102,8 +101,8 @@ Section CompletionFacts.
     rewrite leqNgt in BUG; move: BUG => /negP BUG; apply BUG.
     rewrite /service /service_during big_nat_recr // /= -addn1.
     apply leq_add.
-    * by rewrite -/(service_during sched j 0 t) -/(completed_by sched j t).
-    * by rewrite /service_at; apply: H_scheduled_implies_serviced; rewrite -/(scheduled_at _ _ _).
+    - by rewrite -/(service_during sched j 0 t) -/(completed_by sched j t).
+    - by rewrite /service_at; apply: H_scheduled_implies_serviced; rewrite -/(scheduled_at _ _ _).
   Qed.
 
   (* ... and that a scheduled job cannot be completed. *)
@@ -171,13 +170,13 @@ Section ServiceAndCompletionFacts.
       elim => [| n IH]; first by rewrite service0 //.
       rewrite leq_eqVlt in IH.
       case/orP: IH => [EQ | LT]; rewrite -service_last_plus_before.
-      * rewrite not_scheduled_implies_no_service; first by rewrite addn0 //.
+      - rewrite not_scheduled_implies_no_service; first by rewrite addn0 //.
         apply: completed_implies_not_scheduled; auto. unfold unit_service_proc_model in H_unit_service.
         move /eqP in EQ.
         rewrite /completed_by EQ //.
-      * apply leq_trans with (n := service sched j n + 1).
-        - rewrite leq_add2l /service_at //.
-        - rewrite -(ltnS (service sched j n + 1) _) -(addn1 (job_cost j)) ltn_add2r //.
+      - apply leq_trans with (n := service sched j n + 1).
+        + rewrite leq_add2l /service_at //.
+        + rewrite -(ltnS (service sched j n + 1) _) -(addn1 (job_cost j)) ltn_add2r //.
     Qed.
 
     (* We show that the service received by job j in any interval is no larger
@@ -208,7 +207,7 @@ Section ServiceAndCompletionFacts.
         move=> t SCHED.
         rewrite /pending.
         apply /andP; split;
-          first by apply: H_jobs_must_arrive => //.
+        first by apply: H_jobs_must_arrive => //.
         apply: scheduled_implies_not_completed => //.
       Qed.
 
@@ -225,13 +224,13 @@ Section ServiceAndCompletionFacts.
     move=> t.
     rewrite incomplete_is_positive_remaining_cost => REMCOST.
     rewrite -less_service_than_cost_is_incomplete -(service_cat sched j t);
-      last by rewrite -addnBA //; apply: leq_addr.
+    last by rewrite -addnBA //; apply: leq_addr.
     apply leq_ltn_trans with (n := service sched j t + remaining_cost sched j t - 1).
     - by rewrite -!addnBA //; rewrite leq_add2l; apply cumulative_service_le_delta; exact.
     - rewrite service_cost_invariant // -subn_gt0 subKn //.
       move: REMCOST. rewrite /remaining_cost subn_gt0 => SERVICE.
-      by apply leq_ltn_trans with (n := service sched j t).
- Qed.
+        by apply leq_ltn_trans with (n := service sched j t).
+  Qed.
 
 End ServiceAndCompletionFacts.
 
@@ -275,8 +274,8 @@ Section PositiveCost.
     move=> t COMPLETE.
     have POSITIVE_SERVICE: 0 < service sched j t
       by apply leq_trans with (n := job_cost j); auto.
-    by apply: positive_service_implies_scheduled_since_arrival; assumption.
- Qed.
+      by apply: positive_service_implies_scheduled_since_arrival; assumption.
+  Qed.
 
   (* We also prove that the job is pending at the moment of its arrival. *)
   Lemma job_pending_at_arrival:
@@ -284,7 +283,7 @@ Section PositiveCost.
   Proof.
     rewrite /pending.
     apply/andP; split;
-      first by rewrite /has_arrived //.
+    first by rewrite /has_arrived //.
     rewrite /completed_by no_service_before_arrival // -ltnNge //.
   Qed.
 

behavior/facts/ideal_schedule.v → restructuring/behavior/facts/ideal_schedule.v

-From rt.behavior.schedule Require Import schedule ideal.
+From rt.restructuring.behavior.schedule Require Import schedule ideal.
 (* Note: we do not re-export the basic definitions to avoid littering the global
    namespace with type class instances. *)
 
@@ -8,15 +8,21 @@ Section OnlyOneJobScheduled.
      model. *)
   Context {Job: JobType}.
 
-  (* Consider an ideal schedule... *) Variable sched: schedule (processor_state
-  Job).
+  (* Consider an ideal schedule... *)
+  Variable sched: schedule (processor_state Job).
 
-  (* ...and two given jobs that are to be scheduled. *) Variable j1 j2: Job.
+  (* ...and two given jobs that are to be scheduled. *)
+  Variable j1 j2: Job.
 
   (* At any time t, if both j1 and j2 are scheduled, then they must be the same
-     job. *) Lemma only_one_job_scheduled: forall t, scheduled_at sched j1 t ->
-     scheduled_at sched j2 t -> j1 = j2.  Proof.  rewrite /scheduled_at
-     /scheduled_in /pstate_instance => t /eqP -> /eqP EQ.  by inversion EQ.
-     Qed.
+     job. *)
+  Lemma only_one_job_scheduled:
+    forall t,
+      scheduled_at sched j1 t ->
+      scheduled_at sched j2 t ->
+      j1 = j2.
+  Proof.
+    by rewrite /scheduled_at=>t/eqP->/eqP[->].
+  Qed.
 
 End OnlyOneJobScheduled.

behavior/facts/sequential.v → restructuring/behavior/facts/sequential.v

-From rt.behavior Require Export sequential.
+From rt.restructuring.behavior Require Export schedule.sequential.
 
 Section ExecutionOrder.
   (* Consider any type of job associated with any type of tasks... *)
@@ -39,4 +39,3 @@ Section ExecutionOrder.
   Qed.
 
 End ExecutionOrder.
-

behavior/facts/service.v → restructuring/behavior/facts/service.v

 From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.behavior.schedule Require Export schedule.
+From rt.restructuring.behavior.schedule Require Export schedule.
 From rt.util Require Import tactics step_function sum.
 
 (** In this file, we establish basic facts about the service received by

behavior/job.v → restructuring/behavior/job.v

@@ -3,3 +3,7 @@ From mathcomp Require Export eqtype.
 (* Throughout the library we assume that jobs have decidable equality *)
 
 Definition JobType := eqType.
+
+(* Definition of a generic type of parameter relating jobs to a discrete cost *)
+
+Class JobCost (J : JobType) := job_cost : J -> nat.

behavior/schedule/ideal.v → restructuring/behavior/schedule/ideal.v

-From rt.behavior Require Export schedule.schedule.
+From rt.restructuring.behavior Require Export schedule.schedule.
 
 (** First let us define the notion of an ideal schedule state,
  *  as done in Prosa so far: either a job is scheduled or the system is idle.

behavior/schedule/multiprocessor.v → restructuring/behavior/schedule/multiprocessor.v

 From mathcomp Require Export fintype.
-From rt.behavior.schedule Require Export schedule.
+From rt.restructuring.behavior.schedule Require Export schedule.
 
 Section Schedule.
 

behavior/schedule/schedule.v → restructuring/behavior/schedule/schedule.v

 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-From rt.behavior Require Export arrival.arrival_sequence.
+From rt.restructuring.behavior Require Export arrival.arrival_sequence.
 
 (* We define the notion of a generic processor state. The processor state type
  * determines aspects of the execution environment are modeled (e.g., overheads, spinning).
@@ -22,11 +22,7 @@ Class ProcessorState (Job : eqType) (State : Type) :=
 (* A schedule maps an instant to a processor state *)
 Definition schedule (PState : Type) := instant -> PState.
 
-(* Definition of a generic type of parameter relating jobs to a discrete cost *)
-
-Class JobCost (J : JobType) := job_cost : J -> nat.
-
-Section Service.
+Section Schedule.
   Context {Job : eqType} {PState : Type}.
   Context `{ProcessorState Job PState}.
 
@@ -71,10 +67,8 @@ Section Service.
   Definition remaining_cost j t :=
     job_cost j - service j t.
 
-  (* In this section, we define properties of valid schedules. *)
-  Section ValidSchedules.
-
-    Variable (arr_seq : arrival_sequence Job).
+  (* In this section, we define valid schedules. *)
+  Section ValidSchedule.
 
     (* We define whether jobs come from some arrival sequence... *)
     Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
@@ -88,5 +82,13 @@ Section Service.
     Definition completed_jobs_dont_execute :=
       forall j t, service j t <= job_cost j.
 
-  End ValidSchedules.
-End Service.
+    (* We say that the schedule is valid iff
+       - jobs come from some arrival sequence
+       - a job can only be scheduled if it has arrived and is not completed yet *)
+    Definition valid_schedule (arr_seq : arrival_sequence Job) :=
+      jobs_come_from_arrival_sequence arr_seq /\
+      jobs_must_arrive_to_execute /\
+      completed_jobs_dont_execute.
+
+  End ValidSchedule.
+End Schedule.

behavior/sequential.v → restructuring/behavior/schedule/sequential.v

-From rt.behavior Require Export schedule task.
+From rt.restructuring.behavior Require Export schedule task.
 
 Section PropertyOfSequentiality.
   (* Consider any type of job associated with any type of tasks... *)

behavior/schedule/spin.v → restructuring/behavior/schedule/spin.v

-From rt.behavior.schedule Require Export schedule.
+From rt.restructuring.behavior.schedule Require Export schedule.
 
 (** Next we define a processor state that includes the possibility of spinning,
  *  where spinning jobs do not progress (= don't get service).  *)

behavior/schedule/varspeed.v → restructuring/behavior/schedule/varspeed.v

-From rt.behavior.schedule Require Export schedule.
+From rt.restructuring.behavior.schedule Require Export schedule.
 
 (** Next, let us define a schedule with variable execution speed. *)
 Section State.

behavior/task.v → restructuring/behavior/task.v

 From mathcomp Require Export ssrbool.
-From rt.behavior Require Export job.
+From rt.restructuring.behavior Require Export job.
 
 (* Throughout the library we assume that jobs have decidable equality *)
 

restructuring/model/arrival/sporadic.v

+From rt.restructuring.behavior Require Export arrival.arrival_sequence task.
+
+Section TaskMinInterArrivalTime.
+  Context {T : TaskType}.
+
+  Variable (task_min_inter_arrival_time : duration).
+
+  Definition valid_task_min_inter_arrival_time :=
+    task_min_inter_arrival_time > 0.
+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.
+
+Section SporadicModel.
+  Context {T : TaskType} `{SporadicModel T}.
+
+  Variable ts : seq T.
+
+  Definition valid_taskset_min_inter_arrival_times :=
+    forall tsk : T,
+      tsk \in ts ->
+      task_min_inter_arrival_time tsk > 0.
+
+  Context {J : JobType} `{JobTask J T} `{JobArrival J}.
+
+  Variable arr_seq : arrival_sequence J.
+
+  (* 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).
+
+End SporadicModel.