Fix most definitions

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile apa.v divround.v eqjob_dec.v eqtask_dec.v extralib.v ExtraRelations.v helper.v identmp.v JobDefs.v liulayland.v PlatformDefs.v PriorityDefs.v response_time_bound.v ResponseTimeDefs.v schedulability.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v workload.v 
+# coq_makefile apa.v divround.v eqjob_dec.v eqtask_dec.v extralib.v ExtraRelations.v helper.v identmp.v JobDefs.v liulayland.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v test.v Vbase.v workload.v 
 #
 
 .DEFAULT_GOAL := all
@@ -80,7 +80,7 @@ endif
 #                    #
 ######################
 
-VFILES:= divround.v\
+VFILES:=divround.v\
   extralib.v\
   ExtraRelations.v\
   helper.v\
@@ -88,13 +88,13 @@ VFILES:= divround.v\
   PlatformDefs.v\
   PriorityDefs.v\
   ResponseTimeDefs.v\
-  schedulability.v\
+  SchedulabilityDefs.v\
   ScheduleDefs.v\
   ssromega.v\
   TaskArrivalDefs.v\
   TaskDefs.v\
   Vbase.v\
-  workload.v
+  WorkloadDefs.v
 
 -include $(addsuffix .d,$(VFILES))
 .SECONDARY: $(addsuffix .d,$(VFILES))

ResponseTimeDefs.v

 Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs PlatformDefs helper
                 ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
-(*Module ResponseTime.
+Module ResponseTime.
 
-Import SporadicTaskJob Schedule SporadicTaskset SporadicTaskArrival Platform.
+  Import SporadicTaskJob Schedule SporadicTaskset SporadicTaskArrival.
 
-Section ResponseTimeBound.
+  Section ResponseTimeBound.
+
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> nat.
+    Variable job_cost: Job -> nat.
+    Variable job_task: Job -> sporadic_task.
+  
+    Variable num_cpus: nat.
+    Variable rate: Job -> processor -> nat.
+    Variable schedule_of_platform: schedule Job -> Prop.
+  
+    Variable tsk: sporadic_task.
+    Variable R: time.
+
+    Definition response_time_ub_task :=
+      forall (sched: schedule Job) (j: Job),
+        job_task j == tsk ->
+        schedule_of_platform sched ->
+        completed job_cost num_cpus rate sched j (job_arrival j + R).
+
+  End ResponseTimeBound.
+
+End ResponseTime.
+  
+
+
+
+  
+
+
+
+
+
+  
   
-Variable plat: processor_platform.
+(*Variable plat: processor_platform.
 Variable ts: sporadic_taskset.
 Variable tsk: sporadic_task.
 

SchedulabilityDefs.v

+Require Import Vbase TaskDefs ScheduleDefs
+               ssreflect eqtype ssrbool ssrnat seq.
+
+Module Schedulability.
+
+  Import Schedule SporadicTaskset.
+
+  Section SchedulableDefs.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> nat.
+    Variable job_cost: Job -> nat.
+    Variable job_deadline: Job -> nat.
+  
+    Section SingleSchedule.
+
+      Variable num_cpus: nat.
+      Variable rate: Job -> processor -> nat.
+      Variable schedule_from_platform: schedule Job -> Prop.
+      Variable sched: schedule Job.
+    
+      Hypothesis sched_platform: schedule_from_platform sched.
+
+      Definition job_misses_no_deadline (j: Job) :=
+        completed job_cost num_cpus rate sched j (job_arrival j + job_deadline j).
+
+      Definition no_deadline_misses_in :=
+        forall j arr,
+          arrives_at job_arrival j arr ->
+          completed job_cost num_cpus rate sched j (arr + job_deadline j).
+
+    End SingleSchedule.
+
+    Section SingleScheduleTasks.
+
+      Variable job_task: Job -> sporadic_task.
+    
+      Variable num_cpus: nat.
+      Variable rate: Job -> processor -> nat.
+      Variable schedule_from_platform: schedule Job -> Prop.
+      Variable sched: schedule Job.
+    
+      Hypothesis sched_platform: schedule_from_platform sched.
+
+      Variable ts: sporadic_taskset.
+      Variable tsk: sporadic_task.
+      Hypothesis task_in_taskset : tsk \in ts.
+
+      Definition task_misses_no_deadline :=
+        forall j,
+          job_task j == tsk ->
+          job_misses_no_deadline num_cpus rate sched j.
+
+      Definition task_misses_no_deadline_before (t': time) :=
+        forall j,
+          job_task j == tsk ->
+          job_arrival j + job_deadline j <= t' ->
+          job_misses_no_deadline num_cpus rate sched j.
+
+    End SingleScheduleTasks.
+
+  End SchedulableDefs.
+
+End Schedulability.
+
+
+  (*Definition schedulable_task (ts: taskset) (tsk: sporadic_task) :=
+  forall sched (PLAT: platform sched), task_misses_no_dl sched ts tsk.
+
+Definition schedulable_taskset (ts: taskset) :=
+  forall sched (PLAT: platform sched) (ARRts: ts_arrival_sequence ts sched)
+         tsk (IN: tsk \in ts), task_misses_no_dl sched ts tsk.*)

workload.v → WorkloadDefs.v

-Require Import Vbase TaskDefs ScheduleDefs TaskArrivalDefs divround helper
+Require Import Vbase TaskDefs ScheduleDefs TaskArrivalDefs ResponseTimeDefs
+        SchedulabilityDefs divround helper
         ssreflect ssrbool eqtype ssrnat seq div fintype bigop path ssromega.
 
 Module Workload.
 
-  Import SporadicTaskset Schedule SporadicTaskArrival.
+  Import SporadicTaskset Schedule SporadicTaskArrival ResponseTime Schedulability.
   
   Section WorkloadDef.
     
@@ -14,23 +15,87 @@ Module Workload.
     Variable num_cpus: nat.
     Variable sched: schedule Job.
 
-    Hypothesis rate_at_most_one :
-      forall j cpu, rate j cpu <= 1.
-
+    (* Consider some task *)
     Variable tsk: sporadic_task.
 
+    (* First, we define a function that returns the amount of service
+       received by this task in a particular processor. *)
     Definition service_of_task (cpu: nat) (j: option Job) : nat :=
       match j with
         | Some j' => (job_task j' == tsk) * (rate j' cpu)
         | None => 0
       end.
 
-    (* Workload is defined as the service receives by jobs of
-       a particular task in the interval [t1,t2). *)
+    (* Next, workload is defined as the service received by jobs of
+       the task in the interval [t1,t2). *)
     Definition workload (t1 t2: time) :=
       \sum_(t1 <= t < t2)
         \sum_(0 <= cpu < num_cpus)
           service_of_task cpu (sched cpu t).
+
+    (* Now we provide an alternative definition for workload,
+       which is more suitable for our proof.
+       First, we compute the list of jobs that are scheduled
+       between t1 and t2 (without duplicates). *)
+    Definition jobs_scheduled_between (t1 t2: time) : list Job :=
+      undup (\cat_(t1 <= t < t2)
+               \cat_(0 <= cpu < num_cpus)
+                 match (sched cpu t) with
+                 | Some j => [::j]
+                 | None => [::]
+                 end).
+
+    (* Now, we sum up the cumulative service between t1 and t2
+       of the scheduled jobs, but only those spawned by the task
+       that we care about. *)
+    Definition workload_joblist (t1 t2: time) :=
+      \sum_(j <- jobs_scheduled_between t1 t2 | job_task j == tsk)
+        service_during num_cpus rate sched j t1 t2.
+
+    Lemma workload_eq_workload_joblist (t1 t2: time) :
+      workload t1 t2 = workload_joblist t1 t2.
+    Proof.
+      unfold workload, workload_joblist, service_during.
+      rewrite [\sum_(j <- jobs_scheduled_between _ _ | _) _]exchange_big /=.
+      rewrite -> eq_big_nat with (F2 := fun j =>
+                \sum_(i <- jobs_scheduled_between t1 t2 | job_task i == tsk)
+                  service_at num_cpus rate sched i j); first by ins.
+      intros t LEt; rewrite exchange_big /=.
+      rewrite -> eq_big_nat with (F2 := fun j =>
+              \sum_(i0 <- jobs_scheduled_between t1 t2 | job_task i0 == tsk)
+                    (sched j t == Some i0) * rate i0 j); first by ins.
+      intros cpu LEcpu; rewrite -big_filter.
+      destruct (sched cpu t) eqn:SCHED; simpl; last first.
+        by rewrite -> eq_bigr with (F2 := fun i => 0);
+          [by rewrite big_const_seq iter_addn | by ins].
+        {
+          rename s into j; destruct (job_task j == tsk) eqn:EQtsk; try rewrite mul1n; try rewrite mul0n.
+          {  
+            rewrite -> bigD1_seq with (j := j); last by rewrite filter_undup undup_uniq.
+            { 
+              rewrite -> eq_bigr with (F2 := fun i => 0);
+                first by rewrite big_const_seq iter_addn /= mul0n 2!addn0 eq_refl mul1n.
+                intros i NEQ; destruct (Some j == Some i) eqn:SOMEeq; last by rewrite mul0n.
+                by move: SOMEeq => /eqP SOMEeq; inversion SOMEeq; subst; rewrite eq_refl in NEQ.
+            }
+            {
+              rewrite mem_filter; apply/andP; split; first by ins.
+              rewrite mem_undup.
+              apply mem_bigcat with (j := t); first by ins.
+              apply mem_bigcat with (j := cpu); first by ins.
+              by rewrite SCHED inE; apply/eqP.
+            }
+          }
+          {
+            rewrite big_filter; rewrite -> eq_bigr with (F2 := fun i => 0);
+              first by rewrite big_const_seq iter_addn mul0n addn0.
+            intros i EQtsk2; destruct (Some j == Some i) eqn:SOMEeq; last by rewrite mul0n.
+            by move: SOMEeq => /eqP SOMEeq; inversion SOMEeq;
+              subst; rewrite EQtsk2 in EQtsk.
+          }
+        }
+      Qed.
+ 
   End WorkloadDef.
 
   Section WorkloadBound.
@@ -58,42 +123,41 @@ Module Workload.
 
     Variable Job: eqType.
     Variable job_arrival: Job -> nat.
+    Variable job_cost: Job -> nat.
     Variable job_task: Job -> sporadic_task.
-
+    Variable job_deadline: Job -> nat.
 
     Variable num_cpus: nat.
     Variable rate: Job -> processor -> nat.
+    Variable schedule_of_platform: schedule Job -> Prop.
     Variable sched: schedule Job.
 
+    Hypothesis rate_at_most_one :
+      forall j cpu, rate j cpu <= 1.
+   
     Hypothesis sporadic_tasks: sporadic_task_model job_arrival job_task.
     Hypothesis restricted_deadlines: restricted_deadline_model ts.
 
-    (*Variable higher_priority: sched_job_hp_relation.
-    Hypothesis valid_policy: valid_jldp_policy higher_priority.*)
-
-    (*(* Assume an identical multiprocessor with an arbitrary number of CPUs *)
-    Variable cpumap: job_mapping.
-    Variable num_cpus: nat.
-    Hypothesis sched_of_multiprocessor: ident_mp num_cpus higher_priority cpumap sched.*)
-
     (* Let tsk be any task in the taskset. *)
     Variable tsk: sporadic_task.
     Hypothesis in_ts: tsk \in ts.
 
-    (* Suppose that we are given a response-time bound R_tsk for that task in any
-       schedule of this processor platform. *)
+    (* Assume that a response-time bound R_tsk for that task in any
+       schedule of this processor platform is also given. *)
     Variable R_tsk: time.
-    (*Hypothesis response_time_bound:
-      forall cpumap, response_time_ub (ident_mp num_cpus higher_priority cpumap) ts tsk R_tsk.*)
+    Hypothesis response_time_bound:
+      response_time_ub_task job_arrival job_cost job_task num_cpus rate schedule_of_platform tsk R_tsk.
 
     (* Consider an interval [t1, t1 + delta).*)
     Variable t1 delta: time.
-    (*Hypothesis no_deadline_misses: task_misses_no_dl_before sched ts tsk (t1 + delta).*)
+    Hypothesis no_deadline_misses_during_interval:
+      task_misses_no_deadline_before job_arrival job_cost job_deadline job_task num_cpus rate sched tsk (t1 + delta).
 
     Theorem workload_bound :
       workload job_task rate num_cpus sched tsk t1 (t1 + delta) <=
         W tsk R_tsk delta.
     Proof.
+      rewrite workload_eq_workload_joblist.
       (*rename sched_of_multiprocessor into MULT, sporadic_tasks into SPO, restricted_deadlines into RESTR,
          no_deadline_misses into NOMISS, higher_priority into hp.
   unfold sporadic_task_model, workload, W in *; ins; des.*)

helper.v

@@ -26,6 +26,20 @@ Reserved Notation "\cat_ ( m <= i < n ) F"
 Notation "\cat_ ( m <= i < n ) F" :=
   (\big[cat/[::]]_(m <= i < n) F%N) : nat_scope.
 
+
+Lemma mem_bigcat:
+  forall (T: eqType) x m n j (f: nat -> list T)
+         (LE: m <= j < n) (IN: x \in (f j)),
+  x \in \cat_(m <= i < n) (f i).
+Proof.
+  ins; move: LE => /andP LE; des.
+  rewrite -> big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
+  rewrite mem_cat; apply/orP; right.
+  destruct n; first by rewrite ltn0 in LE0.
+  rewrite big_nat_recl; last by ins.
+  by rewrite mem_cat; apply/orP; left.
+Qed.
+  
 Lemma exists_inP_nat t (P: nat -> bool):
   reflect (exists x, x < t /\ P x) [exists (x | x \in 'I_t), P x].
 Proof.

response_time_bound.v

-Require Import Vbase job task schedule task_arrival response_time platform
-        schedulability divround helper priority identmp helper workload
-        ssreflect ssrbool eqtype ssrnat seq div fintype bigop path ssromega.
-
-Definition interference_bound := sporadic_task -> sporadic_task -> time -> time -> time.
-
-Definition I_fp (hp: task_hp_relation) : interference_bound :=
-  fun (tsk other: sporadic_task) (R_other delta: time) =>
-    if hp other tsk then W other R_other delta else 0.
-
-Definition I_jlfp (hp: sched_job_hp_relation) : interference_bound :=
-  fun (tsk other: sporadic_task) (R_other delta: time) =>
-    if other != tsk then W other R_other delta else 0.
-
-Definition rt_analysis_eq (ts: taskset) (tsk: sporadic_task) (I: interference_bound)
-                          (R_other: sporadic_task -> time) (num_cpus R_tsk: time) :=
-  R_tsk == task_cost tsk + (\sum_(i <- ts) I tsk i (R_other i) R_tsk) %/ num_cpus.
-
-Section RTA_FP.
-
-Definition rt_analysis_fp (hp: task_hp_relation) (ts: taskset) (tsk: sporadic_task)
-                          (R_other: sporadic_task -> time) (num_cpus R_tsk: time) :=
-  (rt_analysis_eq ts tsk (I_fp hp) R_other num_cpus R_tsk) && (R_tsk <= task_deadline tsk).
-
-Definition schedulable_hp (plat: processor_platform) (ts: taskset) (tsk_hp: task_hp_relation) 
-                           (tsk: sporadic_task) :=
-  forall tsk' (IN: tsk' \in ts) (HPother: tsk_hp tsk' tsk),
-    schedulable_task plat ts tsk'.
-
-Definition rt_bound_hp (plat: processor_platform) (ts: taskset) (tsk_hp: task_hp_relation) 
-                       (R_other: sporadic_task -> time) (tsk: sporadic_task) :=
-  forall tsk' (IN: tsk' \in ts) (HPother: tsk_hp tsk' tsk),
-    response_time_ub plat ts tsk' (R_other tsk').
-
-Theorem rt_bound_fp :
-  forall ts sched (SPO: sporadic_task_model ts sched)
-         tsk_hp (VALIDfp: valid_fp_policy tsk_hp)
-         hp (VALIDhp: valid_jldp_policy hp) (CONV: convert_fp_jldp tsk_hp hp) 
-         cpumap num_cpus (MULT: ident_mp num_cpus hp cpumap sched)
-         (RESTR: restricted_deadline_model ts) tsk (IN: tsk \in ts)
-         (SCHEDhp: schedulable_hp (ident_mp num_cpus hp cpumap) ts tsk_hp tsk)
-         R_hp (RThp: forall cpumap, rt_bound_hp (ident_mp num_cpus hp cpumap) ts tsk_hp R_hp tsk)
-         R_tsk (ANALYSIS: rt_analysis_fp tsk_hp ts tsk R_hp num_cpus R_tsk),
-    (forall cpumap, response_time_ub (ident_mp num_cpus hp cpumap) ts tsk R_tsk).
-Proof.
-Admitted.
-
-End RTA_FP.
-
-Section RTA_JLFP.
-  
-Definition rt_analysis_jlfp (hp: sched_job_hp_relation) (ts: taskset) (tsk: sporadic_task)
-                            (R_other: sporadic_task -> time) (num_cpus R_tsk: time) :=
-  (rt_analysis_eq ts tsk (I_jlfp hp) R_other num_cpus R_tsk) && (R_tsk <= task_deadline tsk).
-
-End RTA_JLFP.
\ No newline at end of file

schedulability.v

-Require Import Vbase job task task_arrival schedule platform
-               ssrbool ssrnat seq.
-
-Section Schedulability.
-
-Variable platform: processor_platform.
-
-Section SingleSchedule.
-
-Variable sched: schedule.
-Hypothesis sched_platform: platform sched.
-
-Definition job_misses_no_dl (j: job) :=
-  completed sched j (job_arrival j + job_deadline j).
-
-Definition no_dl_misses :=
-  forall j arr (ARR: arrives_at sched j arr),
-    completed sched j (arr + job_deadline j).
-
-Definition task_misses_no_dl (ts: taskset) (tsk: sporadic_task) :=
-  << IN: tsk \in ts >> /\
-  << ARRts: ts_arrival_sequence ts sched >> /\
-  forall j (JOB: job_task j = tsk) arr (ARR: arrives_at sched j arr),
-    job_misses_no_dl j.
-
-Definition task_misses_no_dl_before (ts: taskset) (tsk: sporadic_task) (t': time) :=
-  << IN: tsk \in ts >> /\
-  << ARRts: ts_arrival_sequence ts sched >> /\
-  forall j (JOB: job_task j = tsk)
-         arr (ARR: arrives_at sched j arr)
-         (BEFOREdl: job_arrival j + job_deadline j <= t'),
-    job_misses_no_dl j.
-
-End SingleSchedule.
-
-Definition schedulable_task (ts: taskset) (tsk: sporadic_task) :=
-  forall sched (PLAT: platform sched), task_misses_no_dl sched ts tsk.
-
-Definition schedulable_taskset (ts: taskset) :=
-  forall sched (PLAT: platform sched) (ARRts: ts_arrival_sequence ts sched)
-         tsk (IN: tsk \in ts), task_misses_no_dl sched ts tsk.
-
-End Schedulability.
\ No newline at end of file