Library prosa.classic.model.schedule.uni.limited.platform.nonpreemptive

Platform for fully nonpreemptive model

In module uni.limited.platform 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 fully nonpreemptive model and prove its correctness.

Module FullyNonPreemptivePlatform.

  Import Job SporadicTaskset UniprocessorSchedule Priority
         Service LimitedPreemptionPlatform.

  Section FullyNonPreemptiveModel.

    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 arrival sequence with consistent, non-duplicate arrivals. *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.

    (* Next, consider any uniprocessor nonpreemptive schedule of this arrival sequence...*)
    Variable sched: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
    Hypothesis H_nonpreemptive_sched:
      NonpreemptiveSchedule.is_nonpreemptive_schedule job_cost sched.

    (* ... where jobs do not execute before their arrival nor after completion. *)
    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.

    (* For simplicity, let's define some local names. *)
    Let job_pending := pending job_arrival job_cost sched.
    Let job_completed_by := completed_by job_cost sched.
    Let job_scheduled_at := scheduled_at sched.

    (* Assume that a job cost cannot be larger than a task cost. *)
    Hypothesis H_job_cost_le_task_cost:
      cost_of_jobs_from_arrival_sequence_le_task_cost
        task_cost job_cost job_task arr_seq.

    (* We say that the model is fully nonpreemptive
       iff every job cannot be preempted until its completion. *)
    Definition can_be_preempted_for_fully_nonpreemptive_model (j: Job) (progr: time) :=
      (progr == 0) || (progr == job_cost j ).

    (* Since in a fully nonpreemptive model a job cannot be preempted after
       it starts the execution, job_max_nps is equal to job_cost. *)
    Let job_max_nps (j: Job) := job_cost j.

    (* In order to bound job_max_nps, task_max_nps should be equal to task_cost. *)
    Let task_max_nps (tsk: Task) := task_cost tsk.

    (* Then, we prove that fully_nonpreemptive_model is a correct preemption model... *)
    Lemma fully_nonpreemptive_model_is_correct:
      correct_preemption_model arr_seq sched can_be_preempted_for_fully_nonpreemptive_model.

    (* ... and has bounded nonpreemptive regions. *)
    Lemma fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions:
      model_with_bounded_nonpreemptive_segments
        job_cost job_task arr_seq can_be_preempted_for_fully_nonpreemptive_model job_max_nps task_max_nps.

  End FullyNonPreemptiveModel.

End FullyNonPreemptivePlatform.