RT bound for partitioned scheduling

analysis/facts/model/partitioned.v

-From prosa Require Export model.schedule.partitioned.
+Require Export prosa.model.schedule.partitioned prosa.analysis.facts.behavior.all.
 
 Section Theory.
   (** Consider any type of jobs... *)
@@ -14,14 +14,14 @@ Section Theory.
   (** We define the projection of an arrival sequence on a core.  *)
   Variable arr_seq: arrival_sequence Job.
 
-  Lemma arrives_at_on : forall j t,
+  Lemma arrives_at_onE : forall j t,
       arrives_at arr_seq j t = arrives_at (arrival_sequence_on arr_seq (job_core j)) j t.
   Proof.
     move=> j t.
       by rewrite /arrives_at/arrivals_at mem_filter eqxx.
   Qed.
 
-  Lemma arrives_at_on_uniq : forall j r t,
+  Lemma arrives_at_on_uniq_core : forall j r t,
       arrives_at (arrival_sequence_on arr_seq r) j t ->
       r = job_core j.
   Proof.
@@ -29,7 +29,7 @@ Section Theory.
       by rewrite /arrives_at/arrivals_at mem_filter=>/andP[/eqP->].
   Qed.
 
-  Lemma arrives_in_on : forall j,
+  Lemma arrives_in_onE : forall j,
       arrives_in arr_seq j <-> arrives_in (arrival_sequence_on arr_seq (job_core j)) j.
   Proof.
     move=> j.
@@ -39,7 +39,7 @@ Section Theory.
     - by rewrite mem_filter eqxx in Ht.
   Qed.
 
-  Lemma arrives_in_on_uniq : forall j r,
+  Lemma arrives_in_on_uniq_core : forall j r,
       arrives_in (arrival_sequence_on arr_seq r) j ->
       r = job_core j.
   Proof.
@@ -48,4 +48,84 @@ Section Theory.
       by rewrite mem_filter=>/andP[/eqP->].
   Qed.
 
+  (* TODO : naming *)
+  Variable sched : schedule PState.
+
+  Hypothesis H_arrs :
+    forall r, jobs_come_from_arrival_sequence (schedule_on sched r) (arrival_sequence_on arr_seq r).
+
+  Lemma scheduled_at_uniq_core : forall j t r,
+      scheduled_at (schedule_on sched r) j t -> r = job_core j.
+  Proof.
+      by move=> j t r /H_arrs/arrives_in_on_uniq_core.
+  Qed.
+
+  Section Elimination.
+    Local Transparent scheduled_on service_on.
+    Lemma scheduled_in_onE : forall j t r,
+        scheduled_in j (schedule_on sched r t) = scheduled_on j (sched t) r.
+    Proof.
+      move=> j t r.
+      by apply/scheduled_inE/idP=>//=[[]].
+    Qed.
+
+    Lemma service_in_onE : forall j t r,
+        service_in j (schedule_on sched r t) = service_on j (sched t) r.
+    Proof.
+      move=> j t r.
+      by rewrite service_inE/=(bigD1 tt)//= big_pred0// addn0.
+    Qed.
+
+  End Elimination.
+
+  Lemma schedule_at_onE : forall j t,
+      scheduled_at (schedule_on sched (job_core j)) j t = scheduled_at sched j t.
+  Proof.
+    move=> j t.
+    rewrite /scheduled_at scheduled_in_onE.
+    apply/idP/scheduled_inE=>[SCHED|[r SCHED]].
+    { by exists (job_core j). }
+    by rewrite -(scheduled_at_uniq_core j t r)// /scheduled_at scheduled_in_onE.
+  Qed.
+
+  Lemma partitioned_jobs_come_from_arrival_sequence :
+    jobs_come_from_arrival_sequence sched arr_seq.
+  Proof.
+    move=> j t.
+    by rewrite -schedule_at_onE=>/H_arrs/arrives_in_onE.
+  Qed.
+
+  Lemma service_at_onE : forall j t,
+      service_at sched j t =
+      service_at (schedule_on sched (job_core j)) j t.
+  Proof.
+    move=> j t.
+    rewrite /service_at service_in_onE service_inE (bigD1 (job_core j))//=.
+    rewrite big1 ?addn0//= => r Hr.
+    apply: service_on_implies_scheduled_on.
+    rewrite -scheduled_in_onE.
+    apply/negP=>/H_arrs/arrives_in_on_uniq_core ABS.
+    by rewrite ABS eqxx in Hr.
+  Qed.
+
+  Lemma service_during_onE : forall j t1 t2,
+      service_during sched j t1 t2 =
+      service_during (schedule_on sched (job_core j)) j t1 t2.
+  Proof.
+    move=> j t1 t2.
+    rewrite /service_during.
+    apply: eq_bigr=> t _.
+    exact: service_at_onE.
+  Qed.
+
+  Context `{JobCost Job} `{JobArrival Job}.
+
+  Lemma partitioned_job_response_time_bound : forall j r,
+      job_response_time_bound (schedule_on sched (job_core j)) j r =
+      job_response_time_bound sched j r.
+  Proof.
+    move=> j r.
+    by rewrite /job_response_time_bound/completed_by/service service_during_onE.
+  Qed.
+
 End Theory.

model/schedule/partitioned.v

-Require Export prosa.behavior.all.
+Require Export prosa.behavior.all prosa.model.task.concept.
 
 (** * Definition of Partitioned Scheduling *)
 
@@ -61,14 +61,25 @@ Section Model.
   (** Given an assignement of jobs to cores.  *)
   Context `{@JobCore Job PState H}. (* TODO : Should we have to refer explicitly to H here? *)
 
-  (** Given a model for each core *)
+  (** Given a scheduling policy for each core *)
   Variable core_model : forall r : Core, arrival_sequence Job -> schedule (core_state r) -> Prop.
 
   (** Given an arrival sequence and schedule.  *)
   Variable arr_seq : arrival_sequence Job.
   Variable sched : schedule PState.
 
-  (** We say that a trace is partitioned according to the model if the projection on each core satisfies the core's model. *)
+  (** In order to define a partitioned model we require that the projection of the arrival sequence and schedule on each core satisfies the core's model. Note that this does not systematically imply that jobs are only scheduled on their assigned core in the schedule. We show in [prosa.analysis.facts.model.partitioned] that this property holds if the projection only schedules jobs from the arrival sequence. *)
   Definition partitioned_model :=
     forall r : Core, core_model r (arrival_sequence_on arr_seq r) (schedule_on sched r).
 End Model.
+
+(** Class for assigning a core to all jobs of a task. *)
+(* TODO: not great to need Job here *)
+Class TaskCore (Task : TaskType) (Job : JobType) (PState : Type) `{ProcessorState Job PState} :=
+  task_core : Task -> Core.
+
+(** Given an assignement of tasks to cores, we can assign jobs to a core depending on their task. *)
+Instance TaskJobCore
+         (Task : TaskType) (Job : JobType) `{JobTask Job Task}
+         (PState : Type) `{ProcessorState Job PState}
+         `{TaskCore Task Job PState} : JobCore Job PState := fun j => task_core (job_task j).