Library prosa.classic.model.schedule.uni.end_time
Require Import Arith Nat.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module end_time.
Import UniprocessorSchedule Job ResponseTime.
Section Task.
Context {task: eqType}.
Variable task_cost: task → time.
Variable task_period: task → time.
Variable task_deadline: task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → task.
(* instant option, to be used in end_time_option *)
Inductive diagnosis_option : Set :=
| OK : instant → diagnosis_option
| Failure : instant → diagnosis_option.
Section Job_end_time_Def.
(* Jobs will be scheduled on an uniprocessor *)
Variable sched: schedule Job.
(* Consider any job *)
Variable job:Job.
(* Recall the definition of scheduled_at for testing wether this job can
be scheduled at time t *)
Let job_scheduled_at t:= scheduled_at sched job t = true.
(* We define the function calculating the job's end time.
It takes three arguments:
t : job arrival instant
c : job cost duration
wf: an extra parameter that allows to realize a well-founded fixpoint
with the type nat. It is supposed big enough to return the actual end time.
Otherwise (i.e., it reaches 0), the function returns Failure t *)
Fixpoint end_time_option (t:instant) (c:duration) (wf:nat):=
match c with
| 0 ⇒ OK t
| S c'⇒ match wf with
| 0 ⇒ Failure t
| S wf'⇒ if scheduled_at sched job t then end_time_option (S t) c' wf'
else end_time_option (S t) c wf'
end
end.
(* We define an end time predicate with three arguments:
the job arrival instant, the job cost duration and
the job end time instant. Its three constructors
correspond to the cases:
- cost = 0 and job has ended
- cost > 0 and job cannot be scheduled at instant t
- cost > 0 and job can be scheduled at instant t
*)
Inductive end_time_predicate : instant→ duration→instant→Prop:=
|C0_: ∀ t, end_time_predicate t 0 t
|S_C_not_sched: ∀ t c e,
¬job_scheduled_at t→
end_time_predicate (S t) (S c) e→
end_time_predicate t (S c) e
|S_C_sched: ∀ t c e,
job_scheduled_at t→
end_time_predicate (S t) c e→
end_time_predicate t (S c) e.
(* The predicate completes_at specifies the instant a job ends
according to its arrival and cost *)
Definition completes_at (t:instant):=
end_time_predicate (job_arrival job) (job_cost job) t.
End Job_end_time_Def.
Section Lemmas.
(* Consider any job *)
Variable job:Job.
(* ... and and uniprocessor schedule this job*)
Variable sched: schedule Job.
(* ... where jobs do not execute before their arrival times nor after completion *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_valid_job:
valid_realtime_job job_cost job_deadline job.
(* Recall the function end_time_option*)
Let job_end_time_function:= end_time_option sched job.
(* Recall the end time predicate*)
Let job_end_time_p:= end_time_predicate sched job.
(* Recall the definition of completes_at*)
Let job_completes_at := completes_at sched job.
(* Recall the definition of scheduled_at for testing wether this job can
be scheduled at time t.*)
Let job_scheduled_at t:= scheduled_at sched job t = true.
(* Then, the job_end_time_function (if it terminates successfully) returns
the same result as the job_end_time_p predicate *)
(* function -> predicate *)
Theorem end_time_function_predicat_equivalence:
∀ e wf t c,
job_end_time_function t c wf = OK e →
job_end_time_p t c e.
(* The end time given by the predicate job_end_time_p is the same as
the result returned by the function job_end_time_function (provided
wf is large enough) *)
Theorem end_time_predicat_function_equivalence:
∀ t c e ,
job_end_time_p t c e →
∃ wf, job_end_time_function t c wf = OK e.
(* If we consider a time t where the job is not scheduled, then
the end_time_predicate returns the same end time starting from t or t+1 *)
Lemma end_time_predicate_not_sched:
∀ t c e,
~(job_scheduled_at t) →
end_time_predicate sched job t c.+1 e →
end_time_predicate sched job t.+1 c.+1 e.
(* If we consider a time t where the job is scheduled, then the end_time_predicate
returns the same end time starting from t with a cost c+1 than from t+1 with a cost c*)
Lemma end_time_predicate_sched:
∀ t c e,
job_scheduled_at t →
end_time_predicate sched job t c.+1 e →
end_time_predicate sched job t.+1 c e.
(* Assume that the job end time is job_end *)
Variable job_end: instant.
(* Recall the definition of completed_by defined in
model/schedule/uni/schedule.v *)
Let job_completed_by:=
completed_by job_cost sched.
(* Recall the definition of service_during defined in
model/schedule/uni/schedule.v *)
Let job_service_during:=
service_during sched job.
(* then the job arrival is less than or equal to job end time *)
Lemma arrival_le_end:
∀ t c e, job_end_time_p t c e → t ≤ e.
(* the sum of job arrival and job cost is less than or equal to
job end time*)
Lemma arrival_add_cost_le_end:
∀ t c e,
job_end_time_p t c e →
t+c≤e.
(* The servive received between the job arrival
and the job end is equal to the job cost*)
Lemma service_eq_cost_at_end_time:
job_completes_at job_end →
job_service_during (job_arrival job) job_end = job_cost job.
(* A job is completed by job end time*)
Lemma completed_by_end_time:
job_completes_at job_end →
job_completed_by job job_end.
(* The job end time is positive *)
Corollary end_time_positive:
job_completes_at job_end → job_end > 0.
(* The service received between job arrival and the previous instant
of job end time is exactly job cost-1*)
Lemma job_uncompletes_at_end_time_sub_1:
job_completes_at job_end →
job_service_during (job_arrival job) (job_end .-1) = (job_cost job) .-1.
(* At any instant from the job arrival and before the job end time,
job cannot be finished; the service received is always less than job cost*)
Lemma job_uncompleted_before_end_time:
job_completes_at job_end →
∀ t', job_arrival job ≤ t' ∧ t'≤ job_end.-1 →
job_service_during (job_arrival job) t' < job_cost job.
End Lemmas.
End Task.
End end_time.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module end_time.
Import UniprocessorSchedule Job ResponseTime.
Section Task.
Context {task: eqType}.
Variable task_cost: task → time.
Variable task_period: task → time.
Variable task_deadline: task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → task.
(* instant option, to be used in end_time_option *)
Inductive diagnosis_option : Set :=
| OK : instant → diagnosis_option
| Failure : instant → diagnosis_option.
Section Job_end_time_Def.
(* Jobs will be scheduled on an uniprocessor *)
Variable sched: schedule Job.
(* Consider any job *)
Variable job:Job.
(* Recall the definition of scheduled_at for testing wether this job can
be scheduled at time t *)
Let job_scheduled_at t:= scheduled_at sched job t = true.
(* We define the function calculating the job's end time.
It takes three arguments:
t : job arrival instant
c : job cost duration
wf: an extra parameter that allows to realize a well-founded fixpoint
with the type nat. It is supposed big enough to return the actual end time.
Otherwise (i.e., it reaches 0), the function returns Failure t *)
Fixpoint end_time_option (t:instant) (c:duration) (wf:nat):=
match c with
| 0 ⇒ OK t
| S c'⇒ match wf with
| 0 ⇒ Failure t
| S wf'⇒ if scheduled_at sched job t then end_time_option (S t) c' wf'
else end_time_option (S t) c wf'
end
end.
(* We define an end time predicate with three arguments:
the job arrival instant, the job cost duration and
the job end time instant. Its three constructors
correspond to the cases:
- cost = 0 and job has ended
- cost > 0 and job cannot be scheduled at instant t
- cost > 0 and job can be scheduled at instant t
*)
Inductive end_time_predicate : instant→ duration→instant→Prop:=
|C0_: ∀ t, end_time_predicate t 0 t
|S_C_not_sched: ∀ t c e,
¬job_scheduled_at t→
end_time_predicate (S t) (S c) e→
end_time_predicate t (S c) e
|S_C_sched: ∀ t c e,
job_scheduled_at t→
end_time_predicate (S t) c e→
end_time_predicate t (S c) e.
(* The predicate completes_at specifies the instant a job ends
according to its arrival and cost *)
Definition completes_at (t:instant):=
end_time_predicate (job_arrival job) (job_cost job) t.
End Job_end_time_Def.
Section Lemmas.
(* Consider any job *)
Variable job:Job.
(* ... and and uniprocessor schedule this job*)
Variable sched: schedule Job.
(* ... where jobs do not execute before their arrival times nor after completion *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_valid_job:
valid_realtime_job job_cost job_deadline job.
(* Recall the function end_time_option*)
Let job_end_time_function:= end_time_option sched job.
(* Recall the end time predicate*)
Let job_end_time_p:= end_time_predicate sched job.
(* Recall the definition of completes_at*)
Let job_completes_at := completes_at sched job.
(* Recall the definition of scheduled_at for testing wether this job can
be scheduled at time t.*)
Let job_scheduled_at t:= scheduled_at sched job t = true.
(* Then, the job_end_time_function (if it terminates successfully) returns
the same result as the job_end_time_p predicate *)
(* function -> predicate *)
Theorem end_time_function_predicat_equivalence:
∀ e wf t c,
job_end_time_function t c wf = OK e →
job_end_time_p t c e.
(* The end time given by the predicate job_end_time_p is the same as
the result returned by the function job_end_time_function (provided
wf is large enough) *)
Theorem end_time_predicat_function_equivalence:
∀ t c e ,
job_end_time_p t c e →
∃ wf, job_end_time_function t c wf = OK e.
(* If we consider a time t where the job is not scheduled, then
the end_time_predicate returns the same end time starting from t or t+1 *)
Lemma end_time_predicate_not_sched:
∀ t c e,
~(job_scheduled_at t) →
end_time_predicate sched job t c.+1 e →
end_time_predicate sched job t.+1 c.+1 e.
(* If we consider a time t where the job is scheduled, then the end_time_predicate
returns the same end time starting from t with a cost c+1 than from t+1 with a cost c*)
Lemma end_time_predicate_sched:
∀ t c e,
job_scheduled_at t →
end_time_predicate sched job t c.+1 e →
end_time_predicate sched job t.+1 c e.
(* Assume that the job end time is job_end *)
Variable job_end: instant.
(* Recall the definition of completed_by defined in
model/schedule/uni/schedule.v *)
Let job_completed_by:=
completed_by job_cost sched.
(* Recall the definition of service_during defined in
model/schedule/uni/schedule.v *)
Let job_service_during:=
service_during sched job.
(* then the job arrival is less than or equal to job end time *)
Lemma arrival_le_end:
∀ t c e, job_end_time_p t c e → t ≤ e.
(* the sum of job arrival and job cost is less than or equal to
job end time*)
Lemma arrival_add_cost_le_end:
∀ t c e,
job_end_time_p t c e →
t+c≤e.
(* The servive received between the job arrival
and the job end is equal to the job cost*)
Lemma service_eq_cost_at_end_time:
job_completes_at job_end →
job_service_during (job_arrival job) job_end = job_cost job.
(* A job is completed by job end time*)
Lemma completed_by_end_time:
job_completes_at job_end →
job_completed_by job job_end.
(* The job end time is positive *)
Corollary end_time_positive:
job_completes_at job_end → job_end > 0.
(* The service received between job arrival and the previous instant
of job end time is exactly job cost-1*)
Lemma job_uncompletes_at_end_time_sub_1:
job_completes_at job_end →
job_service_during (job_arrival job) (job_end .-1) = (job_cost job) .-1.
(* At any instant from the job arrival and before the job end time,
job cannot be finished; the service received is always less than job cost*)
Lemma job_uncompleted_before_end_time:
job_completes_at job_end →
∀ t', job_arrival job ≤ t' ∧ t'≤ job_end.-1 →
job_service_during (job_arrival job) t' < job_cost job.
End Lemmas.
End Task.
End end_time.