From 7b38326fe706ad686ad5d2d3436ee4def1291aae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 22 Nov 2019 20:08:36 +0100
Subject: [PATCH] split job and tasks aspects in preemption.valid_model
The notion of a valid preemption model for *jobs* should
not depend on any task abstraction. Split the two notions.
---
restructuring/model/preemption/valid_model.v | 89 +++----------------
.../task/preemption/fully_nonpreemptive.v | 2 +-
.../model/task/preemption/fully_preemptive.v | 2 +-
.../model/task/preemption/parameters.v | 79 ++++++++++++++++
4 files changed, 95 insertions(+), 77 deletions(-)
diff --git a/restructuring/model/preemption/valid_model.v b/restructuring/model/preemption/valid_model.v
index d57aa0543..38ae8fb60 100644
--- a/restructuring/model/preemption/valid_model.v
+++ b/restructuring/model/preemption/valid_model.v
@@ -1,27 +1,15 @@
Require Export rt.restructuring.model.preemption.job.parameters.
-Require Export rt.restructuring.model.task.preemption.parameters.
(** * Platform with limited preemptions *)
-(** Since the notion of preemption points is based on an user-provided
- predicate (variable job_preemptable), it does not guarantee that
- the scheduler will enforce correct behavior. For that, we must
- define additional predicates. *)
+(** In the follwoing, we define properties that any reasonable job preemption
+ model must satisfy. *)
Section PreemptionModel.
- (** Consider any type of tasks ... *)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
-
- (** ... and any type of jobs associated with these tasks. *)
+ (** Consider any type of jobs... *)
Context {Job : JobType}.
- Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (** In addition, we assume the existence of a function mapping a
- task to its maximal non-preemptive segment ... *)
- Context `{TaskMaxNonpreemptiveSegment Task}.
-
(** ... and the existence of a predicate mapping a job and
its progress to a boolean value saying whether this job is
preemptable at its current point of execution. *)
@@ -37,11 +25,6 @@ Section PreemptionModel.
(** ... and any given schedule. *)
Variable sched : schedule PState.
- (** For simplicity, let's define some local names. *)
- Let job_pending := pending sched.
- Let job_completed_by := completed_by sched.
- Let job_scheduled_at := scheduled_at sched.
-
(** In this section, we define the notion of a valid preemption model. *)
Section ValidPreemptionModel.
@@ -50,26 +33,26 @@ Section PreemptionModel.
words, a job must start execution to become non-preemptive. *)
Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
job_preemptable j 0.
-
+
(** And vice versa, a job cannot remain non-preemptive after its completion. *)
- Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
+ Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
job_preemptable j (job_cost j).
-
- (** Next, if a job j is not preemptive at some time instant t,
- then j must be scheduled at time t. *)
+
+ (** Next, if a job j is not preemptive at some time instant t,
+ then j must be scheduled at time t. *)
Definition not_preemptive_implies_scheduled (j : Job) :=
forall t,
~~ job_preemptable j (service sched j t) ->
- job_scheduled_at j t.
+ scheduled_at sched j t.
(** A job can start its execution only from a preemption point. *)
- Definition execution_starts_with_preemption_point (j : Job) :=
+ Definition execution_starts_with_preemption_point (j : Job) :=
forall prt,
- ~~ job_scheduled_at j prt ->
- job_scheduled_at j prt.+1 ->
+ ~~ scheduled_at sched j prt ->
+ scheduled_at sched j prt.+1 ->
job_preemptable j (service sched j prt.+1).
- (** We say that a preemption model is a valid preemption model if
+ (** We say that a preemption model is a valid preemption model if
all the assumptions given above are satisfied for any job. *)
Definition valid_preemption_model :=
forall j,
@@ -81,48 +64,4 @@ Section PreemptionModel.
End ValidPreemptionModel.
- (** Note that for analysis purposes, it is important that the
- distance between preemption points of a job is bounded. To
- ensure that, next we define the model with bounded nonpreemptive
- segment. *)
- Section ModelWithBoundedNonpreemptiveSegments.
-
- (** First we require that [task_max_nonpreemptive_segment] gives an
- upper bound for values of the function
- [job_max_nonpreemptive_segment]. *)
- Definition job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment (j: Job) :=
- job_max_nonpreemptive_segment j <= task_max_nonpreemptive_segment (job_task j).
-
- (** Next, we require that all the segments of a job [j] have
- bounded length. I.e., for any progress [Ï] of job [j] there
- exists a preemption point [pp] such that [Ï <= pp <= Ï +
- (job_max_nps j - ε)]. That is, in any time interval of length
- [job_max_nps j], there exists a preeemption point which lies
- in this interval. *)
- Definition nonpreemptive_regions_have_bounded_length (j : Job) :=
- forall (Ï : duration),
- 0 <= Ï <= job_cost j ->
- exists (pp : duration),
- Ï <= pp <= Ï + (job_max_nonpreemptive_segment j - ε) /\
- job_preemptable j pp.
-
- (** We say that the schedule enforces bounded nonpreemptive
- segments iff the predicate [job_preemptable] satisfies the two
- conditions above. *)
- Definition model_with_bounded_nonpreemptive_segments :=
- forall j,
- arrives_in arr_seq j ->
- job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
- /\ nonpreemptive_regions_have_bounded_length j.
-
- (** Finally, we say that the schedule enforces _valid_ bounded
- nonpreemptive segments iff the predicate [job_preemptable]
- defines a valid preemption model which has bounded
- non-preemptive segments . *)
- Definition valid_model_with_bounded_nonpreemptive_segments :=
- valid_preemption_model /\
- model_with_bounded_nonpreemptive_segments.
-
- End ModelWithBoundedNonpreemptiveSegments.
-
-End PreemptionModel.
\ No newline at end of file
+End PreemptionModel.
diff --git a/restructuring/model/task/preemption/fully_nonpreemptive.v b/restructuring/model/task/preemption/fully_nonpreemptive.v
index c470b16c5..297fca8b1 100644
--- a/restructuring/model/task/preemption/fully_nonpreemptive.v
+++ b/restructuring/model/task/preemption/fully_nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.valid_model.
+Require Export rt.restructuring.model.task.preemption.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/model/task/preemption/fully_preemptive.v b/restructuring/model/task/preemption/fully_preemptive.v
index a8f0f210c..654a20681 100644
--- a/restructuring/model/task/preemption/fully_preemptive.v
+++ b/restructuring/model/task/preemption/fully_preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.valid_model.
+Require Export rt.restructuring.model.task.preemption.parameters.
(** * Platform for Fully Preemptive Model *)
(** In this section, we instantiate function
diff --git a/restructuring/model/task/preemption/parameters.v b/restructuring/model/task/preemption/parameters.v
index 7d3efc635..686f863e2 100644
--- a/restructuring/model/task/preemption/parameters.v
+++ b/restructuring/model/task/preemption/parameters.v
@@ -1,5 +1,6 @@
Require Export rt.util.all.
Require Export rt.restructuring.model.preemption.job.parameters.
+Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.task.concept.
(** * Static information about preemption points *)
@@ -51,6 +52,84 @@ Section MaxAndLastNonpreemptiveSegment.
End MaxAndLastNonpreemptiveSegment.
+(** * Validity of a Preemption Model *)
+
+Section PreemptionModel.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** In addition, we assume the existence of a function mapping a
+ task to its maximal non-preemptive segment ... *)
+ Context `{TaskMaxNonpreemptiveSegment Task}.
+
+ (** ... and the existence of a predicate mapping a job and
+ its progress to a boolean value saying whether this job is
+ preemptable at its current point of execution. *)
+ Context `{JobPreemptable Job}.
+
+ (** Consider any kind of processor state model, ... *)
+ Context {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ (** ... any job arrival sequence, ... *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** ... and any given schedule. *)
+ Variable sched : schedule PState.
+
+ (** For analysis purposes, it is important that the distance between
+ preemption points of a job is bounded. To ensure that, next we define the
+ model with bounded nonpreemptive segment. *)
+ Section ModelWithBoundedNonpreemptiveSegments.
+
+ (** First we require that [task_max_nonpreemptive_segment] gives an
+ upper bound for values of the function
+ [job_max_nonpreemptive_segment]. *)
+ Definition job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment (j: Job) :=
+ job_max_nonpreemptive_segment j <= task_max_nonpreemptive_segment (job_task j).
+
+ (** Next, we require that all the segments of a job [j] have
+ bounded length. I.e., for any progress [Ï] of job [j] there
+ exists a preemption point [pp] such that [Ï <= pp <= Ï +
+ (job_max_nps j - ε)]. That is, in any time interval of length
+ [job_max_nps j], there exists a preeemption point which lies
+ in this interval. *)
+ Definition nonpreemptive_regions_have_bounded_length (j : Job) :=
+ forall (Ï : duration),
+ 0 <= Ï <= job_cost j ->
+ exists (pp : duration),
+ Ï <= pp <= Ï + (job_max_nonpreemptive_segment j - ε) /\
+ job_preemptable j pp.
+
+ (** We say that the schedule enforces bounded nonpreemptive
+ segments iff the predicate [job_preemptable] satisfies the two
+ conditions above. *)
+ Definition model_with_bounded_nonpreemptive_segments :=
+ forall j,
+ arrives_in arr_seq j ->
+ job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
+ /\ nonpreemptive_regions_have_bounded_length j.
+
+ (** Finally, we say that the schedule enforces _valid_ bounded
+ nonpreemptive segments iff the predicate [job_preemptable]
+ defines a valid preemption model which has bounded
+ non-preemptive segments . *)
+ Definition valid_model_with_bounded_nonpreemptive_segments :=
+ valid_preemption_model arr_seq sched /\
+ model_with_bounded_nonpreemptive_segments.
+
+ End ModelWithBoundedNonpreemptiveSegments.
+
+End PreemptionModel.
+
(** * Task's Run-to-Completion Threshold *)
(** Since a task model may not provide exact information about
preemption point of a task, task's run-to-completion threshold
--
GitLab