Library rt.restructuring.model.preemption.preemption_time


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

Welcome to Coq 8.10.1 (October 2019)

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

From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import ideal_schedule.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model Require Import processor.ideal.
From rt.restructuring.model.preemption Require Import job.parameters task.parameters valid_model.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Preemption Time in Ideal Uni-Processor Model

In this section we define the notion of preemption _time_ for ideal uni-processor model.
Section PreemptionTime.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskMaxNonpreemptiveSegment Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

In addition, we assume the existence of a function mapping a task to its maximal non-preemptive segment ...
  Context `{TaskMaxNonpreemptiveSegment Task}.

... and the existence of a function mapping a job and its progress to a boolean value saying whether this job is preemptable at its current point of execution.
  Context `{JobPreemptable 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 uniprocessor schedule of this arrival sequence ...
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_jobs_come_from_arrival_sequence:
    jobs_come_from_arrival_sequence sched arr_seq.

We say that a time instant t is a preemption time iff the job that is currently scheduled at t can be preempted (according to the predicate).
  Definition preemption_time (t : instant) :=
    if sched t is Some j then
      job_preemptable j (service sched j t)
    else true.

In this section we prove a few basic properties of the preemption_time predicate.
  Section Lemmas.

Consider a valid model with bounded nonpreemptive segments.
    Hypothesis H_model_with_bounded_nonpreemptive_segments:
      valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

Then, we show that time 0 is a preemption time.
    Lemma zero_is_pt: preemption_time 0.

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

1 subgoal (ID 189)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  ============================
  preemption_time 0

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

    Proof.
      unfold preemption_time.

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

1 subgoal (ID 191)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  ============================
  match sched 0 with
  | Some j => job_preemptable j (service sched j 0)
  | None => true
  end

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

      case SCHED: (sched 0) ⇒ [j | ]; last by done.

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

1 subgoal (ID 218)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  j : Job
  SCHED : sched 0 = Some j
  ============================
  job_preemptable j (service sched j 0)

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

      move: (SCHED) ⇒ /eqP; rewrite -scheduled_at_def; move ⇒ ARR.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 302)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  j : Job
  SCHED : sched 0 = Some j
  ARR : scheduled_at sched j 0
  ============================
  job_preemptable j (service sched j 0)

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

      apply H_jobs_come_from_arrival_sequence in ARR.

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

1 subgoal (ID 303)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  j : Job
  SCHED : sched 0 = Some j
  ARR : arrives_in arr_seq j
  ============================
  job_preemptable j (service sched j 0)

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

      rewrite /service /service_during big_geq; last by done.

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

1 subgoal (ID 328)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  j : Job
  SCHED : sched 0 = Some j
  ARR : arrives_in arr_seq j
  ============================
  job_preemptable j 0

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

      destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].

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

1 subgoal (ID 335)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  j : Job
  SCHED : sched 0 = Some j
  ARR : arrives_in arr_seq j
  T1 : valid_preemption_model arr_seq sched
  T2 : model_with_bounded_nonpreemptive_segments arr_seq
  ============================
  job_preemptable j 0

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

        by move: (T1 j ARR) ⇒ [PP _].
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

    Qed.

Also, we show that the first instant of execution is a preemption time.
    Lemma first_moment_is_pt:
      ∀ j prt,
        arrives_in arr_seq j →
        ~~ scheduled_at sched j prt →
        scheduled_at sched j prt.+1 →
        preemption_time prt.+1.

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

1 subgoal (ID 199)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  ============================
  forall (j : Job) (prt : instant),
  arrives_in arr_seq j ->
  ~~ scheduled_at sched j prt ->
  scheduled_at sched j (succn prt) -> preemption_time (succn prt)

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

    Proof.
      intros s pt ARR NSCHED SCHED.

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

1 subgoal (ID 204)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  s : Job
  pt : instant
  ARR : arrives_in arr_seq s
  NSCHED : ~~ scheduled_at sched s pt
  SCHED : scheduled_at sched s (succn pt)
  ============================
  preemption_time (succn pt)

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

      unfold preemption_time.

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

1 subgoal (ID 206)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  s : Job
  pt : instant
  ARR : arrives_in arr_seq s
  NSCHED : ~~ scheduled_at sched s pt
  SCHED : scheduled_at sched s (succn pt)
  ============================
  match sched (succn pt) with
  | Some j => job_preemptable j (service sched j (succn pt))
  | None => true
  end

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

      move: (SCHED); rewrite scheduled_at_def; move ⇒ /eqP SCHED2; rewrite SCHED2; clear SCHED2.

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

1 subgoal (ID 251)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  s : Job
  pt : instant
  ARR : arrives_in arr_seq s
  NSCHED : ~~ scheduled_at sched s pt
  SCHED : scheduled_at sched s (succn pt)
  ============================
  job_preemptable s (service sched s (succn pt))

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

      destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].

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

1 subgoal (ID 257)
  
  Task : TaskType
  H : TaskCost Task
  H0 : TaskMaxNonpreemptiveSegment Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : JobArrival Job
  H3 : JobCost Job
  H4 : TaskMaxNonpreemptiveSegment Task
  H5 : JobPreemptable Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (processor_state Job)
  H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
                                        arr_seq
  H_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
                                                 arr_seq sched
  s : Job
  pt : instant
  ARR : arrives_in arr_seq s
  NSCHED : ~~ scheduled_at sched s pt
  SCHED : scheduled_at sched s (succn pt)
  T1 : valid_preemption_model arr_seq sched
  T2 : model_with_bounded_nonpreemptive_segments arr_seq
  ============================
  job_preemptable s (service sched s (succn pt))

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

        by move: (T1 s ARR) ⇒ [_ [_ [_ P]]]; apply P.

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

No more subgoals.

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

    Qed.

  End Lemmas.

End PreemptionTime.