Library probsa.rt.analysis.completion

From prosa Require Export analysis.facts.behavior.completion.

From probsa.rt.behavior Require Export job schedule service.

Probabilistic Completion is Monotone

Section CompletionLemmas.

Consider a probability space (Ω, μ), ...

Context {Ω} {μ : measure Ω}.

... and any type of jobs. Assume that the jobs have probabilistic costs defined by job_cost.

Context {Job : JobType}
{job_cost : JobCostRV Job Ω μ}.

Consider any schedule sched.

  Context {PState : ProcessorState Job}.
  Variable sched : pr_schedule μ PState.

  Lemma completion_monotone :
    ∀ (j : Job) (t1 t2 : instant) (ω : Ω ),
      (t1 ≤ t2)%nat →
      pr_completed_by sched j t1 ω →
      pr_completed_by sched j t2 ω.
  Proof.
    intros ? ? ? ? LE COMPL.
    unfold pr_completed_by in *; simpl in ×.
    destruct (job_cost j ω) eqn:JC; last by rewrite JC.
    have C := @completion_monotonic
                _ (fun j ⇒ odflt 0%nat (job_cost j ω))
                PState (sched ω) j t1 t2 LE.
    rewrite /completed_by /prosa.behavior.job.job_cost in C.
    rewrite JC; rewrite JC in C; rewrite JC in COMPL.
    by apply C, COMPL.
  Qed.

Given two time instants t1 and t2 such that t1 ≤ t2, we show that the probability that a job j is completed by t1 is smaller than or equal to the probability that the same job j is completed by time t2.

  Lemma completion_monotone_prob :
    ∀ (j : Job) (t1 t2 : instant),
      (t1 ≤ t2)%nat →
      ℙ <μ >{[pr_completed_by sched j t1 ]} ≤ ℙ <μ >{[pr_completed_by sched j t2 ]}.
  Proof.
    intros; apply pr_mono_pred ⇒ ω.
    by apply completion_monotone.
  Qed.

End CompletionLemmas.