Platform for models with limited preemptions

In module we introduce the notion of whether a job can be preempted at a given time (using a predicate can_be_preempted). In this section, we instantiate can_be_preempted for the model with fixed preemption points and model with floating nonpreemptive regions.
Module ModelWithLimitedPreemptions.

  Import Job UniprocessorSchedule LimitedPreemptionPlatform.

  (* In this section, we instantiate can_be_preempted for the model with fixed preemption points and
     the model with floating nonpreemptive regions. We also prove that the definitions are correct. *)

  Section ModelsWithLimitedPreemptions.

    Context {Task: eqType}.
    Variable task_cost: Task time.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_task: Job Task.

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

    (* Next, consider a function that maps a job to the sequence of its preemption points. *)
    Variable job_preemption_points: Job seq time.

    (* In this section, we provide a set of hypotheses for the models with limited preemptions. *)
    Section Definitions.

      (* In this section, we introduce the job-level definitions.
         They are the same for both models. *)

      Section ModelWithLimitedPreemptions.

        (* First, we define a function that maps a job to the 
           sequence of lengths of its nonpreemptive segments. *)

        Definition lengths_of_segments j := 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_nps (j : Job) := max0 (lengths_of_segments j).

        (* Similarly, job_last is a function that maps a job to the  
           length of the last nonpreemptive segment. *)

        Definition job_last_nps (j : Job) := last0 (lengths_of_segments j).

        (* Next, we describe some structural properties that
           a sequence of preemption points should satisfy. *)

        (* (1) The sequence of preemption points of a job with zero cost is equal to 0; 0. *)
        Definition job_with_zero_cost_consists_of_one_empty_segment :=
           j, arrives_in arr_seq j job_cost j = 0 job_preemption_points j = [::0; 0].

        (* (2) The last nonpreemptive segment of a job with positive cost cannot be empty. *)
        Definition last_segment_is_positive :=
           j, arrives_in arr_seq j job_cost j > 0 job_last_nps j > 0.

        (* (3) We also require the sequence of preemption points to contain the beginning... *)
        Definition beginning_of_execution_in_preemption_points :=
           j, arrives_in arr_seq j first0 (job_preemption_points j) = 0.

        (* ... and (4) the end of execution for any job j.*)
        Definition end_of_execution_in_preemption_points :=
           j, arrives_in arr_seq j last0 (job_preemption_points j) = job_cost j.

        (* (5) We require the sequence of preemption points to be a nondecreasing sequence. *)
        Definition preemption_points_is_nondecreasing_sequence :=
           (j: Job),
            arrives_in arr_seq j
            nondecreasing_sequence (job_preemption_points j).

        (* Finally, we define a job-level model with limited preemptions 
           as a concatenation of the hypotheses above.  *)

        Definition limited_preemptions_job_model :=

      End ModelWithLimitedPreemptions.

      (* In this section, we define the model with fixed preemption points. *)
      Section ModelWithFixedPreemptionPoints.

        (* Consider a function that maps a task to the sequence of its preemption points. *)
        Variable task_preemption_points: Task seq time.

        (* Similarly to job's nonpreemptive segments, we define the length of the max
           nonpreemptive segment and lenght of the last nonpreemptive segment. *)

        Definition task_last_nps tsk := last0 (distances (task_preemption_points tsk)).
        Definition task_max_nps tsk := max0 (distances (task_preemption_points tsk)).

        (* Consider an arbitrary task set ts. *)
        Variable ts: list Task.

        (* Next, we describe some structural properties that
           a sequence of preemption points of task should satisfy. *)

        (* (1) We require the sequence of preemption points to contain the beginning... *)
        Definition task_beginning_of_execution_in_preemption_points :=
           tsk, tsk \in ts first0 (task_preemption_points tsk) = 0.

        (* ... and (2) the end of execution for any job j.*)
        Definition task_end_of_execution_in_preemption_points :=
           tsk, tsk \in ts last0 (task_preemption_points tsk) = task_cost tsk.

        (* (3) We require the sequence of preemption points 
           to be a nondecreasing sequence. *)

        Definition task_preemption_points_is_nondecreasing_sequence :=
           tsk, tsk \in ts nondecreasing_sequence (task_preemption_points tsk).

        (* (4) Next, we require the number of nonpreemptive segments of a job to be 
           equal to the number of nonpreemptive segments of its task. Note that 
           some of nonpreemptive segments of a job can have zero length, nonetheless
           the number of segments should match. *)

        Definition job_consists_of_the_same_number_of_segments_as_task :=
            arrives_in arr_seq j
            size (job_preemption_points j) = size (task_preemption_points (job_task j)).

        (* (5) We require lengths of nonpreemptive segments of a job to be bounded 
           by lenghts of the corresponding segments of its task.  *)

        Definition lengths_of_task_segments_bound_length_of_job_segments :=
           j n,
            arrives_in arr_seq j
            nth 0 (distances (job_preemption_points j)) n
             nth 0 (distances (task_preemption_points (job_task j))) n.

        (* (6) Lastly, we ban empty nonpreemptive segments for tasks. *)
        Definition task_segments_are_nonempty :=
           tsk n,
            (tsk \in ts)
            n < size (distances (task_preemption_points tsk))
            ε nth 0 (distances (task_preemption_points tsk)) n.

        (* We define a task-level model with fixed preemption points 
           as a concatenation of the hypotheses above. *)

        Definition fixed_preemption_points_task_model :=

        (* We define the model with fixed preemption points as 
           the model with fixed preemptions points at the task-level
           and model with limited preemptions at the job-level. *)

        Definition fixed_preemption_points_model :=

      End ModelWithFixedPreemptionPoints.

      (* In this section, we define the model with floating nonpreemptive regions. *)
      Section ModelWithFloatingNonpreemptiveRegions.

        (* Consider a function task_max_nps that maps a task to 
           the lenght of its max nonpreemptive segment. *)

        Variable task_max_nps: Task time.

        (* We require task_max_nps (job_task j) to be an upper bound 
           of the lenght of the max nonpreemptive segment of job j. *)

        Definition job_max_np_segment_le_task_max_np_segment :=
           (j: Job),
            arrives_in arr_seq j
            job_max_nps j task_max_nps (job_task j).

        (* We define the model with floating nonpreemptive regions as 
           the model with floating nonpreemptive regions at the task-level
           and model with limited preemptions at the job-level.  *)

        Definition model_with_floating_nonpreemptive_regions :=

      End ModelWithFloatingNonpreemptiveRegions.

      (* Given a list of preemption points for each job, we define the function 
         can_be_preempted for the model with limited preemptions as follows. We say 
         that job j can be preempted at time t iff the service received by j at 
         time t belongs to the list of preemptions points. *)

      Definition can_be_preempted_for_model_with_limited_preemptions (j: Job) (progr: time) :=
        progr \in job_preemption_points j.

      (* Based on the definition of the model with limited preemptions, 
         we define a schedule with limited preemptions. *)

      Definition is_schedule_with_limited_preemptions (sched: schedule Job) :=
         j t,
          arrives_in arr_seq j
          ~~ can_be_preempted_for_model_with_limited_preemptions j (service sched j t)
          scheduled_at sched j t.

    End Definitions.

    (* In this section, we prove correctness of the model defined by 
       function model_with_limited_preemptions. *)

    Section Lemmas.

      (* Consider any uniprocessor schedule with limited preemptions...*)
      Variable sched: schedule Job.
      Hypothesis H_is_schedule_with_limited_preemptions:
        is_schedule_with_limited_preemptions sched.

      (* ...where jobs do not execute after their completion. *)
      Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.

      (* Next, we assume that preemption points are defined by the model with 
         floating nonpreemptive regions. Note that the assumptions of the
         model with floating nonpreemptive regions are a strict subset of
         the assumptions of the model with fixed preemption points. This 
         guaranties that the results below work for both models. *)

      Variable task_max_nps: Task time.
      Hypothesis H_limited_preemptions_job_model: limited_preemptions_job_model.
      Hypothesis H_job_max_np_segment_le_task_max_np_segment:
        job_max_np_segment_le_task_max_np_segment task_max_nps.

      (* First, we prove a few basic auxiliary lemmas. *)
      Section AuxiliaryLemmas.

        (* Consider a job j. *)
        Variable j: Job.
        Hypothesis H_j_arrives: arrives_in arr_seq j.

        (* We prove that the list of preemption points is not empty. *)
        Lemma list_of_preemption_point_is_not_empty:
          0 < size (job_preemption_points j).

        (* We prove that 0 is a preemption point. *)
        Lemma zero_in_preemption_points: 0 \in job_preemption_points j.

        (* Next, we prove that the cost of a job is a preemption point. *)
        Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemption_points j.

        (* As a corollary, we prove that the size of the sequence of nonpreemptive points is at least 2. *)
        Corollary number_of_preemption_points_at_least_two: 2 size (job_preemption_points j).

      End AuxiliaryLemmas.

      (* We prove that the fixed_preemption_point_model function defines 
         a correct preemption model. *)

      Lemma model_with_fixed_preemption_points_is_correct:
        correct_preemption_model arr_seq sched can_be_preempted_for_model_with_limited_preemptions.

      (* Next we prove that the fixed_preemption_point_model function defines 
         a model with bounded nonpremtive regions. *)

      Lemma model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions:
          job_cost job_task arr_seq can_be_preempted_for_model_with_limited_preemptions
          job_max_nps task_max_nps.
    End Lemmas.

  End ModelsWithLimitedPreemptions.

End ModelWithLimitedPreemptions.