nonpreemptive.v 3.64 KB
Newer Older
1 2
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
3
Require Import rt.restructuring.analysis.definitions.job_properties.
4
Require Import rt.restructuring.model.task.concept.
5 6 7
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
8
Require Import rt.restructuring.model.task.preemption.parameters.
9

10
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
11
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
12 13
Require Import rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
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 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
    to completion threshold] to the fully non-preemptive model
    indeed defines a valid run-to-completion threshold function. *)
Section TaskRTCThresholdFullyNonPreemptive.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}. 
  Context `{TaskCost Task}.

  (**  ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  
  (** Consider any arrival sequence with consistent arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

  (** Next, consider any ideal non-preemptive uniprocessor schedule of
      this arrival sequence ... *)
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched.

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

  (** First we prove that if the cost of a job j is equal to 0, then 
      [job_run_to_completion_threshold j = 0] ...  *)
  Fact job_rtc_threshold_is_0:
    forall j,
      job_cost j = 0 -> 
      job_run_to_completion_threshold j = 0.
  Proof.
    intros.
    apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
    unfold job_run_to_completion_threshold.
      by rewrite H3; compute.
  Qed.
  
  (** ... and ε otherwise. *)
  Fact job_rtc_threshold_is_ε:
    forall j,
      job_cost j > 0 ->
      arrives_in arr_seq j ->
      job_run_to_completion_threshold j = ε.
  Proof.
    intros ? ARRj POSj; unfold ε in *.
    unfold job_run_to_completion_threshold.
    rewrite job_last_nps_is_job_cost.
      by rewrite subKn.
  Qed.
  
  (** Consider a task with a positive cost. *)
  Variable tsk : Task.
  Hypothesis H_positive_cost : 0 < task_cost tsk.
                
  (** Then, we prove that [task_run_to_completion_threshold] function
      defines a valid task's run to completion threshold. *)     
  Lemma fully_nonpreemptive_valid_task_run_to_completion_threshold:
    valid_task_run_to_completion_threshold arr_seq tsk.
  Proof.
    intros; split.
    - by unfold task_run_to_completion_threshold_le_task_cost.
    - intros j ARR TSK.
      rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.
      edestruct (posnP (job_cost j)) as [ZERO|POS].
      + by rewrite job_rtc_threshold_is_0.
      + by erewrite job_rtc_threshold_is_ε; eauto 2. 
  Qed.
    
End TaskRTCThresholdFullyNonPreemptive.
Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.