Require Import Vbase job task util_lemmas arrival_sequence ssreflect ssrbool eqtype ssrnat seq fintype bigop. (* Definition, properties and lemmas about schedules. *) Module Schedule. Export ArrivalSequence. (* A processor is defined as a bounded natural number: [0, num_cpus). *) Definition processor (num_cpus: nat) := 'I_num_cpus. Section ScheduleDef. Context {Job: eqType}. (* Given the number of processors and an arrival sequence, ...*) Variable num_cpus: nat. Variable arr_seq: arrival_sequence Job. (* ... we define a schedule as a mapping such that each processor at each time contains either a job from the sequence or none. *) Definition schedule := processor num_cpus -> time -> option (JobIn arr_seq). End ScheduleDef. (* Next, we define properties of jobs in a schedule. *) Section ScheduledJobs. Context {Job: eqType}. (* Given an arrival sequence, ... *) Context {arr_seq: arrival_sequence Job}. Variable job_cost: Job -> nat. (* ... a job cost function, ... *) (* ... and the number of processors, ...*) Context {num_cpus: nat}. (* ... we define the following properties for job j in schedule sched. *) Variable sched: schedule num_cpus arr_seq. Variable j: JobIn arr_seq. (* A job j is scheduled at time t iff there exists a cpu where it is mapped.*) Definition scheduled (t: time) := [exists cpu in 'I_(num_cpus), sched cpu t == Some j]. (* A processor cpu is idle at time t if it doesn't contain any jobs. *) Definition is_idle (cpu: 'I_(num_cpus)) (t: time) := sched cpu t = None. (* The instantaneous service of job j at time t is the number of cpus where it is scheduled on. Note that we use a sum to account for parallelism if required. *) Definition service_at (t: time) := \sum_(cpu < num_cpus | sched cpu t == Some j) 1. (* The cumulative service received by job j during [0, t'). *) Definition service (t': time) := \sum_(0 <= t < t') service_at t. (* The cumulative service received by job j during [t1, t2). *) Definition service_during (t1 t2: time) := \sum_(t1 <= t < t2) service_at t. (* Job j has completed at time t if it received enough service. *) Definition completed (t: time) := service t == job_cost j. (* Job j is pending at time t iff it has arrived but has not completed. *) Definition pending (t: time) := has_arrived j t && ~~completed t. (* Job j is backlogged at time t iff it is pending and not scheduled. *) Definition backlogged (t: time) := pending t && ~~scheduled t. (* Job j is carry-in in interval [t1, t2) iff it arrives before t1 and is not complete at time t1 *) Definition carried_in (t1: time) := arrived_before j t1 && ~~ completed t1. (* Job j is carry-out in interval [t1, t2) iff it arrives after t1 and is not complete at time t2 *) Definition carried_out (t1 t2: time) := arrived_before j t2 && ~~ completed t2. (* The list of scheduled jobs at time t is the concatenation of the jobs scheduled on each processor. *) Definition jobs_scheduled_at (t: time) := \cat_(cpu < num_cpus) make_sequence (sched cpu t). (* The list of jobs scheduled during the interval [t1, t2) is the the duplicate-free concatenation of the jobs scheduled at instant. *) Definition jobs_scheduled_between (t1 t2: time) := undup (\cat_(t1 <= t < t2) jobs_scheduled_at t). End ScheduledJobs. (* In this section, we define properties of valid schedules. *) Section ValidSchedules. Context {Job: eqType}. (* Assume a job type with decidable equality, ...*) Context {arr_seq: arrival_sequence Job}. (* ..., an arrival sequence, ...*) Variable job_cost: Job -> nat. (* ... a cost function, .... *) (* ... and a schedule. *) Context {num_cpus: nat}. Variable sched: schedule num_cpus arr_seq. (* Next, we define whether job parallelism is disallowed, ... *) Definition jobs_dont_execute_in_parallel := forall j t cpu1 cpu2, sched cpu1 t = Some j -> sched cpu2 t = Some j -> cpu1 = cpu2. (* ... whether a job can only be scheduled if it has arrived, ... *) Definition jobs_must_arrive_to_execute := forall j t, scheduled sched j t -> has_arrived j t. (* ... whether a job can be scheduled after it completes. *) Definition completed_jobs_dont_execute := forall j t, service sched j t <= job_cost j. End ValidSchedules. (* In this section, we prove some basic lemmas about a job. *) Section JobLemmas. (* Consider an arrival sequence, ...*) Context {Job: eqType}. Context {arr_seq: arrival_sequence Job}. (* ... a job cost function, ...*) Variable job_cost: Job -> nat. (* ..., and a particular schedule. *) Context {num_cpus: nat}. Variable sched: schedule num_cpus arr_seq. (* Next, we prove some lemmas about the service received by a job j. *) Variable j: JobIn arr_seq. Section Basic. (* At any time t, job j is not scheduled iff it doesn't get service. *) Lemma not_scheduled_no_service : forall t, ~~ scheduled sched j t = (service_at sched j t == 0). Proof. unfold scheduled, service_at; intros t; apply/idP/idP. { intros NOTSCHED. rewrite negb_exists_in in NOTSCHED. move: NOTSCHED => /forall_inP NOTSCHED. rewrite big_seq_cond. rewrite -> eq_bigr with (F2 := fun i => 0); first by rewrite big_const_seq iter_addn mul0n addn0. move => cpu /andP [_ SCHED]. exploit (NOTSCHED cpu); [by ins | clear NOTSCHED]. by move: SCHED => /eqP SCHED; rewrite SCHED eq_refl. } { intros NOSERV; rewrite big_mkcond -sum_nat_eq0_nat in NOSERV. move: NOSERV => /allP ALL. rewrite negb_exists; apply/forall_inP. move => x /andP [IN SCHED]. by exploit (ALL x); [by apply mem_index_enum | by desf]. } Qed. (* If the cumulative service during a time interval is not zero, there must be a time t in this interval where the service is not 0. *) Lemma job_scheduled_during_interval : forall t1 t2, service_during sched j t1 t2 != 0 -> exists t, t1 <= t < t2 /\ service_at sched j t != 0. Proof. intros t1 t2 NONZERO. destruct ([exists t: 'I_t2, (t >= t1) && (service_at sched j t != 0)]) eqn:EX. { move: EX => /existsP EX; destruct EX as [x EX]. move: EX => /andP [GE SERV]. exists x; split; last by done. by apply/andP; split; [by done | apply ltn_ord]. } { apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP EX. unfold service_during in NONZERO; rewrite big_nat_cond in NONZERO. rewrite (eq_bigr (fun x => 0)) in NONZERO; first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 in NONZERO. intros i; rewrite andbT; move => /andP [GT LT]. specialize (EX (Ordinal LT)); simpl in EX. by rewrite GT andTb negbK in EX; apply/eqP. } Qed. End Basic. Section NoParallelism. (* If jobs cannot execute in parallel, then... *) Hypothesis no_parallelism: jobs_dont_execute_in_parallel sched. (* ..., the service received by job j at any time t is at most 1, ... *) Lemma service_at_most_one : forall t, service_at sched j t <= 1. Proof. unfold service_at, jobs_dont_execute_in_parallel in *; ins. destruct (scheduled sched j t) eqn:SCHED; unfold scheduled in SCHED. { move: SCHED => /exists_inP SCHED; des. move: H2 => /eqP SCHED. rewrite -big_filter. rewrite (bigD1_seq x); [simpl | | by rewrite filter_index_enum enum_uniq]; last first. { by rewrite mem_filter; apply/andP; split; [by apply/eqP | by rewrite mem_index_enum]. } rewrite -big_filter -filter_predI big_filter. rewrite -> eq_bigr with (F2 := fun cpu => 0); first by rewrite /= big_const_seq iter_addn mul0n 2!addn0. intro i; move => /andP [/eqP NEQ /eqP SCHEDi]. by apply no_parallelism with (cpu1 := x) in SCHEDi; subst. } { apply negbT in SCHED; rewrite negb_exists_in in SCHED. move: SCHED => /forall_inP SCHED. by rewrite big_pred0; red; ins; apply negbTE, SCHED. } Qed. (* ..., which implies that the service receive during a interval of length delta is at most delta. *) Lemma cumulative_service_le_delta : forall t delta, service_during sched j t (t + delta) <= delta. Proof. unfold service_at, jobs_dont_execute_in_parallel in *; ins. generalize dependent t. induction delta. { ins; unfold service_during; rewrite addn0. by rewrite big_geq. } { unfold service_during; intro t. rewrite -addn1 addnA addn1 big_nat_recr; last by apply leq_addr. apply leq_add; first by apply IHdelta. by apply service_at_most_one. } Qed. End NoParallelism. Section Completion. (* Assume that completed jobs do not execute. *) Hypothesis H_completed_jobs: completed_jobs_dont_execute job_cost sched. (* Then, after job j completes, it remains completed. *) Lemma completion_monotonic : forall t t', t <= t' -> completed job_cost sched j t -> completed job_cost sched j t'. Proof. unfold completed; move => t t' LE /eqP COMPt. rewrite eqn_leq; apply/andP; split; first by apply H_completed_jobs. by apply leq_trans with (n := service sched j t); [by rewrite COMPt | by apply extend_sum]. Qed. (* A completed job cannot be scheduled. *) Lemma completed_implies_not_scheduled : forall t, completed job_cost sched j t -> ~~ scheduled sched j t. Proof. rename H_completed_jobs into COMP. unfold completed_jobs_dont_execute in *. intros t COMPLETED. apply/negP; red; intro SCHED. have BUG := COMP j t.+1. rewrite leqNgt in BUG; move: BUG => /negP BUG; apply BUG. unfold service; rewrite big_nat_recr // /= -addn1. apply leq_add; first by move: COMPLETED => /eqP <-. by rewrite lt0n -not_scheduled_no_service negbK. Qed. (* The service received by job j in any interval is no larger than its cost. *) Lemma cumulative_service_le_job_cost : forall t t', service_during sched j t t' <= job_cost j. Proof. unfold service_during; rename H_completed_jobs into COMP; red in COMP; ins. destruct (t > t') eqn:GT. by rewrite big_geq // -ltnS; apply ltn_trans with (n := t); ins. apply leq_trans with (n := \sum_(0 <= t0 < t') service_at sched j t0); last by apply COMP. rewrite -> big_cat_nat with (m := 0) (n := t); [by apply leq_addl | by ins | by rewrite leqNgt negbT //]. Qed. End Completion. Section Arrival. (* Assume that jobs must arrive to execute. *) Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched. (* Then, job j does not receive service at any time t prior to its arrival. *) Lemma service_before_job_arrival_zero : forall t, t < job_arrival j -> service_at sched j t = 0. Proof. rename H_jobs_must_arrive into ARR; red in ARR; intros t LT. specialize (ARR j t). apply contra with (c := scheduled sched j t) (b := has_arrived j t) in ARR; last by rewrite -ltnNge. apply/eqP; rewrite -leqn0; unfold service_at. rewrite -> eq_bigr with (F2 := fun cpu => 0); first by rewrite big_const_seq iter_addn mul0n addn0. intros i SCHED; move: ARR; rewrite negb_exists_in; move => /forall_inP ARR. by exploit (ARR i); [by ins | ins]; destruct (sched i t == Some j). Qed. (* The same applies for the cumulative service received by job j. *) Lemma cumulative_service_before_job_arrival_zero : forall t1 t2, t2 <= job_arrival j -> \sum_(t1 <= i < t2) service_at sched j i = 0. Proof. intros t1 t2 LE; apply/eqP; rewrite -leqn0. apply leq_trans with (n := \sum_(t1 <= i < t2) 0); last by rewrite big_const_nat iter_addn mul0n addn0. rewrite big_nat_cond [\sum_(_ <= _ < _) 0]big_nat_cond. apply leq_sum; intro i; rewrite andbT; move => /andP LTi; des. rewrite service_before_job_arrival_zero; first by ins. by apply leq_trans with (n := t2); ins. Qed. (* Hence, you can ignore the service received by a job before its arrival time. *) Lemma service_before_arrival_eq_service_during : forall t0 t, t0 <= job_arrival j -> \sum_(t0 <= t < job_arrival j + t) service_at sched j t = \sum_(job_arrival j <= t < job_arrival j + t) service_at sched j t. Proof. intros t0 t LE; rewrite -> big_cat_nat with (n := job_arrival j); [| by ins | by apply leq_addr]. by rewrite /= cumulative_service_before_job_arrival_zero; [rewrite add0n | apply leqnn]. Qed. End Arrival. Section Pending. (* Assume that jobs must arrive to execute. *) Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched. (* Assume that completed jobs do not execute. *) Hypothesis H_completed_jobs: completed_jobs_dont_execute job_cost sched. (* Then, if job j is scheduled, it must be pending. *) Lemma scheduled_implies_pending: forall t, scheduled sched j t -> pending job_cost sched j t. Proof. rename H_jobs_must_arrive into ARRIVE, H_completed_jobs into COMP. unfold jobs_must_arrive_to_execute, completed_jobs_dont_execute in *. intros t SCHED. unfold pending; apply/andP; split; first by apply ARRIVE. apply/negP; unfold not; intro COMPLETED. have BUG := COMP j t.+1. rewrite leqNgt in BUG; move: BUG => /negP BUG; apply BUG. unfold service; rewrite -addn1 big_nat_recr // /=. apply leq_add; first by move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED. rewrite lt0n; apply/eqP; red; move => /eqP NOSERV. rewrite -not_scheduled_no_service in NOSERV. by rewrite SCHED in NOSERV. Qed. End Pending. End JobLemmas. (* In this section, we prove some lemmas about the list of jobs scheduled at time t. *) Section ScheduledJobsLemmas. (* Consider an arrival sequence ...*) Context {Job: eqType}. Context {arr_seq: arrival_sequence Job}. (* ... and some schedule. *) Context {num_cpus: nat}. Variable sched: schedule num_cpus arr_seq. Section Membership. (* A job is in the list of scheduled jobs iff it is scheduled. *) Lemma mem_scheduled_jobs_eq_scheduled : forall j t, j \in jobs_scheduled_at sched t = scheduled sched j t. Proof. unfold jobs_scheduled_at, scheduled. intros j t; apply/idP/idP. { intros IN. apply mem_bigcat_ord_exists in IN; des. apply/exists_inP; exists i; first by done. destruct (sched i t); last by done. by rewrite mem_seq1 in IN; move: IN => /eqP IN; subst. } { move => /exists_inP EX; destruct EX as [i IN SCHED]. apply mem_bigcat_ord with (j := i); first by apply ltn_ord. by move: SCHED => /eqP SCHED; rewrite SCHED /= mem_seq1 eq_refl. } Qed. End Membership. Section Uniqueness. (* Suppose there's no job parallelism. *) Hypothesis H_no_parallelism : jobs_dont_execute_in_parallel sched. (* Then, the list of jobs scheduled at any time t has no duplicates. *) Lemma scheduled_jobs_uniq : forall t, uniq (jobs_scheduled_at sched t). Proof. intros t; rename H_no_parallelism into SEQUENTIAL. unfold jobs_dont_execute_in_parallel in SEQUENTIAL. clear -SEQUENTIAL. unfold jobs_scheduled_at. induction num_cpus; first by rewrite big_ord0. { rewrite big_ord_recr cat_uniq; apply/andP; split. { apply bigcat_ord_uniq; first by intro i; unfold make_sequence; desf. intros x i1 i2 IN1 IN2; unfold make_sequence in *. desf; move: Heq0 Heq => SOME1 SOME2. rewrite mem_seq1 in IN1; rewrite mem_seq1 in IN2. move: IN1 IN2 => /eqP IN1 /eqP IN2; subst x j0. specialize (SEQUENTIAL j t (widen_ord (leqnSn n) i1) (widen_ord (leqnSn n) i2) SOME1 SOME2). by inversion SEQUENTIAL; apply ord_inj. } apply/andP; split; last by unfold make_sequence; destruct (sched ord_max). { rewrite -all_predC; apply/allP; unfold predC; simpl. intros x INx. unfold make_sequence in INx. destruct (sched ord_max t) eqn:SCHED; last by rewrite in_nil in INx. apply/negP; unfold not; intro IN'. have EX := mem_bigcat_ord_exists _ x n. apply EX in IN'; des; clear EX. unfold make_sequence in IN'. desf; rename Heq into SCHEDi. rewrite mem_seq1 in INx; rewrite mem_seq1 in IN'. move: INx IN' => /eqP INx /eqP IN'; subst x j0. specialize (SEQUENTIAL j t ord_max (widen_ord (leqnSn n) i) SCHED SCHEDi). inversion SEQUENTIAL; destruct i as [i EQ]; simpl in *. clear SEQUENTIAL SCHEDi. by rewrite H0 ltnn in EQ. } } Qed. End Uniqueness. Section NumberOfJobs. (* The number of scheduled jobs is no larger than the number of cpus. *) Lemma num_scheduled_jobs_le_num_cpus : forall t, size (jobs_scheduled_at sched t) <= num_cpus. Proof. intros t. unfold jobs_scheduled_at. destruct num_cpus; first by rewrite big_ord0. apply size_bigcat_ord; first by apply (Ordinal (ltnSn n)). by ins; unfold make_sequence; desf. Qed. End NumberOfJobs. End ScheduledJobsLemmas. End Schedule. (* Specific properties of a schedule of sporadic jobs. *) Module ScheduleOfSporadicTask. Import SporadicTask Job. Export Schedule. Section Properties. Context {sporadic_task: eqType}. Context {Job: eqType}. Variable job_cost: Job -> nat. Variable job_task: Job -> sporadic_task. (* Consider any schedule. *) Context {arr_seq: arrival_sequence Job}. Context {num_cpus: nat}. Variable sched: schedule num_cpus arr_seq. (* Next we define intra-task parallelism, ... *) Definition jobs_of_same_task_dont_execute_in_parallel := forall (j j': JobIn arr_seq) t, job_task j = job_task j' -> scheduled sched j t -> scheduled sched j' t -> j = j'. (* ... and task precedence constraints. *) Definition task_precedence_constraints := forall (j j': JobIn arr_seq) t, job_task j = job_task j' -> job_arrival j < job_arrival j' -> pending job_cost sched j t -> ~~ scheduled sched j' t. End Properties. Section BasicLemmas. (* Assume the job cost and task are known. *) Context {sporadic_task: eqType}. Variable task_cost: 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. (* Then, in a valid schedule of sporadic tasks ...*) Context {arr_seq: arrival_sequence Job}. Context {num_cpus: nat}. Variable sched: schedule num_cpus arr_seq. (* ...such that jobs do not execute after completion, ...*) Hypothesis jobs_dont_execute_after_completion : completed_jobs_dont_execute job_cost sched. Variable tsk: sporadic_task. Variable j: JobIn arr_seq. Hypothesis H_job_of_task: job_task j = tsk. Hypothesis valid_job: valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j. (* Remember that for any job of tsk, service <= task_cost tsk *) Lemma cumulative_service_le_task_cost : forall t t', service_during sched j t t' <= task_cost tsk. Proof. rename valid_job into VALID; unfold valid_sporadic_job in *; ins; des. apply leq_trans with (n := job_cost j); last by rewrite -H_job_of_task; apply VALID0. by apply cumulative_service_le_job_cost. Qed. End BasicLemmas. End ScheduleOfSporadicTask. (* Specific properties for a schedule of sporadic tasks with jitter. *) Module ScheduleOfTaskWithJitter. Export ScheduleOfSporadicTask. Section ArrivalAfterJitter. (* Assume the job cost, task and jitter are known. *) Context {sporadic_task: eqType}. Context {Job: eqType}. Variable job_cost: Job -> nat. Variable job_task: Job -> sporadic_task. Variable job_jitter: Job -> nat. (* Then, in a valid schedule of sporadic jobs with jitter, ... *) Context {arr_seq: arrival_sequence Job}. Context {num_cpus: nat}. Variable sched: schedule num_cpus arr_seq. (* ... a job can only be scheduled after the jitter. *) Definition jobs_execute_after_jitter := forall j t, scheduled sched j t -> job_arrival j + job_jitter j <= t. Section BasicLemmas. (* Note that if a job only executes after the jitter, it also only executes after its arrival time. *) Lemma arrival_before_jitter : jobs_execute_after_jitter -> jobs_must_arrive_to_execute sched. Proof. unfold jobs_execute_after_jitter, jobs_must_arrive_to_execute. intros ARRIVE j t SCHED; unfold has_arrived. rewrite -(leq_add2r (job_jitter j)). by apply leq_trans with (n := t); [by apply ARRIVE | by apply leq_addr]. Qed. End BasicLemmas. End ArrivalAfterJitter. End ScheduleOfTaskWithJitter.