Cleanup task arrival, response time, schedulability

response_time.v

 Require Import Vbase task job task_arrival schedule util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
+(* Definition of response-time bound and some simple lemmas. *)
 Module ResponseTime.
 
   Import Schedule SporadicTaskset SporadicTaskArrival.
-                                    
+  
   Section ResponseTimeBound.
 
     Context {sporadic_task: eqType}.
@@ -57,16 +58,16 @@ Module ResponseTime.
 
     Section SpecificJob.
 
-      (* Consider any job ...*)
+      (* Then, for any job j ...*)
       Variable j: JobIn arr_seq.
       
-      (* ...with response-time bound R in this schedule. *)
+      (* ...with response-time bound R in this schedule, ... *)
       Variable R: time.
       Hypothesis response_time_bound:
         job_has_completed_by j (job_arrival j + R). 
 
-      (* The service at any time t' after the response time is 0. *)
-      Lemma service_at_after_job_rt_zero :
+      (* the service received by j at any time t' after its response time is 0. *)
+      Lemma service_after_job_rt_zero :
         forall t',
           t' >= job_arrival j + R ->
           service_at rate sched j t' = 0.
@@ -86,8 +87,8 @@ Module ResponseTime.
           by rewrite big_nat_recr // /=; apply leq_addl.
       Qed.
 
-      (* The cumulative service after the response time is 0. *)
-      Lemma sum_service_after_job_rt_zero :
+      (* The same applies for the cumulative service of job j. *)
+      Lemma cumulative_service_after_job_rt_zero :
         forall t' t'',
           t' >= job_arrival j + R ->
           \sum_(t' <= t < t'') service_at rate sched j t = 0.
@@ -96,7 +97,7 @@ Module ResponseTime.
         rewrite big_nat_cond; rewrite -> eq_bigr with (F2 := fun i => 0);
           first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
         intro i; rewrite andbT; move => /andP [LE _].
-        by rewrite service_at_after_job_rt_zero;
+        by rewrite service_after_job_rt_zero;
           [by ins | by apply leq_trans with (n := t')].
       Qed.
       
@@ -104,33 +105,35 @@ Module ResponseTime.
     
     Section AllJobs.
 
-      (* Assume a task tsk ...*)
+      (* Consider any task tsk ...*)
       Variable tsk: sporadic_task.
 
-      (* ...and that R is a response-time bound of tsk in this schedule. *)
+      (* ... for which a response-time bound R is known. *)
       Variable R: time.
       Hypothesis response_time_bound:
         is_response_time_bound_of_task job_cost job_task tsk rate sched R.
 
+      (* Then, for any job j of this task, ...*)
       Variable j: JobIn arr_seq.
       Hypothesis H_job_of_task: job_task j = tsk.
 
-      (* The service at any time t' after the response time is 0. *)
-      Lemma service_at_after_rt_zero :
+      (* the service received by job j at any time t' after the response time is 0. *)
+      Lemma service_after_task_rt_zero :
         forall t',
           t' >= job_arrival j + R ->
           service_at rate sched j t' = 0.
       Proof.
-        by ins; apply service_at_after_job_rt_zero with (R := R); [apply response_time_bound |].
+        by ins; apply service_after_job_rt_zero with (R := R); [apply response_time_bound |].
       Qed.
 
-      (* The cumulative service after the response time is 0. *)
-      Lemma sum_service_after_rt_zero :
+      (* The same applies for the cumulative service of job j. *)
+      Lemma cumulative_service_after_task_rt_zero :
         forall t' t'',
           t' >= job_arrival j + R ->
           \sum_(t' <= t < t'') service_at rate sched j t = 0.
       Proof.
-        by ins; apply sum_service_after_job_rt_zero with (R := R); [apply response_time_bound |].
+        by ins; apply cumulative_service_after_job_rt_zero with (R := R);
+          first by apply response_time_bound. 
       Qed.
       
     End AllJobs.

schedulability.v

-Require Import Vbase task schedule
-               ssreflect eqtype ssrbool ssrnat seq.
+Require Import Vbase job task schedule util_lemmas
+               ssreflect eqtype ssrbool ssrnat seq bigop.
 
+(* Definitions of deadline miss. *)
 Module Schedulability.
 
-  Import Schedule SporadicTaskset.
+  Import Schedule SporadicTaskset Job.
 
   Section SchedulableDefs.
-    
+
+    (* Assume that the cost and deadline of a job is known. *)
     Context {Job: eqType}.
     Context {arr_seq: arrival_sequence Job}.
     Variable job_cost: Job -> nat.
@@ -14,13 +16,14 @@ Module Schedulability.
   
     Section ScheduleOfJobs.
 
+      (* For any job j in schedule sched, ...*)
       Context {num_cpus: nat}.
       Variable rate: Job -> processor num_cpus -> nat.
       Variable sched: schedule num_cpus arr_seq.
 
       Variable j: JobIn arr_seq.
 
-      (* Job won't miss its deadline if it is completed by its arrival time plus its (relative) deadline. *)
+      (* job j misses no deadline in sched if it completed by its absolute deadline. *)
       Definition job_misses_no_deadline :=
         completed job_cost rate sched j (job_arrival j + job_deadline j).
 
@@ -35,19 +38,20 @@ Module Schedulability.
       Variable rate: Job -> processor num_cpus -> nat.
       Variable sched: schedule num_cpus arr_seq.
 
-      Variable ts: taskset_of sporadic_task.
+      (* Consider any task tsk. *)
       Variable tsk: sporadic_task.
 
-      (* A task doesn't miss its deadline iff all of its jobs don't miss their deadline. *)
+      (* Task tsk doesn't miss its deadline iff all of its jobs don't miss their deadline. *)
       Definition task_misses_no_deadline :=
         forall (j: JobIn arr_seq),
-          job_task j == tsk ->
+          job_task j = tsk ->
           job_misses_no_deadline rate sched j.
 
-      (* Whether a task misses a deadline before a particular time. *)
+      (* Task tsk doesn't miss its deadline before time t' iff all of its jobs don't miss
+         their deadline by that time. *)
       Definition task_misses_no_deadline_before (t': time) :=
         forall (j: JobIn arr_seq),
-          job_task j == tsk ->
+          job_task j = tsk ->
           job_arrival j + job_deadline j < t' ->
           job_misses_no_deadline rate sched j.
 
@@ -55,4 +59,113 @@ Module Schedulability.
 
   End SchedulableDefs.
 
+  Section BasicLemmas.
+
+    Context {sporadic_task: eqType}.
+    Variable task_cost: sporadic_task -> nat.
+    Variable task_period: sporadic_task -> nat.
+    Variable task_deadline: sporadic_task -> nat.
+    
+    Context {Job: eqType}.
+    Variable job_cost: Job -> nat.
+    Variable job_deadline: Job -> nat.
+    Variable job_task: Job -> sporadic_task.
+
+    Context {arr_seq: arrival_sequence Job}.
+    
+    (* Consider any valid schedule... *)
+    Context {num_cpus : nat}.
+    Variable sched: schedule num_cpus arr_seq.
+    Variable rate: Job -> processor num_cpus -> nat.
+
+    (* ... where jobs dont execute after completion. *)
+    Hypothesis H_completed_jobs_dont_execute:
+      completed_jobs_dont_execute job_cost rate sched.
+
+    Section SpecificJob.
+
+      (* Then, for any job j ...*)
+      Variable j: JobIn arr_seq.
+      
+      (* ...that doesn't miss a deadline in this schedule, ... *)
+      Hypothesis no_deadline_miss:
+        job_misses_no_deadline job_cost job_deadline rate sched j.
+
+      (* the service received by j at any time t' after its deadline is 0. *)
+      Lemma service_after_job_deadline_zero :
+        forall t',
+          t' >= job_arrival j + job_deadline j ->
+          service_at rate sched j t' = 0.
+      Proof.
+        intros t' LE.
+        rename no_deadline_miss into NOMISS,
+               H_completed_jobs_dont_execute into EXEC.
+        unfold job_misses_no_deadline, completed, completed_jobs_dont_execute in *.
+        apply/eqP; rewrite -leqn0.
+        rewrite <- leq_add2l with (p := job_cost j).
+        move: NOMISS => /eqP NOMISS; rewrite -{1}NOMISS addn0.
+        apply leq_trans with (n := service rate sched j t'.+1); last by apply EXEC.
+        unfold service; rewrite -> big_cat_nat with
+                                   (p := t'.+1) (n := job_arrival j + job_deadline j);
+            [rewrite leq_add2l /= | by ins | by apply ltnW].
+          by rewrite big_nat_recr // /=; apply leq_addl.
+      Qed.
+
+      (* The same applies for the cumulative service of job j. *)
+      Lemma cumulative_service_after_job_deadline_zero :
+        forall t' t'',
+          t' >= job_arrival j + job_deadline j ->
+          \sum_(t' <= t < t'') service_at rate sched j t = 0.
+      Proof.
+        ins; apply/eqP; rewrite -leqn0.
+        rewrite big_nat_cond; rewrite -> eq_bigr with (F2 := fun i => 0);
+          first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
+        intro i; rewrite andbT; move => /andP [LE _].
+        by rewrite service_after_job_deadline_zero;
+          [by ins | by apply leq_trans with (n := t')].
+      Qed.
+      
+    End SpecificJob.
+    
+    Section AllJobs.
+
+      (* Consider any task tsk ...*)
+      Variable tsk: sporadic_task.
+
+      (* ... that doesn't miss any deadline. *)
+      Hypothesis no_deadline_misses:
+        task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
+
+      (* Then, for any valid job j of this task, ...*)
+      Variable j: JobIn arr_seq.
+      Hypothesis H_job_of_task: job_task j = tsk.
+      Hypothesis H_valid_job:
+        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+      
+      (* the service received by job j at any time t' after the deadline is 0. *)
+      Lemma service_after_task_deadline_zero :
+        forall t',
+          t' >= job_arrival j + task_deadline tsk ->
+          service_at rate sched j t' = 0.
+      Proof.
+        rename H_valid_job into PARAMS; unfold valid_sporadic_job in *; des; intros t'.
+        rewrite -H_job_of_task -PARAMS1.
+        by apply service_after_job_deadline_zero, no_deadline_misses.
+      Qed.
+
+      (* The same applies for the cumulative service of job j. *)
+      Lemma cumulative_service_after_task_deadline_zero :
+        forall t' t'',
+          t' >= job_arrival j + task_deadline tsk ->
+          \sum_(t' <= t < t'') service_at rate sched j t = 0.
+      Proof.
+        rename H_valid_job into PARAMS; unfold valid_sporadic_job in *; des; intros t' t''.
+        rewrite -H_job_of_task -PARAMS1.
+        by apply cumulative_service_after_job_deadline_zero, no_deadline_misses.
+      Qed.
+      
+    End AllJobs.
+
+  End BasicLemmas.
+
 End Schedulability.
\ No newline at end of file

task_arrival.v

 Require Import Vbase task job schedule util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
+(* Properties of the job arrival. *)
 Module SporadicTaskArrival.
 
 Import SporadicTaskset Schedule.
   
   Section ArrivalModels.
 
+    (* Assume the task period is known. *)
     Context {sporadic_task: eqType}.
     Variable task_period: sporadic_task -> nat.
     
@@ -14,13 +16,14 @@ Import SporadicTaskset Schedule.
     Variable arr_seq: arrival_sequence Job.
     Variable job_task: Job -> sporadic_task.
 
-    (* We define the sporadic task model *)
+    (* Then, we define the sporadic task model as follows.*)
+    
     Definition sporadic_task_model :=
       forall (j j': JobIn arr_seq),
-             j <> j' -> (* Given two different jobs j and j' such that ... *)
-             job_task j = job_task j' -> (* ...they are from the same task ... *)
-             job_arrival j <= job_arrival j' -> (* ...and arr <= arr'...  *)
-        (* then the next jobs arrives 'period' time units later. *)
+             j <> j' -> (* Given two different jobs j and j' ... *)
+             job_task j = job_task j' -> (* ... of 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_period (job_task j).
 
   End ArrivalModels.