Library rt.restructuring.model.preemption.job.instance.limited
(* ----------------------------------[ 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.preemption Require Import job.parameters task.parameters.
Definition of a parameter relating a job
to the sequence of its preemption points.
Platform for Models with Limited Preemptions
In this section, we instantiate [job_preemptable] for the model with limited preemptions and introduce a set of requirements for function [job_preemption_points], so it is coherent with limited preemptions model.
Consider any type of jobs.
In addition, assume the existence of a function that
maps a job to the sequence of its preemption points.
In the model with limited preemptions a job can be preempted
if its progress is equal to one of the preemption points.
Global Instance limited_preemptions_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := ρ \in job_preemption_points j
}.
{
job_preemptable (j : Job) (ρ : work) := ρ \in job_preemption_points j
}.
Next, we describe some structural properties that
a sequence of preemption points should satisfy.
Consider any arrival sequence.
We require the sequence of preemption points to contain the beginning ...
Definition beginning_of_execution_in_preemption_points :=
∀ j, arrives_in arr_seq j → 0 \in job_preemption_points j.
∀ j, arrives_in arr_seq j → 0 \in job_preemption_points j.
... and the end of execution for any job j.
Definition end_of_execution_in_preemption_points :=
∀ j, arrives_in arr_seq j → last0 (job_preemption_points j) = job_cost j.
∀ j, arrives_in arr_seq j → last0 (job_preemption_points j) = job_cost j.
We require the sequence of preemption points to be a non-decreasing sequence.
Definition preemption_points_is_nondecreasing_sequence :=
∀ j, arrives_in arr_seq j → nondecreasing_sequence (job_preemption_points j).
∀ j, arrives_in arr_seq j → nondecreasing_sequence (job_preemption_points j).
We define a valid job-level model with limited preemptions
as a conjunction of the hypotheses above.