Initial draft of the base for the behavior part of the refactored hierarchy....

Initial draft of the base for the behavior part of the refactored hierarchy. Implements most of the proposal discussed in Braunschweig.

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.util Require Import all.
+
+
+(* Definitions and properties of job arrival sequences. *)
+
+(* We begin by defining a job arrival sequence. *)
+Section ArrivalSequenceDef.
+
+  (* Given any job type with decidable equality, ... *)
+  Variable Job: JobType.
+
+  (* ..., an arrival sequence is a mapping from any time to a (finite) sequence of jobs. *)
+  Definition arrival_sequence := instant -> seq Job.
+
+End ArrivalSequenceDef.
+
+(* Next, we define properties of jobs in a given arrival sequence. *)
+Section JobProperties.
+
+  (* Consider any job arrival sequence. *)
+  Context {Job: JobType}.
+  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.
+
+  (* 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.
+
+  (* 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.
+
+End JobProperties.
+
+(* Definition of a generic type of parameter for job_arrival *)
+
+Class JobArrival (J : JobType) := job_arrival : J -> instant.
+
+(* Next, we define properties of a valid arrival sequence. *)
+Section ArrivalSequenceProperties.
+
+  (* Assume that job arrival times are known. *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+
+  (* Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (* 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 :=
+    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).
+
+End ArrivalSequenceProperties.
+
+(* Next, we define properties of job arrival times. *)
+Section PropertiesOfArrivalTime.
+
+  (* Assume that job arrival times are known. *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+
+  (* Let j be any job. *)
+  Variable j: Job.
+
+  (* We say that job j has arrived at time t iff it arrives at some time t_0 with t_0 <= t. *)
+  Definition has_arrived (t : instant) := job_arrival j <= t.
+
+  (* Next, we say that job j arrived before t iff it arrives at some time t_0 with t_0 < t. *)
+  Definition arrived_before (t : instant) := job_arrival j < t.
+
+  (* Finally, we say that job j arrives between t1 and t2 iff it arrives at some time t with
+       t1 <= t < t2. *)
+  Definition arrived_between (t1 t2 : instant) := t1 <= job_arrival j < t2.
+
+End PropertiesOfArrivalTime.
+
+(* In this section, we define arrival sequence prefixes, which are useful
+     to define (computable) properties over sets of jobs in the schedule. *)
+Section ArrivalSequencePrefix.
+
+  (* Assume that job arrival times are known. *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+
+  (* 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.
+
+    (* We begin with basic lemmas for manipulating the sequences. *)
+    Section Basic.
+
+      (* First, we show that the set of arriving jobs can be split
+           into disjoint intervals. *)
+      Lemma job_arrived_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.
+      Proof.
+        unfold jobs_arrived_between; intros t1 t t2 GE LE.
+          by rewrite (@big_cat_nat _ _ _ t).
+      Qed.
+
+      Lemma jobs_arrived_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).
+      Proof.
+          by intros j t1 t t2 GE LE; rewrite (job_arrived_between_cat _ t).
+      Qed.
+
+      Lemma jobs_arrived_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'.
+      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.
+        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].
+          by rewrite mem_cat; apply/orP; left.
+      Qed.
+
+    End Basic.
+
+    (* Next, we relate the arrival prefixes with job arrival times. *)
+    Section ArrivalTimes.
+
+      (* Assume that job arrival times are consistent. *)
+      Hypothesis H_arrival_times_are_consistent:
+        arrival_times_are_consistent arr_seq.
+
+      (* First, we prove that if a job belongs to the prefix (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.
+      Proof.
+        rename H_arrival_times_are_consistent into CONS.
+        intros j t1 t2 IN.
+        apply mem_bigcat_nat_exists in IN.
+        move: IN => [arr [IN _]].
+          by exists arr.
+      Qed.
+
+      (* Next, we prove that if a job belongs to the prefix (jobs_arrived_between t1 t2),
+         then it indeed arrives between t1 and t2. *)
+      Lemma in_arrivals_implies_arrived_between:
+        forall j t1 t2,
+          j \in jobs_arrived_between t1 t2 ->
+                arrived_between j t1 t2.
+      Proof.
+        rename H_arrival_times_are_consistent into CONS.
+        intros j t1 t2 IN.
+        apply mem_bigcat_nat_exists in IN.
+        move: IN => [t0 [IN /= LT]].
+          by apply CONS in IN; rewrite /arrived_between IN.
+      Qed.
+
+      (* Similarly, if a job belongs to the prefix (jobs_arrived_before t),
+           then it indeed arrives before time t. *)
+      Lemma in_arrivals_implies_arrived_before:
+        forall j t,
+          j \in jobs_arrived_before 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.
+
+      (* Similarly, we prove that if a job from the arrival sequence arrives before t,
+         then it belongs to the sequence (jobs_arrived_before t). *)
+      Lemma arrived_between_implies_in_arrivals:
+        forall j t1 t2,
+          arrives_in arr_seq j ->
+          arrived_between j t1 t2 ->
+          j \in jobs_arrived_between t1 t2.
+      Proof.
+        rename H_arrival_times_are_consistent 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)).
+      Qed.
+
+      (* 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 ->
+        forall t1 t2, uniq (jobs_arrived_between t1 t2).
+      Proof.
+        rename H_arrival_times_are_consistent into CONS.
+        unfold jobs_arrived_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.
+      Qed.
+
+    End ArrivalTimes.
+
+  End Lemmas.
+
+End ArrivalSequencePrefix.

behavior/job.v

+From mathcomp Require Export eqtype.
+
+(* Throughout the library we assume that jobs have decidable equality *)
+
+Definition JobType := eqType.

behavior/schedule/ideal.v

+From rt.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.
+ *)
+
+Section State.
+
+  Variable Job: eqType.
+
+  Definition processor_state := option Job.
+
+  Instance pstate_instance : ProcessorState Job (option Job) :=
+    {
+      scheduled_in j s := s == Some j;
+      service_in j s   := s == Some j
+    }.
+  Proof.
+      by move=> j [j'->|].
+  Qed.
+End State.

behavior/schedule/multiprocessor.v

+From mathcomp Require Export fintype.
+From rt.behavior.schedule Require Export schedule.
+
+Section Schedule.
+
+  Variable Job: eqType.
+  Variable processor_state: Type.
+  Context `{ProcessorState Job processor_state}.
+
+  Definition processor (num_cpus: nat) := 'I_num_cpus.
+
+  Variable num_cpus : nat.
+
+  Definition identical_state := processor num_cpus -> processor_state.
+
+  Instance multiproc_state : ProcessorState Job (identical_state) :=
+    {
+      scheduled_in j s := [exists cpu, scheduled_in j (s cpu)];
+      service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu)
+    }.
+  Proof.
+    move=> j s /existsP Hsched.
+    apply/eqP.
+    rewrite sum_nat_eq0.
+    apply/forallP=>/= c.
+    rewrite service_implies_scheduled//.
+    case: (boolP (scheduled_in _ _))=>//= Habs.
+    exfalso; apply: Hsched.
+      by exists c.
+  Qed.
+End Schedule.

behavior/schedule/schedule.v

+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+From rt.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).
+ * In the most simple case (i.e., Ideal.processor_state), at any time,
+ * either a particular job is either scheduled or it is idle. *)
+Class ProcessorState (Job : eqType) (State : Type) :=
+  {
+    (* For a given processor state, the [scheduled_in] predicate checks whether a given
+     * job is running in that state. *)
+    scheduled_in: Job -> State -> bool;
+    (* For a given processor state, the [service_in] function determines how much
+     * service a given job receives in that state. *)
+    service_in: Job -> State -> nat;
+    (* For a given processor state, a job does not receive service if it is not scheduled
+     * in that state *)
+    service_implies_scheduled :
+      forall j s, scheduled_in j s = false -> service_in j s = 0
+  }.
+
+(* 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.
+  Context {Job : eqType} {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  Variable sched : schedule PState.
+
+  (* First, we define whether a job j is scheduled at time t, ... *)
+  Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
+
+  (* ... and the instantaneous service received by
+           job j at time t. *)
+  Definition service_at (j : Job) (t : instant) := service_in j (sched t).
+
+  (* Based on the notion of instantaneous service, we define the
+           cumulative service received by job j during any interval [t1, t2). *)
+  Definition service_during (j : Job) (t1 t2 : instant) :=
+    \sum_(t1 <= t < t2) service_at j t.
+
+  (* Using the previous definition, we define the cumulative service
+           received by job j up to time t, i.e., during interval [0, t). *)
+  Definition service (j : Job) (t : instant) := service_during j 0 t.
+
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+
+  (* Next, we say that job j has completed by time t if it received enough
+           service in the interval [0, t). *)
+  Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
+
+  (* Job j is pending at time t iff it has arrived but has not yet completed. *)
+  Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
+
+  (* Job j is pending earlier and at time t iff it has arrived before time t
+           and has not been completed yet. *)
+  Definition pending_earlier_and_at (j : Job) (t : instant) :=
+    arrived_before j t && ~~ completed_by j t.
+
+  (* Job j is backlogged at time t iff it is pending and not scheduled. *)
+  Definition backlogged (j : Job) (t : instant) := pending j t && ~~ scheduled_at j t.
+
+  (* Let's define the remaining cost of job j as the amount of service
+         that has to be received for its completion. *)
+  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).
+
+    (* We define whether jobs come from some arrival sequence... *)
+    Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
+      forall j t, scheduled_at j t -> arrives_in arr_seq j.
+
+    (* ..., whether a job can only be scheduled if it has arrived ... *)
+    Definition jobs_must_arrive_to_execute :=
+      forall j t, scheduled_at j t -> has_arrived j t.
+
+    (* ... and whether a job cannot be scheduled after it completes. *)
+    Definition completed_jobs_dont_execute :=
+      forall j t, service j t <= job_cost j.
+
+  End ValidSchedules.
+End Service.

behavior/schedule/spin.v

+From rt.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).  *)
+Section State.
+
+  Variable Job: eqType.
+
+  Inductive processor_state :=
+    Idle
+  | Spin (j : Job)
+  | Progress (j : Job).
+
+  Section Service.
+
+    Variable j : Job.
+
+    Definition scheduled_in (s : processor_state) : bool :=
+      match s with
+      | Idle        => false
+      | Spin j'     => j' == j
+      | Progress j' => j' == j
+      end.
+
+    Definition service_in (s : processor_state) : nat :=
+      match s with
+      | Idle        => 0
+      | Spin j'     => 0
+      | Progress j' => j' == j
+      end.
+
+  End Service.
+
+  Instance pstate_instance : ProcessorState Job (processor_state) :=
+    {
+      scheduled_in := scheduled_in;
+      service_in   := service_in
+    }.
+  Proof.
+    by move=> j [|j'|j']//=->.
+  Qed.
+End State.

behavior/schedule/varspeed.v

+From rt.behavior.schedule Require Export schedule.
+
+(** Next, let us define a schedule with variable execution speed. *)
+Section State.
+
+  Variable Job: eqType.
+
+  Inductive processor_state :=
+    Idle
+  | Progress (j : Job) (speed : nat).
+
+  Section Service.
+
+    Variable j : Job.
+
+    Definition scheduled_in (s : processor_state) : bool :=
+      match s with
+      | Idle => false
+      | Progress j' _  => j' == j
+      end.
+
+    Definition service_in (s : processor_state) : nat :=
+      match s with
+      | Idle => 0
+      | Progress j' s  => if j' == j then s else 0
+      end.
+
+  End Service.
+
+  Instance pstate_instance : ProcessorState Job processor_state :=
+    {
+      scheduled_in := scheduled_in;
+      service_in   := service_in
+    }.
+  Proof.
+      by move=> j []//= j' s->.
+  Qed.
+End State.

behavior/task.v

+From rt.behavior Require Export job.
+
+(* Throughout the library we assume that jobs have decidable equality *)
+
+Definition TaskType := eqType.
+
+(* Definition of a generic type of parameter relating jobs to tasks *)
+
+Class JobTask (T : TaskType) (J : JobType) := job_task : J -> T.
\ No newline at end of file

behavior/time.v

+(* Time is defined as a natural number. *)
+
+Definition duration := nat.
+Definition instant  := nat.