limited_preemptive.v 2.28 KB
Newer Older
1
Require Export rt.restructuring.model.preemption.parameter.
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58

(** Definition of a parameter relating a job
    to the sequence of its preemption points. *)
Class JobPreemptionPoints (Job : JobType) :=
  {
    job_preemption_points : Job -> seq work
  }.

(** * Platform for Models with Limited Preemptions *)
(** In this section, we instantiate [job_preemptable] for the model
    with limited preemptions and introduce a set of requirements for
    function [job_preemption_points], so it is coherent with limited
    preemptions model. *)
Section LimitedPreemptions.

  (**  Consider any type of jobs. *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  
  (** In addition, assume the existence of a function that
      maps a job to the sequence of its preemption points. *)
  Context `{JobPreemptionPoints Job}.

  (** In the model with limited preemptions a job can be preempted 
      if its progress is equal to one of the preemption points. *)
  Global Instance limited_preemptions_model : JobPreemptable Job :=
    {
      job_preemptable (j : Job) (ρ : work) := ρ \in job_preemption_points j
    }.  
  
  (** Next, we describe some structural properties that
      a sequence of preemption points should satisfy. *)

  (** Consider any arrival sequence. *) 
  Variable arr_seq : arrival_sequence Job.

  (** We require the sequence of preemption points to contain the beginning ... *)
  Definition beginning_of_execution_in_preemption_points :=
    forall j, arrives_in arr_seq j -> 0 \in job_preemption_points j.
  
  (** ... and the end of execution for any job j. *)
  Definition end_of_execution_in_preemption_points :=
    forall j, arrives_in arr_seq j -> last0 (job_preemption_points j) = job_cost j.

  (** We require the sequence of preemption points to be a non-decreasing sequence. *)
  Definition preemption_points_is_nondecreasing_sequence :=
    forall j, arrives_in arr_seq j -> nondecreasing_sequence (job_preemption_points j).

  (** We define a valid job-level model with limited preemptions 
      as a conjunction of the hypotheses above.  *)
  Definition valid_limited_preemptions_job_model :=
    beginning_of_execution_in_preemption_points /\
    end_of_execution_in_preemption_points /\
    preemption_points_is_nondecreasing_sequence.
  
End LimitedPreemptions.