diff --git a/model/schedule/uni/nonpreemptive/platform.v b/model/schedule/uni/nonpreemptive/platform.v
new file mode 100644
index 0000000000000000000000000000000000000000..45b8a76f6230a758ccf1433df52f9951e40a9be9
--- /dev/null
+++ b/model/schedule/uni/nonpreemptive/platform.v
@@ -0,0 +1,121 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
+Require Import rt.model.schedule.uni.schedule
+ rt.model.schedule.uni.basic.platform.
+Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+Module NonpreemptivePlatform.
+
+ Import Job SporadicTaskset UniprocessorSchedule Priority.
+
+ (* In this section, we define properties of the processor platform. *)
+ Section Properties.
+
+ Context {sporadic_task: eqType}.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+ Variable job_task: Job -> sporadic_task.
+
+ (* Consider any job arrival sequence ...*)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* ...and any uniprocessor schedule of these jobs. *)
+ Variable sched: schedule Job.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_completed_by := completed_by job_cost sched.
+ Let job_scheduled_at := scheduled_at sched.
+
+ (* First, we define the notion of a preemption point. *)
+ Section PreemptionPoint.
+
+ (* We say that t is a preemption point iff (a) t is equal to 0
+ or (b) there is no scheduling job at time t or
+ (c) a job that was scheduled at time (t - 1) and
+ has completed by t exists. *)
+ Definition is_preemption_point' (t: time) :=
+ t = 0
+ \/ sched (t-1) = None
+ \/ exists j, scheduled_at sched j (t - 1) /\ job_completed_by j t.
+
+ (* Moreover, we provide a shorter definition, more convenient for the proofs. *)
+ Definition is_preemption_point (t: time) :=
+ t = 0 \/ forall j, job_scheduled_at j (t - 1) -> job_completed_by j t.
+
+ (* Let's prove that the definitions above are equal. *)
+ Lemma defitions_of_preemption_point_are_equal:
+ forall t, is_preemption_point t <-> is_preemption_point' t.
+ Proof.
+ unfold is_preemption_point, is_preemption_point'.
+ intros; split; intros.
+ {
+ destruct H as [H | H]; [by left | right].
+ destruct (sched (t-1)) eqn:SCHED; [right; exists s | by left].
+ move: SCHED => /eqP SCHED.
+ by split; last by apply H in SCHED.
+ }
+ {
+ destruct H as [H | [H | H]]; [by left| | ]; right; intros.
+ unfold job_scheduled_at, scheduled_at in H0. rewrite H in H0. inversion H0.
+ inversion H as [j' [H1 H2]]. unfold job_scheduled_at in H0.
+ have EQ: j = j'. by apply (only_one_job_scheduled sched) with (t := t-1).
+ by subst j'.
+ }
+ Qed.
+
+ End PreemptionPoint.
+
+ (* Next, we define properties related to execution. *)
+ Section Execution.
+
+ (* We say that a scheduler is work-conserving iff whenever a job j
+ is backlogged, the processor is always busy with another job. *)
+ (* Imported from the preemptive schedule. *)
+ Definition work_conserving := Platform.work_conserving job_cost.
+
+ End Execution.
+
+ (* Next, we define properties related to FP scheduling. *)
+ Section FP.
+
+ (* We say that an FP policy...*)
+ Variable higher_eq_priority: FP_policy sporadic_task.
+
+ (* ...is respected by the schedule iff a scheduled task has
+ higher (or same) priority than (as) any backlogged task at
+ every preemption point. *)
+ Definition respects_FP_policy_at_preemption_point :=
+ forall j j_hp t,
+ arrives_in arr_seq j ->
+ backlogged job_arrival job_cost sched j t ->
+ scheduled_at sched j_hp t ->
+ is_preemption_point t ->
+ higher_eq_priority (job_task j_hp) (job_task j).
+
+ End FP.
+
+ (* Next, we define properties related to JLFP policies. *)
+ Section JLFP.
+
+ (* We say that a JLFP policy ...*)
+ Variable higher_eq_priority: JLFP_policy Job.
+
+ (* ... is respected by the scheduler iff a scheduled job has
+ higher (or same) priority than (as) any backlogged job at
+ every preemption point. *)
+ Definition respects_JLFP_policy_at_preemption_point :=
+ forall j j_hp t,
+ arrives_in arr_seq j ->
+ backlogged job_arrival job_cost sched j t ->
+ scheduled_at sched j_hp t ->
+ is_preemption_point t ->
+ higher_eq_priority j_hp j.
+
+ End JLFP.
+
+ End Properties.
+
+End NonpreemptivePlatform.
\ No newline at end of file
diff --git a/model/schedule/uni/nonpreemptive/schedule.v b/model/schedule/uni/nonpreemptive/schedule.v
new file mode 100644
index 0000000000000000000000000000000000000000..f22542c0c65f9c0b540f22bff33f3c990babe009
--- /dev/null
+++ b/model/schedule/uni/nonpreemptive/schedule.v
@@ -0,0 +1,383 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job.
+Require Import rt.model.schedule.uni.schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module NonpreemptiveSchedule.
+
+ Export UniprocessorSchedule.
+
+ Section Definitions.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+
+ (* Consider any uniprocessor schedule. *)
+ Variable sched: schedule Job.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_completed_by := completed_by job_cost sched.
+ Let job_remaining_cost j t := remaining_cost job_cost sched j t.
+
+ (* We define schedule to be nonpreemptive iff every job remains scheduled until completion. *)
+ Definition is_nonpreemptive_schedule :=
+ forall j t t',
+ t <= t' ->
+ scheduled_at sched j t ->
+ ~~ job_completed_by j t' ->
+ scheduled_at sched j t'.
+
+ (* In this section, we prove some basic lemmas about nonpreemptive schedules. *)
+ Section Lemmas.
+
+ (* Assume that we have a nonpreemptive schedule. *)
+ Hypothesis H_nonpreemptive: is_nonpreemptive_schedule.
+
+ Section BasicLemmas.
+
+ (* Consider any job j. *)
+ Variable j: Job.
+
+ (* Assume that completed jobs do not execute. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* First, we show that if j is scheduled at any two time instants,
+ then it is also scheduled at any time between them. *)
+ Lemma continuity_of_nonpreemptive_scheduling:
+ forall t t1 t2,
+ t1 <= t <= t2 ->
+ scheduled_at sched j t1 ->
+ scheduled_at sched j t2 ->
+ scheduled_at sched j t.
+ Proof.
+ move => t t1 t2 /andP [GT LE] SCHEDt1 SCHEDt2.
+ unfold is_nonpreemptive_schedule, job_completed_by in *.
+ apply H_nonpreemptive with (t := t1); [by done| by done| ].
+ apply /negP; intros COMP.
+ apply (scheduled_implies_not_completed job_cost) in SCHEDt2; last by done.
+ apply completion_monotonic with (t' := t2) in COMP; [ |by done| by done].
+ by move: SCHEDt2 => /negP SCHEDt2; apply: SCHEDt2.
+ Qed.
+
+ (* Next, we show that in any nonpreemptive schedule, once a job is scheduled,
+ it cannot be preempted until completion. *)
+ Lemma in_nonpreemption_schedule_preemption_implies_completeness:
+ forall t t' ,
+ t <= t' ->
+ scheduled_at sched j t ->
+ ~~ scheduled_at sched j t' ->
+ job_completed_by j t'.
+ Proof.
+ intros t t' LE SCHED; apply contraNT.
+ by apply H_nonpreemptive with (t := t).
+ Qed.
+
+ End BasicLemmas.
+
+ (* In this section, we prove properties related to job completion. *)
+ Section CompletionUnderNonpreemptive.
+
+ (* Assume that completed jobs do not execute. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* If job j is scheduled at time t, then it must complete by (t + remaining_cost j t). *)
+ Lemma job_completes_after_remaining_cost:
+ forall j t,
+ scheduled_at sched j t ->
+ job_completed_by j (t + job_remaining_cost j t).
+ Proof.
+ intros j t SCHED.
+ rewrite /job_completed_by /completed_by eqn_leq.
+ apply /andP; split;
+ first by apply cumulative_service_le_job_cost.
+ rewrite /service /service_during.
+ rewrite (@big_cat_nat _ _ _ t) //= ?leq_addr //.
+ apply leq_trans with (n := service sched j t + job_remaining_cost j t);
+ first by rewrite /remaining_cost subnKC //.
+ rewrite leq_add2l.
+ set t2 := t + _.
+ apply leq_trans with (n := \sum_(t <= i < t2) 1);
+ first by simpl_sum_const; rewrite /t2 addKn.
+ apply leq_sum_nat.
+ move => i /andP [GE LT _].
+ rewrite lt0n eqb0 negbK.
+ apply (H_nonpreemptive j t i); try (by done).
+ unfold t2 in *; clear t2.
+ have NOTCOMP: ~~ job_completed_by j t.
+ {
+ apply contraT. rewrite negbK. intros COMP.
+ apply completed_implies_not_scheduled in COMP; last by done.
+ by rewrite SCHED in COMP.
+ }
+ apply job_doesnt_complete_before_remaining_cost in NOTCOMP; last by done.
+ apply contraT; rewrite negbK; intros COMP.
+ exfalso; move: NOTCOMP => /negP NOTCOMP; apply: NOTCOMP.
+ apply completion_monotonic with (t0 := i); try ( by done).
+ apply subh3; first by rewrite addn1.
+ by apply leq_ltn_trans with (n := i).
+ Qed.
+
+ End CompletionUnderNonpreemptive.
+
+ (* In this section, we determine bounds on the length of the execution interval. *)
+ Section ExecutionInterval.
+
+ (* Assume that jobs do not execute after completion. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* Let j be any job scheduled at time t. *)
+ Variable j: Job.
+ Variable t: time.
+ Hypothesis H_j_is_scheduled_at_t: scheduled_at sched j t.
+
+ (* Is this section we show that there is a bound for how early job j can start. *)
+ Section LeftBound.
+
+ (* We prove that job j is scheduled at time (t - service sched j t)... *)
+ Lemma j_is_scheduled_at_t_minus_service:
+ scheduled_at sched j (t - service sched j t).
+ Proof.
+ unfold is_nonpreemptive_schedule in *.
+ apply contraT; intros CONTRA; exfalso.
+ rename H_j_is_scheduled_at_t into SCHED.
+
+ have COSTPOS: job_cost j > 0.
+ {
+ apply (scheduled_implies_not_completed job_cost) in SCHED.
+ unfold job_completed_by, completed_by in SCHED.
+ apply contraT; rewrite -eqn0Ngt.
+ move => /eqP EQ0.
+ rewrite EQ0 in SCHED.
+ move: SCHED => /eqP GT0.
+ exfalso; apply: GT0; apply /eqP.
+ rewrite eqn_leq.
+ apply /andP; split; last by done.
+ rewrite -EQ0.
+ apply H_completed_jobs_dont_execute.
+ by done.
+ }
+
+ have H := job_completes_after_remaining_cost
+ H_completed_jobs_dont_execute
+ j t SCHED.
+
+ unfold job_completed_by, completed_by in H.
+ move: H => /eqP H.
+
+ unfold service, service_during in H.
+
+ rewrite
+ (@big_cat_nat _ _ _ (t - service sched j t)) //= in H;
+ last by rewrite leq_subLR addnC -addnA leq_addr.
+ have R: forall a b c, a + b = c -> b < c -> a > 0.
+ {
+ by intros a b c EQ LT; induction a;
+ first by rewrite add0n in EQ; subst b;
+ rewrite ltnn in LT.
+ }
+
+ apply R in H; last first.
+ {
+ have CUMLED := cumulative_service_le_delta sched j 0 t.
+ have CUMLEJC := cumulative_service_le_job_cost _ _ H_completed_jobs_dont_execute j 0 t.
+ rewrite (@big_cat_nat _ _ _ ((t - service sched j t).+1)) //=.
+ {
+ rewrite big_nat_recl; last by done.
+ rewrite big_geq; last by done.
+ rewrite -eqb0 in CONTRA; move: CONTRA => /eqP CONTRA.
+ rewrite /service_at CONTRA add0n add0n.
+ apply leq_ltn_trans with
+ (t + job_remaining_cost j t - ((t - service sched j t).+1)).
+ set (t - service sched j t).+1 as T.
+ apply leq_trans with (\sum_(T <= i < t + job_remaining_cost j t) 1).
+ rewrite leq_sum //; intros; by destruct (scheduled_at sched j i).
+ simpl_sum_const. by done.
+ unfold job_remaining_cost, remaining_cost.
+ rewrite -addn1 -addn1 subh1; first by
+ by rewrite leq_subLR addnBA;
+ first by rewrite -addnA [1+job_cost j]addnC addnA -subh1.
+ {
+ rewrite subh1; last by done.
+ rewrite leq_subLR addnA.
+ rewrite addnBA; last by done.
+ rewrite [_+t]addnC [_+job_cost j]addnC addnA.
+ rewrite -addnBA; last by done.
+ by rewrite subnn addn0 addnC leq_add2r.
+ }
+ }
+ {
+ unfold remaining_cost.
+ rewrite addnBA; last by done.
+ rewrite -addn1 subh1; last by done.
+ rewrite leq_subLR -addnBA; last by done.
+ rewrite addnA [_+t]addnC -addnA leq_add2l addnBA; last by done.
+ by rewrite addnC -addnBA; first by rewrite subnn addn0.
+ }
+ }
+ {
+ rewrite lt0n in H; move: H => /neqP H; apply: H.
+ rewrite big_nat_cond big1 //; move => i /andP [/andP [_ LT] _].
+ apply /eqP; rewrite eqb0; apply /negP; intros CONT.
+
+ have Y := continuity_of_nonpreemptive_scheduling j _ (t - service sched j t) i t.
+ feed_n 4 Y; try(done).
+ by apply/andP; split; [rewrite ltnW | rewrite leq_subr].
+ by move: CONTRA => /negP CONTRA; apply CONTRA.
+ }
+ Qed.
+
+ (* ... and it is not scheduled at time (t - service sched j t - 1). *)
+ Lemma j_is_not_scheduled_at_t_minus_service_minus_one:
+ t - service sched j t > 0 ->
+ ~~ scheduled_at sched j (t - service sched j t - 1).
+ Proof.
+ rename H_j_is_scheduled_at_t into SCHED.
+ intros GT; apply/negP; intros CONTRA.
+
+ have L1 := job_doesnt_complete_before_remaining_cost
+ job_cost sched H_completed_jobs_dont_execute
+ j t.
+ feed L1; first by rewrite scheduled_implies_not_completed.
+
+ have L2 := job_completes_after_remaining_cost
+ H_completed_jobs_dont_execute
+ j (t-service sched j t - 1).
+ feed L2; first by done.
+
+ have EQ:
+ t + job_remaining_cost j t - 1 =
+ t - service sched j t - 1 + job_remaining_cost j (t - service sched j t - 1).
+ {
+ have T1: service sched j (t - service sched j t - 1) = 0.
+ {
+
+ rewrite [service _ _ _]/service /service_during.
+ rewrite big_nat_cond big1 //; move => t' /andP [/andP [_ LT] _].
+ apply /eqP; rewrite eqb0; apply /negP; intros CONTR.
+
+ have COMPL: completed_by job_cost sched j (t + job_remaining_cost j t - 1).
+ {
+ apply completion_monotonic with (t0 := t' + job_remaining_cost j t');
+ [by done | | by apply job_completes_after_remaining_cost].
+
+ unfold remaining_cost.
+
+ have LLF: t' < t - service sched j t.
+ {
+ by apply ltn_trans with (t - service sched j t - 1);
+ last by rewrite -addn1 subh1 // -addnBA // subnn addn0.
+ } clear LT.
+
+ rewrite !addnBA;
+ try(rewrite H_completed_jobs_dont_execute //).
+ rewrite [t' + _]addnC [t + _]addnC.
+ rewrite -addnBA; last by rewrite cumulative_service_le_delta.
+ rewrite -addnBA; last by rewrite cumulative_service_le_delta.
+ rewrite -addnBA ?leq_add2l; last by done.
+ by apply leq_trans with (t' + 1 - 1);
+ rewrite addn1 subn1 -pred_Sn;
+ [rewrite leq_subr | rewrite subh3 // addn1].
+ }
+
+ have L3 := job_doesnt_complete_before_remaining_cost job_cost sched
+ H_completed_jobs_dont_execute j t;
+ feed L3; first by rewrite scheduled_implies_not_completed.
+ unfold job_completed_by in *.
+ by move: L3 => /negP L3; apply L3.
+ }
+ rewrite /job_remaining_cost /remaining_cost T1 subn0 addnBA; last by done.
+ rewrite -subh1.
+ by rewrite -[(t-service sched j t) + _ - _]subh1.
+ by rewrite cumulative_service_le_delta.
+ }
+ move: L1 => /neqP L1; apply: L1.
+ rewrite -EQ in L2.
+ by unfold job_completed_by, completed_by in L2; move: L2 => /eqP L2.
+ Qed.
+
+ (* Using the previous lemma, we show that job j cannot be scheduled
+ before (t - service sched j t). *)
+ Lemma j_is_not_scheduled_earlier_t_minus_service:
+ forall t',
+ t' < t - service sched j t ->
+ ~~ scheduled_at sched j t'.
+ Proof.
+ intros t' GT.
+ have NOTSCHED := j_is_not_scheduled_at_t_minus_service_minus_one;
+ feed NOTSCHED; first by apply leq_ltn_trans with t'.
+ apply/negP; intros CONTRA.
+ move: NOTSCHED => /negP NOTSCHED; apply: NOTSCHED.
+ apply continuity_of_nonpreemptive_scheduling with (t1 := t') (t2 := t);
+ [ by done | | by done | by done ].
+ apply/andP; split; last by apply leq_trans with (t - service sched j t); rewrite leq_subr.
+ rewrite [t']pred_Sn -subn1 leq_sub2r //.
+ Qed.
+
+ End LeftBound.
+
+ (* Is this section we prove that job j cannot be scheduled after (t + remaining_cost j t - 1). *)
+ Section RightBound.
+
+ (* We show that if job j is scheduled at time t,
+ then it is also scheduled at time (t + remaining_cost j t - 1)... *)
+ Lemma j_is_scheduled_at_t_plus_remaining_cost_minus_one:
+ scheduled_at sched j (t + job_remaining_cost j t - 1).
+ Proof.
+ move: (H_j_is_scheduled_at_t) => COMP.
+ apply (scheduled_implies_not_completed job_cost) in COMP; last by done.
+ apply job_doesnt_complete_before_remaining_cost in COMP; last by done.
+ move: COMP; apply contraR; intros CONTR.
+ apply in_nonpreemption_schedule_preemption_implies_completeness
+ with (t:=t); [|by done| by done].
+ rewrite subh3 // ?leq_add2l;
+ first by rewrite scheduled_implies_positive_remaining_cost //.
+ rewrite addn_gt0; apply/orP; right;
+ rewrite scheduled_implies_positive_remaining_cost //.
+ Qed.
+
+ (* ... and it is not scheduled after (t + remaining cost j t - 1). *)
+ Lemma j_is_not_scheduled_after_t_plus_remaining_cost_minus_one:
+ forall t',
+ t + job_remaining_cost j t <= t' ->
+ ~~ scheduled_at sched j t'.
+ Proof.
+ intros t' GE.
+ unfold job_completed_by in *.
+ rename H_j_is_scheduled_at_t into SCHED.
+ apply job_completes_after_remaining_cost in SCHED; last by done.
+ by apply (completion_monotonic job_cost) with (t' := t') in SCHED; first
+ by apply (completed_implies_not_scheduled job_cost).
+ Qed.
+
+ End RightBound.
+
+ (* To conclude, we identify the interval where job j is scheduled. *)
+ Lemma nonpreemptive_executing_interval:
+ forall t',
+ t - service sched j t <= t' < t + job_remaining_cost j t ->
+ scheduled_at sched j t'.
+ Proof.
+ move => t' /andP [GE LE].
+ move: (H_j_is_scheduled_at_t) => SCHED1; move: (H_j_is_scheduled_at_t) => SCHED2.
+ rewrite -addn1 in LE; apply subh3 with (m := t') (p := 1) in LE;
+ last by rewrite addn_gt0; apply/orP; right;
+ rewrite scheduled_implies_positive_remaining_cost //.
+ apply continuity_of_nonpreemptive_scheduling with
+ (t1 := t - service sched j t)
+ (t2 := t + job_remaining_cost j t - 1); first by done.
+ - by apply/andP;split.
+ - by apply j_is_scheduled_at_t_minus_service.
+ - by apply j_is_scheduled_at_t_plus_remaining_cost_minus_one.
+ Qed.
+
+ End ExecutionInterval.
+
+ End Lemmas.
+
+ End Definitions.
+
+End NonpreemptiveSchedule.
\ No newline at end of file
diff --git a/model/schedule/uni/schedule.v b/model/schedule/uni/schedule.v
index 3ab7a3e9491c92d3f12246461e33fadcaeb23a36..806426fa99c7ce61670e0a1d40e498486af7cbbd 100644
--- a/model/schedule/uni/schedule.v
+++ b/model/schedule/uni/schedule.v
@@ -8,7 +8,7 @@ Module UniprocessorSchedule.
Export Time ArrivalSequence.
Section Schedule.
-
+
(* We begin by defining a uniprocessor schedule. *)
Section ScheduleDef.
@@ -60,9 +60,14 @@ Module UniprocessorSchedule.
(* Job j is pending at time t iff it has arrived but has not yet completed. *)
Definition pending (t: time) := has_arrived job_arrival j t && ~~ completed_by 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 (t: time) :=
+ arrived_before job_arrival j t && ~~ completed_by t.
+
(* Job j is backlogged at time t iff it is pending and not scheduled. *)
Definition backlogged (t: time) := pending t && ~~ scheduled_at t.
-
+
End JobProperties.
(* In this section, we define some properties of the processor. *)
@@ -80,6 +85,25 @@ Module UniprocessorSchedule.
Definition total_service (t2: time) := total_service_during 0 t2.
End ProcessorProperties.
+
+ Section PropertyOfSequentiality.
+
+ Context {Task: eqType}.
+ Variable job_task: Job -> Task.
+
+ (* We say that two jobs j1 and j2 are from the same task, if job_task j1 is equal to job_task j2. *)
+ Let same_task j1 j2 := job_task j1 == job_task j2.
+
+ (* We say that the jobs are sequential if they are executed
+ in the order they arrived. *)
+ Definition sequential_jobs :=
+ forall j1 j2 t,
+ same_task j1 j2 ->
+ job_arrival j1 < job_arrival j2 ->
+ scheduled_at j2 t ->
+ completed_by j1 t.
+
+ End PropertyOfSequentiality.
End ScheduleProperties.
@@ -117,6 +141,11 @@ Module UniprocessorSchedule.
(* Consider any uniprocessor schedule. *)
Variable sched: schedule Job.
+ (* 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 sched j t.
+
(* Let's begin with lemmas about service. *)
Section Service.
@@ -142,6 +171,24 @@ Module UniprocessorSchedule.
by apply leq_sum; intros t0 _; apply leq_b1.
Qed.
+ (* Assume that completed jobs do not execute. *)
+ Hypothesis H_completed_jobs:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* Note that if a job scheduled at some time t then remaining
+ cost at this point is positive *)
+ Lemma scheduled_implies_positive_remaining_cost:
+ forall t,
+ scheduled_at sched j t ->
+ remaining_cost j t > 0.
+ Proof.
+ intros.
+ 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.
+ by rewrite big_nat_recr //= -addn1 leq_add2l lt0b.
+ Qed.
+
End Service.
(* Next, we prove properties related to job completion. *)
@@ -160,7 +207,7 @@ Module UniprocessorSchedule.
t <= t' ->
completed_by job_cost sched j t ->
completed_by job_cost sched j t'.
- Proof.
+ Proof.
unfold completed_by; move => t t' LE /eqP COMPt.
rewrite eqn_leq; apply/andP; split; first by apply H_completed_jobs.
rewrite- COMPt; by apply extend_sum.
@@ -182,6 +229,29 @@ Module UniprocessorSchedule.
apply leq_add; first by move: COMPLETED => /eqP <-.
by rewrite /service_at SCHED.
Qed.
+
+ (* ... and that a scheduled job cannot be completed. *)
+ Lemma scheduled_implies_not_completed:
+ forall t,
+ scheduled_at sched j t ->
+ ~~ completed_by job_cost sched j t.
+ Proof.
+ rename H_completed_jobs into COMP.
+ unfold completed_jobs_dont_execute in COMP.
+ move => t SCHED.
+ rewrite /completed_by neq_ltn.
+ apply /orP; left.
+ apply leq_trans with (service sched j t.+1); last by done.
+ rewrite /service /service_during.
+ rewrite [in X in _ < X] (@big_cat_nat _ _ _ t) //=.
+ rewrite -[\sum_(0 <= t0 < t) service_at sched j t0]addn0;
+ rewrite -addnA ltn_add2l addnC addn0 big_nat1.
+ rewrite lt0n; apply/neqP; intros CONT;
+ move: CONT => /eqP CONT; rewrite eqb0 in CONT;
+ move: CONT => /neqP CONT; apply CONT;
+ unfold scheduled_at in SCHED; move: SCHED => /eqP SCHED;
+ by rewrite SCHED.
+ Qed.
(* Next, we show that the service received by job j in any interval
is no larger than its cost. *)
@@ -198,7 +268,113 @@ Module UniprocessorSchedule.
rewrite -> big_cat_nat with (m := 0) (n := t);
[by apply leq_addl | by ins | by rewrite leqNgt negbT //].
Qed.
-
+
+ (* If a job isn't complete at time t,
+ it can't be completed at time (t + remaining_cost j t - 1). *)
+ Lemma job_doesnt_complete_before_remaining_cost:
+ forall t,
+ ~~ completed_by job_cost sched j t ->
+ ~~ completed_by job_cost sched j (t + remaining_cost j t - 1).
+ Proof.
+ intros t GT0.
+ unfold remaining_cost, completed_by in *.
+ have COSTGT0: job_cost j > 0.
+ {
+ apply contraT; rewrite -eqn0Ngt.
+ move => /eqP EQ0.
+ rewrite EQ0 in GT0.
+ move: GT0 => /eqP GT0.
+ exfalso; apply: GT0; apply /eqP.
+ rewrite eqn_leq.
+ apply /andP; split; last by done.
+ by rewrite -EQ0.
+ }
+ rewrite neq_ltn; apply /orP; left.
+ rewrite /service /service_during.
+ set delta := (X in (t + X - 1)).
+ have NONZERO: delta > 0.
+ {
+ rewrite neq_ltn in GT0.
+ move: GT0 => /orP [LTcost | GTcost]; first by rewrite ltn_subRL addn0.
+ exfalso.
+ rewrite ltnNge in GTcost; move: GTcost => /negP GTcost.
+ by apply GTcost.
+ }
+ rewrite (@big_cat_nat _ _ _ t) //= ?leq_addr //;
+ last by rewrite -addnBA; [rewrite leq_addr | done].
+ apply leq_ltn_trans with (n := service sched j t + \sum_(t <= i < t + delta - 1) 1);
+ first by rewrite leq_add2l; apply leq_sum; intros; apply leq_b1.
+ simpl_sum_const.
+ rewrite -addnBA // addKn.
+ rewrite addnBA // /delta.
+ rewrite subnKC; last by done.
+ rewrite subn1 -(ltn_add2r 1) addn1.
+ by rewrite prednK // addn1 ltnSn.
+ Qed.
+
+ (* In this section, we prove that the job with a positive
+ cost must be scheduled to be completed. *)
+ Section JobMustBeScheduled.
+
+ (* We assume that job j has positive cost, from which we can
+ infer that there always is a time in which j is pending. *)
+ Hypothesis H_positive_cost: job_cost j > 0.
+
+ (* Assume that jobs must arrive to execute. *)
+ Hypothesis H_jobs_must_arrive:
+ jobs_must_arrive_to_execute job_arrival sched.
+
+ (* Then, we prove that the job with a positive cost
+ must be scheduled to be completed. *)
+ Lemma completed_implies_scheduled_before:
+ forall t,
+ completed_by job_cost sched j t ->
+ exists t',
+ job_arrival j <= t' < t
+ /\ scheduled_at sched j t'.
+ Proof.
+ intros t COMPL.
+ induction t.
+ {
+ exfalso.
+ unfold completed_by, service, service_during in COMPL.
+ move: COMPL; rewrite big_geq //; move => /eqP H0.
+ by destruct (job_cost j).
+ }
+
+ destruct (completed_by job_cost sched j t) eqn:COMPLatt.
+ {
+ feed IHt; first by done.
+ move: IHt => [t' [JA SCHED]].
+ exists t'. split; first apply/andP; first split.
+ - by apply H_jobs_must_arrive in SCHED.
+ - move: JA => /andP [_ LT]. by apply leq_trans with t.
+ - by done.
+ }
+ {
+ clear IHt.
+ apply negbT in COMPLatt. unfold completed_by in *.
+ rewrite neq_ltn in COMPLatt; move: COMPLatt => /orP [LT | F].
+ {
+ unfold service, service_during in COMPL.
+ rewrite big_nat_recr //= in COMPL.
+ move: COMPL => /eqP COMPL. rewrite -COMPL -addn1 leq_add2l in LT.
+ rewrite lt0b in LT.
+
+ exists t; split.
+ - by apply/andP; by split; first by apply H_jobs_must_arrive in LT.
+ - by done.
+ }
+ {
+ exfalso.
+ rewrite ltnNge in F. move: F => /negP F. apply F.
+ apply H_completed_jobs.
+ }
+ }
+ Qed.
+
+ End JobMustBeScheduled.
+
End Completion.
(* In this section we prove properties related to job arrivals. *)
@@ -476,5 +652,5 @@ Module UniprocessorSchedule.
End Lemmas.
End Schedule.
-
+
End UniprocessorSchedule.
\ No newline at end of file