Library rt.restructuring.model.preemption.valid_schedule
(* ----------------------------------[ 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.model Require Import processor.ideal.
From rt.restructuring.model.preemption Require Import job.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Schedule with Limited Preemptions
In this section we introduce the notion of preemptions-aware schedule.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Consider any arrival sequence.
Next, consider any ideal uniprocessor schedule of this arrival sequence.
Based on the definition of the model with preemption points,
we define a valid schedule with limited preemptions.
Definition valid_schedule_with_limited_preemptions :=
∀ j t,
arrives_in arr_seq j →
~~ job_preemptable j (service sched j t) →
scheduled_at sched j t.
End ScheduleWithLimitedPreemptions.
∀ j t,
arrives_in arr_seq j →
~~ job_preemptable j (service sched j t) →
scheduled_at sched j t.
End ScheduleWithLimitedPreemptions.