Library probsa.rt.behavior.response_time
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export etime.
From probsa.rt.behavior Require Export service.
Local Open Scope nat_scope.
(* ---------------------------------- Main ---------------------------------- *)
From probsa.util Require Export etime.
From probsa.rt.behavior Require Export service.
Local Open Scope nat_scope.
(* ---------------------------------- Main ---------------------------------- *)
Section PrResponseTime.
Context {Ω} {μ : measure Ω}.
Context {Job : JobType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_cost : JobCostRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable sched : pr_schedule μ PState.
Context {Ω} {μ : measure Ω}.
Context {Job : JobType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_cost : JobCostRV Job Ω μ}.
Context {PState : ProcessorState Job}.
Variable sched : pr_schedule μ PState.
We use a variable horizon to denote the time instant when the
system is terminated. If a job completes beyond this time, it
will be considered as having an infinite response time. Notice
that the horizon has the option type; we use None to denote
the case when the termination time is not set, so the system
runs forever.
In this section, we introduce a definition of the response time
of a job using the limited principle of omniscience (LPO), which
is a simple, classically true, proposition that is not true in
intuitionistic mathematics stating that (∀ n : nat, P n ∨ ¬ P n)
→ {n : nat | P n} + {∀ n : nat, ¬ P n}. The advantage of such
an approach is that we are not restricted by the decidability
rules, so we can handle a case when the response time of a job
is infinite.
Lemma completed_by_is_dec :
∀ (ω : Ω) (j : Job) (compl_time : instant),
pr_completed_by sched j compl_time ω ∨ ¬ pr_completed_by sched j compl_time ω.
∀ (ω : Ω) (j : Job) (compl_time : instant),
pr_completed_by sched j compl_time ω ∨ ¬ pr_completed_by sched j compl_time ω.
Next, LPO_min finds the minimum time instant t such that
completed_by_is_dec ω j, and, if such a time instant does
not exist, LPO_min returns None.
Definition min_completion_time (ω : Ω) (j : Job) :=
LPO_min (fun compl_time ⇒ pr_completed_by sched j compl_time ω) (completed_by_is_dec ω j).
LPO_min (fun compl_time ⇒ pr_completed_by sched j compl_time ω) (completed_by_is_dec ω j).
We use both LPO_min and horizon to define the response
time of a job. We need to consider the following cases:
1. Job does not arrive ==> response time = Undef
2. Job arrives but never completes ==> response time = Infty
3. Job arrives at time instant a, completes at a time
instant ct, and horizon = None ==> response time = cr -
a
4. Job arrives at time instant a, completes at a time
instant ct, horizon = Some h, and ct ≥ h ==> response
time = Infty
5. Finally, if the job arrives at time instant a, completes
at a time instant ct, horizon = Some h, and ct < h ==>
response time = cr - a.
Definition response_time (j : Job) : rvar μ [eqType of etime] :=
mkRvar μ (fun ω:Ω ⇒
match job_arrival j ω with
| None ⇒ Undef
| Some ar ⇒
match min_completion_time ω j, horizon with
| inright _, _ ⇒ Infty
| inleft (exist compl_time _), None ⇒ Fin (compl_time - ar)
| inleft (exist compl_time _), Some h ⇒
if compl_time ≥ h then Infty else Fin (compl_time - ar)
end
end
).
Definition response_time_exceeds (j : Job) (R : duration) : brvar μ :=
mkRvar μ (fun ω:Ω ⇒ exceeds (response_time j ω) R).
End LPO_ResponseTime.
End PrResponseTime.
mkRvar μ (fun ω:Ω ⇒
match job_arrival j ω with
| None ⇒ Undef
| Some ar ⇒
match min_completion_time ω j, horizon with
| inright _, _ ⇒ Infty
| inleft (exist compl_time _), None ⇒ Fin (compl_time - ar)
| inleft (exist compl_time _), Some h ⇒
if compl_time ≥ h then Infty else Fin (compl_time - ar)
end
end
).
Definition response_time_exceeds (j : Job) (R : duration) : brvar μ :=
mkRvar μ (fun ω:Ω ⇒ exceeds (response_time j ω) R).
End LPO_ResponseTime.
End PrResponseTime.