Library probsa.rt.analysis.completion_time
From prosa.analysis Require Export facts.model.service_of_jobs.
From prosa Require Export model.preemption.fully_preemptive.
From probsa.rt.model Require Export abort_readiness.
From probsa.rt.model Require Export carry_in.
From probsa.rt.model.assumptions
Require Export basic pr_respects_policy pr_must_be_ready pr_work_conserving.
Local Open Scope nat_scope.
From prosa Require Export model.preemption.fully_preemptive.
From probsa.rt.model Require Export abort_readiness.
From probsa.rt.model Require Export carry_in.
From probsa.rt.model.assumptions
Require Export basic pr_respects_policy pr_must_be_ready pr_work_conserving.
Local Open Scope nat_scope.
Existence of Completion Time
Section CompletionTimeExists.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Hypothesis H_transitive_priorities : transitive hep_task.
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Variable sched : pr_schedule μ (ideal.processor_state Job).
Hypothesis H_work_conserving : pr_work_conserving sched pr_abort_ready_instance.
Hypothesis H_respects_policy_at_preemption_point :
pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.
Hypothesis H_pr_jobs_must_be_ready_to_execute :
pr_jobs_must_be_ready_to_execute sched pr_abort_ready_instance.
Hypothesis H_pr_completed_jobs_dont_execute : pr_completed_jobs_dont_execute sched.
Hypothesis H_pr_jobs_must_arrive_to_execute : pr_jobs_must_arrive_to_execute sched.
Hypothesis H_pr_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence sched.
Variable tsk : Task.
Let V := pr_carry_in_workload_of_hep_jobs sched tsk : instant → rvar μ [eqType of work].
Section StepByStepProof.
Variable ω : Ω.
Consider a non-empty interval
[t, t + Δ) ...
... such that all carry-in workload at time t and all the
new higher-or-equal priority workload released in
[t, t + Δ)
are consumed.
Hypothesis H_workload_is_consumed :
V t ω + pr_workload_of_hep_tasks tsk t (t + Δ) ω ≤ Δ.
Let ARR1 := [eta pr_arrivals_between 0 t].
Let ARR2 := [eta pr_arrivals_between t (t + Δ)].
Let P1 (ω : Ω) (j : Job) := before_deadline j ω t && hep_task (job_task j) tsk.
Let P2 (j : Job) := hep_task (job_task j) tsk.
Variable j : Job.
Hypothesis H_hep_tsk : hep_task (job_task j) tsk.
Hypothesis H_arrival : job_arrival j ω = Some t.
Hypothesis H_deadline_in_future : t + Δ ≤ odflt0 (job_deadline j) ω.
Hypothesis H_not_completed : ~~ pr_completed_by sched j (t + Δ) ω.
V t ω + pr_workload_of_hep_tasks tsk t (t + Δ) ω ≤ Δ.
Let ARR1 := [eta pr_arrivals_between 0 t].
Let ARR2 := [eta pr_arrivals_between t (t + Δ)].
Let P1 (ω : Ω) (j : Job) := before_deadline j ω t && hep_task (job_task j) tsk.
Let P2 (j : Job) := hep_task (job_task j) tsk.
Variable j : Job.
Hypothesis H_hep_tsk : hep_task (job_task j) tsk.
Hypothesis H_arrival : job_arrival j ω = Some t.
Hypothesis H_deadline_in_future : t + Δ ≤ odflt0 (job_deadline j) ω.
Hypothesis H_not_completed : ~~ pr_completed_by sched j (t + Δ) ω.
Overall, the proof employs the standard technique that has been used
many times before in Prosa:
- Show some job is always scheduled (work-conserving property)
- Derive lower bound on total service from Step 1 (it is at least Δ)
- Show workload ≤ service (follows from H_workload_is_consumed)
- Combine Steps 2 and 3 to show workload = service
- Conclude job j completes (workload = service implies completion).
Section Step1.
Remark scheduled_if_before_deadline :
∀ j ω t,
scheduled_at (sched ω) j t →
before_deadline j ω t.
Local Lemma some_job_scheduled :
∀ to,
t ≤ to < t + Δ →
∃ j, scheduled_at (sched ω) j to ∧ (P1 ω j ∧ j \in ARR1 ω ∨ P2 j ∧ j \in ARR2 ω).
End Step1.
Section Step2.
Remark pr_service_of_jobs_cat :
∀ (P : pred Job) (jobs : seq Job) (t1 t2 t : instant) (ω : Ω),
t1 ≤ t ≤ t2 →
service_of_jobs (sched ω) P jobs t1 t2
= service_of_jobs (sched ω) P jobs t1 t
+ service_of_jobs (sched ω) P jobs t t2.
Local Lemma lower_bound_on_service_of_jobs :
Δ ≤
service_of_jobs (sched ω) (P1 ω) (ARR1 ω) t (t + Δ)
+ service_of_jobs (sched ω) P2 (ARR2 ω) t (t + Δ).
End Step2.
Section Step3.
Local Lemma workload_le_service :
V t ω + pr_workload_of_hep_tasks tsk t (t + Δ) ω
≤ service_of_jobs (sched ω) (P1 ω) (ARR1 ω) t (t + Δ)
+ service_of_jobs (sched ω) P2 (ARR2 ω) t (t + Δ).
End Step3.
Section Step4.
Remark summand_wise_bound_implies_eq :
∀ (a b c d : nat),
a ≥ c →
b ≥ d →
a + b ≤ c + d →
a = c ∧ b = d.
Lemma carry_in_workload_eq_service_of_jobs :
V t ω = service_of_jobs (sched ω) (P1 ω) (ARR1 ω) t (t + Δ)
∧ pr_workload_of_hep_tasks tsk t (t + Δ) ω = service_of_jobs (sched ω) P2 (ARR2 ω) t (t + Δ).
End Step4.
Section Step5.
Local Lemma j_completed :
pr_completed_by sched j (t + Δ) ω.
End Step5.
End StepByStepProof.
Variable ω : Ω.
Consider a non-empty interval
[t, t + Δ) ...
... such that all carry-in workload at time t and all the new
higher-or-equal priority workload released in
[t, t + Δ) are
consumed.
We show that there exists a time δ ≤ Δ by which all higher-or-equal
priority jobs arriving at time t complete, provided they have sufficient
deadline slack (i.e., t + δ ≤ job_deadline).
The deadline condition is important: under the abort-ready model, jobs
that miss their deadlines are aborted and never complete.