Library rt.restructuring.model.schedule.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model Require Import job.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
In this section we introduce the notion of a non-preemptive schedule.
Consider any type of jobs ...
... and any kind of processor state model.
Consider any uniprocessor schedule.
We define a schedule to be nonpreemptive iff every job remains scheduled until completion.
Definition is_nonpreemptive_schedule :=
∀ (j : Job) (t t' : instant),
t ≤ t' →
scheduled_at sched j t →
~~ completed_by sched j t' →
scheduled_at sched j t'.
End NonpreemptiveSchedule.
∀ (j : Job) (t t' : instant),
t ≤ t' →
scheduled_at sched j t →
~~ completed_by sched j t' →
scheduled_at sched j t'.
End NonpreemptiveSchedule.