Library rt.restructuring.model.schedule.preemption_time
Require Export rt.restructuring.model.preemption.parameter.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Throughout this file, we assume ideal uniprocessor schedules.
Preemption Time in Ideal Uni-Processor Model
In this section we define the notion of preemption time for ideal uni-processor model.
Consider any type of jobs...
... and assume 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.
Consider any arrival sequence with consistent arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
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.
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.
End PreemptionTime.
if sched t is Some j then
job_preemptable j (service sched j t)
else true.
End PreemptionTime.