Commit fa83b9f7 authored by Markus Anders's avatar Markus Anders

EDF continued

parents fd9f952e 99a3d9f4
Require Import rt.util.all.
Require Import rt.model.time rt.model.job rt.model.arrival_sequence.
Require Import rt.model.time rt.model.job rt.model.arrival_sequence rt.model.priority.
Require Import rt.model.uni.schedule rt.model.uni.schedulability.
Require Import rt.model.uni.basic.platform.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Demand.
Import UniprocessorSchedule Schedulability.
Import UniprocessorSchedule Schedulability Priority Platform Job.
(* In this section, we define the concept of demand. *)
Section DefiningDemand.
Context {Task: eqType}.
......@@ -18,46 +20,54 @@ Module Demand.
(* Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
(* For simplicity, let us define some local variables.*)
Let arrivals_between := jobs_arrived_between arr_seq.
Let absolute_deadline (j: JobIn arr_seq) :=
job_arrival j + job_deadline j.
(* Flters all jobs which arrived and have to complete during [t1, t2). *)
Definition jobs_with_arrival_and_deadline_between t1 t2 :=
[seq j <- arrivals_between t1 t2 | absolute_deadline j < t2].
(* In this section, we define the demand of a job set. *)
Section TotalDemand.
Variable t1 t2: time.
(* Let us define the total demand in the interval [t1,t2) as the
workload of jobs with arrival and deadline inside the interval.*)
Definition total_demand :=
Definition total_demand_during t1 t2 :=
\sum_(j <- jobs_with_arrival_and_deadline_between t1 t2) job_cost j.
(* Similarly the total demand before t is the demand in the interval [0, t). *)
Definition total_demand_before t :=
total_demand_during 0 t.
End TotalDemand.
(* In this section, we define the demand of a given task. *)
Section DemandOfTask.
(* Let tsk be a task ... *)
Variable tsk: Task.
(* ...and define a property that decides whether a job j is of tsk. *)
Let job_of_tsk (j: JobIn arr_seq) := job_task j == tsk.
Variable t1 t2: time.
Definition jobs_of_task_with_arrival_and_deadline_between :=
(* Filters the jobs of tsk that arrived and have to complete in the interval [t1, t2). *)
Definition jobs_of_task_with_arrival_and_deadline_between t1 t2 :=
[seq j <- jobs_with_arrival_and_deadline_between t1 t2 | job_of_tsk j].
(* Let us define the processor demand of a task in the
(* Then let us define the processor demand of a task in the
interval [t1,t2) as the workload of jobs of tsk with
arrival and deadline inside this interval. *)
Definition total_task_demand :=
\sum_(j <- jobs_of_task_with_arrival_and_deadline_between) job_cost j.
Definition total_task_demand_during t1 t2 :=
\sum_(j <- jobs_of_task_with_arrival_and_deadline_between t1 t2) job_cost j.
Definition total_task_demand_before t :=
total_task_demand_during 0 t.
End DemandOfTask.
End DefiningDemand.
(* In this section, we prove some useful lemmas about demand. *)
Section Lemmas.
Context {Task: eqType}.
......@@ -65,34 +75,163 @@ Module Demand.
Variable job_cost: Job -> time.
Variable job_deadline: Job -> time.
Variable job_task: Job -> Task.
(* Consider any job arrival sequence ... *)
Context {arr_seq: arrival_sequence Job}.
(* ... and a schedule sched of this arrival sequence. *)
Variable sched: schedule arr_seq.
(* Furthermore there is a schedule which enforces EDF policy. *)
Variable schededf: schedule arr_seq.
Hypothesis H_edf_policy: enforces_JLDP_policy job_cost schededf (EDF job_deadline).
(* Let all jobs have valid job parameters and only execute after they arrived. *)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
valid_realtime_job job_cost job_deadline j.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
(* For simplicity define a function which provides whether all
deadlines have been met in a given schedule. *)
Let no_deadline_miss_in (sched: schedule arr_seq) :=
forall j, job_misses_no_deadline job_cost job_deadline sched j.
(* For now, assume that EDF is optimal which means that there
is an EDF schedule where all deadlines are met if there
is any schedule where all deadlines are met. *)
Hypothesis H_optimality_of_edf_schedules:
no_deadline_miss_in sched -> no_deadline_miss_in schededf.
(* For simplicity, let us define some local variables about demand. *)
Let absolute_deadline (j: JobIn arr_seq) :=
job_arrival j + job_deadline j.
job_arrival j + job_deadline j.
Let demand_during := total_demand_during job_cost job_deadline arr_seq.
Let demand_before := total_demand_before job_cost job_deadline arr_seq.
(* In this section, we prove properties if a job set is schedulable. *)
Section Schedulability.
(* Assume that the job set is schedulable. *)
Hypothesis H_no_deadline_miss:
no_deadline_miss_in sched.
(* Has to go to a different file. *)
(* The total service providable is bounded by the length of the interval. *)
Lemma total_service_bounded_by_interval_length:
forall t delta, total_service_during sched t (t + delta) <= delta.
Proof.
Admitted.
(* Then the total service is not greater than the total demand. *)
Lemma total_service_ge_total_demand_if_schedulable:
forall t delta, demand_during t (t + delta) <= total_service_during sched t (t + delta).
Proof.
Admitted.
Let total_demand_before := total_demand job_cost job_deadline arr_seq 0.
Let is_schedulable := job_misses_no_deadline job_cost job_deadline sched.
Hypothesis H_demand_always_satisfied:
forall j t,
t = absolute_deadline j ->
total_demand_before t <= t .
Lemma schedulable_if_demand_satisfied:
forall j, is_schedulable j.
(*service received by j at deadline will be enough.*)
(* As a corollary, the demand will never exceed the length of the interval. *)
Lemma demand_never_exceeds_time_if_schedulable:
forall t delta, demand_during t (t + delta) <= delta.
(*service received by j at deadline will be not enough.*)
Proof.
intros j.
unfold is_schedulable, job_misses_no_deadline, completed_by.
Admitted.
rename H_optimality_of_edf_schedules into OPTEDF,
H_no_deadline_miss into NOMISS.
apply OPTEDF in NOMISS.
induction t.
{
admit.
}
intros delta. apply contraT.
rewrite -ltnNge.
(*have SERVLTT : forall j, service_during sched j 0 t0.+1 <= t0.+1.*)
{
admit.
}
Admitted.
End Schedulability.
(* In this section, we introduce properties which you have to
check in order to check schedulability. *)
Section SatisfiedDemand.
(*If the demand during any interval is bounded by the length of the interval, ... *)
Hypothesis H_demand_always_satisfied:
forall t delta, demand_during t (t + delta) <= delta.
(*...then the job set is schedulable. *)
Lemma schedulable_if_demand_always_satisfied:
no_deadline_miss_in sched.
Proof.
rename H_valid_job_parameters into VALID.
rename H_demand_always_satisfied into SAT.
rewrite /no_deadline_miss_in.
suff NOMISS : forall t j, job_arrival j + job_deadline j <= t ->
job_misses_no_deadline job_cost job_deadline sched j.
{
intro j.
by apply (NOMISS (job_arrival j + job_deadline j)).
}
induction t.
{
intros j.
rewrite leqn0 addn_eq0.
have DEAD0 : (job_deadline j == 0) = false.
{
apply negbTE. rewrite -lt0n.
rewrite /valid_realtime_job in VALID.
apply VALID.
}
by rewrite DEAD0 // andbF.
}
intros j LE.
(*j is the first job to miss its deadline.*)
case: (leqP (job_arrival j + job_deadline j) (t)) => [LEQ | GT].
-by apply IHt.
have TDEAD : (job_arrival j + job_deadline j) == t.+1.
{
rewrite eqn_leq.
rewrite LE //.
}
clear LE GT IHt.
apply contraT.
(* For now, we know that j is the first job to miss its deadline
and the deadline is at t.+1. *)
(*proof sketch:
exists t1 so that [t1, t.+1) is a busy interval.
-> t1 is quiet time, every point in interval is busy
there is a deadline miss at t.+1
=> demand t1 t.+1 > (t.+1 - t1)
contradiction.
*)
Admitted.
End SatisfiedDemand.
(* In this section, we combine the lemmas from the two sections
before so that we know equivalence of both properties. *)
Section Iff.
Variable t : time.
Lemma schedulable_iff_demand_always_satisfied:
no_deadline_miss_in sched <->
forall t delta, demand_during t (t +delta) <= delta.
Proof.
rewrite iff_to_and.
split.
{
intro NOMISS.
by apply demand_never_exceeds_time_if_schedulable.
}
{
intro SCHED.
by apply schedulable_if_demand_always_satisfied.
}
Qed.
End Iff.
End Lemmas.
End Demand.
End Demand.
\ No newline at end of file
......@@ -3,11 +3,12 @@ Require Import rt.model.time rt.model.job rt.model.arrival_sequence rt.model.pri
Require Import rt.model.uni.schedule rt.model.uni.schedulability.
Require Import rt.model.uni.basic.platform.
Require Import rt.model.uni.transformations.swap.
Require Import rt.model.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module EarliestDeadlineFirst.
Import UniprocessorSchedule Schedulability Priority Platform Swap.
Import UniprocessorSchedule Schedulability Priority Platform Swap ScheduleConstruction.
Section Construction.
......@@ -47,32 +48,141 @@ Module EarliestDeadlineFirst.
(* ...and take the minimum. *)
Definition earliest_scheduled sched j := seq_min (is_scheduled sched j).
Section Lemmas.
(* Lemma: If j is not completed by t_min and completed by t_max -> earliest_scheduled != None *)
(* Lemma: earliest_scheduled is earliest *)
End Lemmas.
End EarliestScheduled.
(* Find the deadline of a job in an arrival sequence... *)
Definition job_in_arr_seq_deadline (j : JobIn arr_seq) :=
job_deadline (job_of_job_in j).
Section EarliestDeadlineJob.
(* Find the deadline of a job in an arrival sequence... *)
Definition job_in_arr_seq_deadline (j : JobIn arr_seq) :=
job_deadline (job_of_job_in j).
(* *)
Definition earliest_deadline_job (sched : schedule arr_seq) (t_start : time) :=
seq_argmin (job_in_arr_seq_deadline) (arrivals_not_completed sched t_start).
Section Lemmas.
Variable sched : schedule arr_seq.
Variable t : time.
Lemma earliest_deadline_job_exists_if_pending_not_empty :
forall (j: JobIn arr_seq),
j \in (arrivals_not_completed sched t) -> seq_argmin (job_in_arr_seq_deadline) (arrivals_not_completed sched t) != None.
Proof.
intros j H.
by apply seq_min_exists with (x := j).
Qed.
Lemma earliest_deadline_job_has_earliest_deadline :
forall x y,
seq_argmin job_in_arr_seq_deadline (arrivals_not_completed sched t) = Some x -> y \in (arrivals_not_completed sched t) -> job_in_arr_seq_deadline x <= job_in_arr_seq_deadline y.
intros x y HASMIN INPENDING.
by apply seq_min_computes_min with (l := (arrivals_not_completed sched t)).
Qed.
End Lemmas.
End EarliestDeadlineJob.
(* ...to find a swap partner after t_start that is pending and has the least deadline. *)
Definition find_swap_slot (sched : schedule arr_seq) (t_start : time) :=
let swap_job := seq_argmin (job_in_arr_seq_deadline) (arrivals_not_completed sched t_start) in
let swap_job := earliest_deadline_job sched t_start in
if swap_job is Some j then
earliest_scheduled t_start (job_in_arr_seq_deadline j) sched j
match earliest_scheduled t_start (job_in_arr_seq_deadline j) sched j with
| Some t => t
| None => t_start
end
else
Some t_start.
t_start.
(* *)
(* Lemma doesnt break deadlines *)
(* Lemma edf_swap_slot_invariant *)
(* Recursively constructs an EDF schedule until time t from any valid schedule. *)
Fixpoint edf_swap (sched : schedule arr_seq) (t_max : time) : schedule arr_seq :=
Fixpoint edf_swap' (sched : schedule arr_seq) (t_max : time) : schedule arr_seq :=
if t_max is t_dec.+1 then
let rec_sched := (edf_swap sched t_dec) in
let rec_sched := (edf_swap' sched t_dec) in
fun t' => (swap rec_sched (find_swap_slot rec_sched t_max) t') t'
else
fun t' => (swap sched (find_swap_slot sched 0) t') t'.
(* Constructs an EDF schedule for any given schedule *)
Definition edf' (sched : schedule arr_seq) (t : time) :=
(edf_swap' sched t) t.
Variable base_sched : schedule arr_seq.
Let edf_sched := edf' base_sched.
(* Lemma edf_swap_slot_invariant: *)
(* forall t, *)
(* find_swap_slot (edf' base_sched) t = t. *)
(* Proof. *)
(* intro t. *)
(* induction t. *)
(* rewrite /edf' /find_swap_slot. *)
(* case *)
(* Qed. *)
(* Construction using schedule prefixes *)
Definition edf_swap (sched : schedule arr_seq) (t_max : time) : option (JobIn arr_seq) :=
(swap sched (find_swap_slot sched t_max) t_max) t_max.
Definition edf (sched : schedule arr_seq) :=
fun t => (edf_swap sched t) t.
build_schedule_from_prefixes arr_seq edf_swap sched.
(* Maybe show a) Forall t: edf_sched t = job with earliest deadline
b) edf_swap will change t to earliest deadline of pending jobs
c) edf_swap doesn't change all k < t*)
(* Lemma edf_swap_slot_invariant: *)
(* forall t, *)
(* find_swap_slot (edf base_sched) t = t. *)
(* Proof. *)
(* rewrite /edf. *)
(* rewrite /build_schedule_from_prefixes /schedule_prefix. *)
(* intro t. *)
(* induction t using strong_ind. *)
(* Qed. *)
Lemma edf_construction_uses_swap:
forall t,
edf_sched t = edf_swap edf_sched t.
Proof.
intros t.
induction t using strong_ind.
(* { *)
(* rewrite /edf_swap /find_swap_slot. *)
(* set jobs := earliest_deadline_job _ _. *)
(* have EMPTY: jobs = None. *)
(* by admit. *)
(* rewrite EMPTY. *)
(* by rewrite swap_same_schedule_for_same_time. *)
(* } *)
{
rewrite /edf_swap /find_swap_slot.
rewrite /earliest_scheduled.
admit.
}
(* by rewrite edf_swap_slot_invariant. *)
Admitted.
Print prefix_construction_uses_function.
(* Lemma edf_depends_only_on_service : *)
(* forall sched1 sched2 t, *)
(* (forall j, service sched1 j t = service sched2 j t) -> *)
(* edf_swap sched1 t = edf_swap sched2 t. *)
(* Proof. *)
(* intros sched1 sched2 t ALL. *)
(* rewrite /edf_swap /swap eq_refl. *)
(* Constructs an EDF schedule for any given schedule *)
(* Definition edf (sched : schedule arr_seq) := *)
(* fun t => (edf_swap sched t) t. *)
End Construction.
Section OptimalityOfEDF.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment