Library rt.restructuring.model.preemption.job.parameters


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.10.1 (October 2019)

----------------------------------------------------------------------------- *)

From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.

Job Preemptable

There are many equivalent ways to represent preemption points of a job.
In Prosa Preemption points are represented with a predicate [job_preemptable] which maps a job and its progress to a boolean value saying whether this job is preemptable at its current point of execution.
Class JobPreemptable (Job : JobType) :=
  job_preemptable : Job → work → bool.

Derived Parameters

Job Maximum and Last Non-preemptive Segment

In this section we define the notions of the maximal and the last non-preemptive segments.
Section MaxAndLastNonpreemptiveSegment.

Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobCost Job}.
  Context `{JobPreemptable Job}.

It is useful to have a representation of preemption points of a job defined as an actual sequence of points where this job can be preempted.
  Definition job_preemption_points (j : Job) : seq work :=
    [seq ρ:work <- range 0 (job_cost j) | job_preemptable j ρ].

Note that the conversion preserves the equivalence.
  Remark conversion_preserves_equivalence:
    ∀ (j : Job) (ρ : work),
      ρ ≤ job_cost j →
      job_preemptable j ρ ↔ ρ \in job_preemption_points j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  ============================
  forall (j : Job) (ρ : work),
  ρ <= job_cost j -> job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

  Proof.
    intros ? ? LE.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  ============================
  job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

    case: (posnP (job_cost j)) ⇒ [ZERO|POS].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 71)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  ZERO : job_cost j = 0
  ============================
  job_preemptable j ρ <-> ρ \in job_preemption_points j

subgoal 2 (ID 72) is:
 job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 71)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  ZERO : job_cost j = 0
  ============================
  job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

unfold job_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 74)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  ZERO : job_cost j = 0
  ============================
  job_preemptable j ρ <->
  ρ \in [seq ρ0 <- range 0 (job_cost j) | job_preemptable j ρ0]

----------------------------------------------------------------------------- *)

      split; intros PP.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 78)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  ZERO : job_cost j = 0
  PP : job_preemptable j ρ
  ============================
  ρ \in [seq ρ0 <- range 0 (job_cost j) | job_preemptable j ρ0]

subgoal 2 (ID 79) is:
 job_preemptable j ρ

----------------------------------------------------------------------------- *)

      - move: LE; rewrite ZERO leqn0; move ⇒ /eqP EQ; subst.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 126)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ZERO : job_cost j = 0
  PP : job_preemptable j 0
  ============================
  0 \in [seq ρ <- range 0 0 | job_preemptable j ρ]

subgoal 2 (ID 79) is:
 job_preemptable j ρ

----------------------------------------------------------------------------- *)

          by simpl; rewrite PP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 79)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  ZERO : job_cost j = 0
  PP : ρ \in [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]
  ============================
  job_preemptable j ρ

----------------------------------------------------------------------------- *)

      - rewrite ZERO in PP; simpl in PP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 170)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  ZERO : job_cost j = 0
  PP : ρ \in (if job_preemptable j 0 then [:: 0] else [::])
  ============================
  job_preemptable j ρ

----------------------------------------------------------------------------- *)

        destruct (job_preemptable j 0) eqn:EQ; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 187)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  ZERO : job_cost j = 0
  EQ : job_preemptable j 0 = true
  PP : ρ \in [:: 0]
  ============================
  job_preemptable j ρ

----------------------------------------------------------------------------- *)

          by move: PP ⇒ /orP [/eqP A1| FF]; subst.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)

subgoal 1 (ID 72) is:
 job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  ============================
  job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

    have F: job_cost j == 0 = false.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 323)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  ============================
  (job_cost j == 0) = false

subgoal 2 (ID 325) is:
 job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 323)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  ============================
  (job_cost j == 0) = false

----------------------------------------------------------------------------- *)

by apply/eqP/neqP; rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 325)

subgoal 1 (ID 325) is:
 job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 325)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  F : (job_cost j == 0) = false
  ============================
  job_preemptable j ρ <-> ρ \in job_preemption_points j

----------------------------------------------------------------------------- *)

    split; intros PP.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 457)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  F : (job_cost j == 0) = false
  PP : job_preemptable j ρ
  ============================
  ρ \in job_preemption_points j

subgoal 2 (ID 458) is:
 job_preemptable j ρ

----------------------------------------------------------------------------- *)

    all: unfold job_preemption_points in ×.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 460)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  F : (job_cost j == 0) = false
  PP : job_preemptable j ρ
  ============================
  ρ \in [seq ρ0 <- range 0 (job_cost j) | job_preemptable j ρ0]

subgoal 2 (ID 462) is:
 job_preemptable j ρ

----------------------------------------------------------------------------- *)

    - rewrite mem_filter; apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 495)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  F : (job_cost j == 0) = false
  PP : job_preemptable j ρ
  ============================
  ρ \in range 0 (job_cost j)

subgoal 2 (ID 462) is:
 job_preemptable j ρ

----------------------------------------------------------------------------- *)

        by rewrite mem_iota subn0 add0n //; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 462)
  
  Job : JobType
  H : JobArrival Job
  H0, H1 : JobCost Job
  H2 : JobPreemptable Job
  j : Job
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  F : (job_cost j == 0) = false
  PP : ρ \in [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]
  ============================
  job_preemptable j ρ

----------------------------------------------------------------------------- *)


    - by move: PP; rewrite mem_filter; move ⇒ /andP [PP _].
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We define a function that maps a job to the sequence of lengths of its nonpreemptive segments.
  Definition lengths_of_segments (j : Job) := distances (job_preemption_points j).

Next, we define a function that maps a job to the length of the longest nonpreemptive segment of job j.
  Definition job_max_nonpreemptive_segment (j : Job) := max0 (lengths_of_segments j).

Similarly, we define a function that maps a job to the length of the last nonpreemptive segment.
  Definition job_last_nonpreemptive_segment (j : Job) := last0 (lengths_of_segments j).

We define the notion of job's run-to-completion threshold: run-to-completion threshold is the amount of service after which a job cannot be preempted until its completion.
  Definition job_run_to_completion_threshold (j : Job) :=
    job_cost j - (job_last_nonpreemptive_segment j - ε).

End MaxAndLastNonpreemptiveSegment.