Library rt.restructuring.model.preemption.task.instance.floating
(* ----------------------------------[ 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 Require Import model.job model.task.
From rt.restructuring.model.preemption Require Import job.parameters task.parameters.
From rt.restructuring.model.preemption Require Import job.instance.limited.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Platform for Models with Floating Non-Preemptive Regions
In this section, we introduce a set of requirements for function [task_max_nonpr_segment], so it is coherent with model with floating non-preemptive regions.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptionPoints Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptionPoints Job}.
Consider any arrival sequence.
We require [task_max_nonpreemptive_segment (job_task j)] to be
an upper bound of the lenght of the max nonpreemptive segment of
job [j].
Definition job_max_np_segment_le_task_max_np_segment :=
∀ (j : Job),
arrives_in arr_seq j →
job_max_nonpreemptive_segment j ≤ task_max_nonpreemptive_segment (job_task j).
∀ (j : Job),
arrives_in arr_seq j →
job_max_nonpreemptive_segment j ≤ task_max_nonpreemptive_segment (job_task j).
We define a valid model with floating nonpreemptive regions as the
model with floating nonpreemptive regions at the task-level and
valid model with limited preemptions at the job-level.