From 6c4a4aeea94d42355180151d10591b55327f6594 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 25 Mar 2022 22:50:40 +0100
Subject: [PATCH] import and comment tweaks in results & analysis
---
.../facts/preemption/rtc_threshold/floating.v | 8 +++---
.../facts/preemption/rtc_threshold/limited.v | 13 ++++-----
.../preemption/rtc_threshold/nonpreemptive.v | 13 +++++----
.../preemption/rtc_threshold/preemptive.v | 25 +++++++++--------
analysis/facts/preemption/task/floating.v | 8 +++---
.../facts/preemption/task/nonpreemptive.v | 18 ++++++-------
analysis/facts/preemption/task/preemptive.v | 20 +++++++-------
results/edf/optimality.v | 27 +++++++++----------
results/edf/rta/bounded_nps.v | 10 +++----
results/edf/rta/bounded_pi.v | 10 +++----
results/edf/rta/floating_nonpreemptive.v | 10 +++----
results/edf/rta/fully_nonpreemptive.v | 10 +++----
results/edf/rta/fully_preemptive.v | 10 +++----
results/edf/rta/limited_preemptive.v | 10 +++----
results/fifo/rta.v | 10 +++----
15 files changed, 97 insertions(+), 105 deletions(-)
diff --git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index 68cc14ee5..0c286cb6a 100644
--- a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -7,9 +7,6 @@ Require Export prosa.model.task.preemption.floating_nonpreemptive.
threshold] for the model with floating non-preemptive regions. *)
Section TaskRTCThresholdFloatingNonPreemptiveRegions.
- (** Furthermore, we assume the task model with floating non-preemptive regions. *)
- #[local] Existing Instance floating_preemptive_rtc_threshold.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -19,7 +16,10 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
-
+
+ (** We assume a task model with floating non-preemptive regions. *)
+ #[local] Existing Instance floating_preemptive_rtc_threshold.
+
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 567ce69b0..2ff20119d 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -1,9 +1,6 @@
Require Export prosa.analysis.facts.preemption.task.limited.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
-Require Import prosa.model.task.preemption.limited_preemptive.
-
-(** Furthermore, we assume the task model with fixed preemption points. *)
-Require Import prosa.model.preemption.limited_preemptive.
+Require Export prosa.model.task.preemption.limited_preemptive.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
@@ -11,10 +8,6 @@ Require Import prosa.model.preemption.limited_preemptive.
indeed defines a valid run-to-completion threshold function. *)
Section TaskRTCThresholdLimitedPreemptions.
- (** We assume the task model with fixed preemption points. *)
- #[local] Existing Instance limited_preemptive_job_model.
- #[local] Existing Instance limited_preemptions_rtc_threshold.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -26,6 +19,10 @@ Section TaskRTCThresholdLimitedPreemptions.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptionPoints Job}.
+
+ (** We assume a task model with fixed preemption points. *)
+ #[local] Existing Instance limited_preemptive_job_model.
+ #[local] Existing Instance limited_preemptions_rtc_threshold.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index cbb93e198..6b7ae3a73 100644
--- a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,6 +1,5 @@
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
-Require Import prosa.model.preemption.fully_nonpreemptive.
-Require Import prosa.model.task.preemption.fully_nonpreemptive.
+Require Export prosa.model.task.preemption.fully_nonpreemptive.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
@@ -8,11 +7,6 @@ Require Import prosa.model.task.preemption.fully_nonpreemptive.
indeed defines a valid run-to-completion threshold function. *)
Section TaskRTCThresholdFullyNonPreemptive.
- (** We assume the fully non-preemptive task model. *)
- #[local] Existing Instance fully_nonpreemptive_job_model.
- #[local] Existing Instance fully_nonpreemptive_task_model.
- #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -22,6 +16,11 @@ Section TaskRTCThresholdFullyNonPreemptive.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
+
+ (** We assume a fully non-preemptive task model. *)
+ #[local] Existing Instance fully_nonpreemptive_job_model.
+ #[local] Existing Instance fully_nonpreemptive_task_model.
+ #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
index 8edd7e222..aef7dc2d6 100644
--- a/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -1,18 +1,12 @@
-(** Furthermore, we assume the fully preemptive task model. *)
-Require Import prosa.model.preemption.fully_preemptive.
-Require Import prosa.model.task.preemption.fully_preemptive.
-Require Import prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export prosa.model.preemption.fully_preemptive.
+Require Export prosa.model.task.preemption.fully_preemptive.
(** * Task's Run to Completion Threshold *)
-(** In this section, we prove that instantiation of function [task run
- to completion threshold] to the fully preemptive model
- indeed defines a valid run-to-completion threshold function. *)
-Section TaskRTCThresholdFullyPreemptiveModel.
- (** We assume that jobs and tasks are fully preemptive. *)
- #[local] Existing Instance fully_preemptive_job_model.
- #[local] Existing Instance fully_preemptive_task_model.
- #[local] Existing Instance fully_preemptive_rtc_threshold.
+(** In this section, we prove that the instantiation of the task
+ run-to-completion threshold for the fully preemptive model is valid. *)
+Section TaskRTCThresholdFullyPreemptiveModel.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
@@ -22,7 +16,12 @@ Section TaskRTCThresholdFullyPreemptiveModel.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
-
+
+ (** Assume that jobs and tasks are fully preemptive. *)
+ #[local] Existing Instance fully_preemptive_job_model.
+ #[local] Existing Instance fully_preemptive_task_model.
+ #[local] Existing Instance fully_preemptive_rtc_threshold.
+
(** Next, consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
index b6a9cf733..4b3b8d282 100644
--- a/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -1,11 +1,11 @@
Require Export prosa.analysis.facts.preemption.job.limited.
-Require Import prosa.model.task.preemption.floating_nonpreemptive.
-Require Import prosa.model.preemption.limited_preemptive.
-
+Require Export prosa.model.task.preemption.floating_nonpreemptive.
+Require Export prosa.model.preemption.limited_preemptive.
(** * Platform for Floating Non-Preemptive Regions Model *)
+
(** In this section, we prove that instantiation of functions
- [job_preemptable and task_max_nonpreemptive_segment] to the model
+ [job_preemptable] and [task_max_nonpreemptive_segment] for the model
with floating non-preemptive regions indeed defines a valid
preemption model with bounded non-preemptive regions. *)
Section FloatingNonPreemptiveRegionsModel.
diff --git a/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
index 807a26a70..fbd95cd1b 100644
--- a/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ -1,19 +1,14 @@
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
-Require Import prosa.model.preemption.fully_nonpreemptive.
-Require Import prosa.model.task.preemption.fully_nonpreemptive.
+Require Export prosa.model.task.preemption.fully_nonpreemptive.
(** * Platform for Fully Non-Preemptive Model *)
+
(** In this section, we prove that instantiation of functions
- [job_preemptable and task_max_nonpreemptive_segment] to the fully
+ [job_preemptable] and [task_max_nonpreemptive_segment] to the fully
non-preemptive model indeed defines a valid preemption model with
bounded non-preemptive regions. *)
Section FullyNonPreemptiveModel.
- (** We assume the fully non-preemptive task model. *)
- #[local] Existing Instance fully_nonpreemptive_job_model.
- #[local] Existing Instance fully_nonpreemptive_task_model.
- #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -24,6 +19,11 @@ Section FullyNonPreemptiveModel.
Context `{JobArrival Job}.
Context `{JobCost Job}.
+ (** Assume a fully non-preemptive task model. *)
+ #[local] Existing Instance fully_nonpreemptive_job_model.
+ #[local] Existing Instance fully_nonpreemptive_task_model.
+ #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
+
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
@@ -40,7 +40,7 @@ Section FullyNonPreemptiveModel.
Hypothesis H_valid_job_cost:
arrivals_have_valid_job_costs arr_seq.
- (** Then we prove that [fully_nonpreemptive_model] function
+ (** Then we prove that the [fully_nonpreemptive_model] function
defines a model with bounded non-preemptive regions.*)
Lemma fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
diff --git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index 7b7caa698..d73ba3edf 100644
--- a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -1,19 +1,14 @@
-Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.preemption.job.preemptive.
-Require Import prosa.model.task.preemption.fully_preemptive.
+Require Export prosa.model.task.preemption.fully_preemptive.
(** * Platform for Fully Preemptive Model *)
-(** In this section, we prove that instantiation of functions
- [job_preemptable and task_max_nonpreemptive_segment] to the fully
+
+(** In this section, we prove that the instantiations of the functions
+ [job_preemptable] and [task_max_nonpreemptive_segment] for the fully
preemptive model indeed defines a valid preemption model with
bounded non-preemptive regions. *)
Section FullyPreemptiveModel.
- (** We assume that jobs and tasks are fully preemptive. *)
- #[local] Existing Instance fully_preemptive_job_model.
- #[local] Existing Instance fully_preemptive_task_model.
- #[local] Existing Instance fully_preemptive_rtc_threshold.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -24,6 +19,11 @@ Section FullyPreemptiveModel.
Context `{JobArrival Job}.
Context `{JobCost Job}.
+ (** Assume that jobs and tasks are fully preemptive. *)
+ #[local] Existing Instance fully_preemptive_job_model.
+ #[local] Existing Instance fully_preemptive_task_model.
+ #[local] Existing Instance fully_preemptive_rtc_threshold.
+
(** Consider any kind of processor state model, ... *)
Context {PState : ProcessorState Job}.
@@ -33,7 +33,7 @@ Section FullyPreemptiveModel.
(** ... and any given schedule. *)
Variable sched : schedule PState.
- (** We prove that [fully_preemptive_model] function
+ (** We prove that the [fully_preemptive_model] function
defines a model with bounded non-preemptive regions.*)
Lemma fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
diff --git a/results/edf/optimality.v b/results/edf/optimality.v
index c4e99dece..afd4d24cd 100644
--- a/results/edf/optimality.v
+++ b/results/edf/optimality.v
@@ -3,6 +3,7 @@ Require Import prosa.model.preemption.fully_preemptive.
Require Export prosa.analysis.facts.transform.edf_opt.
Require Export prosa.analysis.facts.transform.edf_wc.
Require Export prosa.analysis.facts.edf_definitions.
+Require prosa.model.priority.edf.
(** * Optimality of EDF on Ideal Uniprocessors *)
@@ -11,13 +12,18 @@ Require Export prosa.analysis.facts.edf_definitions.
schedule), then there is also an (ideal) EDF schedule in which all
deadlines are met. *)
-(** The following results assume the EDF priority policy, ... *)
-Require prosa.model.priority.edf.
-
(** ** Optimality Theorem *)
Section Optimality.
+ (** Consider any given type of jobs, each characterized by execution
+ costs, an arrival time, and an absolute deadline,... *)
+ Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+ (** ... and any valid arrival sequence of such jobs. *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
+
(** We assume the classic (i.e., Liu & Layland) model of readiness
without jitter or self-suspensions, wherein pending jobs are
always ready. *)
@@ -26,18 +32,9 @@ Section Optimality.
(** We assume that jobs are fully preemptive. *)
#[local] Existing Instance fully_preemptive_job_model.
- (** For any given type of jobs, each characterized by execution
- costs, an arrival time, and an absolute deadline,... *)
- Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
-
- (** ... and any valid job arrival sequence. *)
- Variable arr_seq: arrival_sequence Job.
- Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
-
- (** We observe that EDF is optimal in the sense that, if there exists
- any schedule in which all jobs of [arr_seq] meet their deadline,
- then there also exists an EDF schedule in which all deadlines are
- met. *)
+ (** Under these assumptions, EDF is optimal in the sense that, if there
+ exists any schedule in which all jobs of [arr_seq] meet their deadline,
+ then there also exists an EDF schedule in which all deadlines are met. *)
Theorem EDF_optimality:
(exists any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq /\
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 4c8fef8f4..7995cd09e 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -20,11 +20,6 @@ Require Export prosa.analysis.facts.busy_interval.priority_inversion.
RTA for EDF-schedulers is applicable to this instantiation. *)
Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
- (** We assume the classic (i.e., Liu & Layland) model of readiness
- without jitter or self-suspensions, wherein pending jobs are
- always ready. *)
- #[local] Existing Instance basic_ready_instance.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -38,6 +33,11 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
(** For clarity, let's denote the relative deadline of a task as [D]. *)
Let D tsk := task_deadline tsk.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 11d1b49f0..4b8b57732 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -29,11 +29,6 @@ Require Import prosa.analysis.facts.readiness.basic.
Section AbstractRTAforEDFwithArrivalCurves.
- (** We assume the classic (i.e., Liu & Layland) model of readiness
- without jitter or self-suspensions, wherein pending jobs are
- always ready. *)
- #[local] Existing Instance basic_ready_instance.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -47,6 +42,11 @@ Section AbstractRTAforEDFwithArrivalCurves.
Context {Cost : JobCost Job}.
Context `{JobPreemptable Job}.
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
(** For clarity, let's denote the relative deadline of a task as D. *)
Let D tsk := task_deadline tsk.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 8b0ace62b..b4b8490a0 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -13,11 +13,6 @@ Require Import prosa.model.priority.edf.
Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
- (** We assume the classic (i.e., Liu & Layland) model of readiness
- without jitter or self-suspensions, wherein pending jobs are
- always ready. *)
- #[local] Existing Instance basic_ready_instance.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -29,6 +24,11 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
Context `{JobArrival Job}.
Context `{JobCost Job}.
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
(** We assume that jobs are limited-preemptive. *)
#[local] Existing Instance limited_preemptive_job_model.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 042dad591..f137e31a5 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -15,11 +15,6 @@ Require Import prosa.model.priority.edf.
Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
- (** We assume the classic (i.e., Liu & Layland) model of readiness
- without jitter or self-suspensions, wherein pending jobs are
- always ready. *)
- #[local] Existing Instance basic_ready_instance.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -31,6 +26,11 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
Context `{JobArrival Job}.
Context `{JobCost Job}.
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
(** We assume that jobs and tasks are fully nonpreemptive. *)
#[local] Existing Instance fully_nonpreemptive_job_model.
#[local] Existing Instance fully_nonpreemptive_task_model.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index dae26a4fa..1d9a599e1 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -15,11 +15,6 @@ Require Import prosa.model.priority.edf.
Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
- (** We assume the classic (i.e., Liu & Layland) model of readiness
- without jitter or self-suspensions, wherein pending jobs are
- always ready. *)
- #[local] Existing Instance basic_ready_instance.
-
(** We assume that jobs and tasks are fully preemptive. *)
#[local] Existing Instance fully_preemptive_job_model.
#[local] Existing Instance fully_preemptive_task_model.
@@ -36,6 +31,11 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Context `{JobArrival Job}.
Context `{JobCost Job}.
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 832104c63..a939ad9df 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -15,11 +15,6 @@ Require Export prosa.model.priority.edf.
Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
- (** We assume the classic (i.e., Liu & Layland) model of readiness
- without jitter or self-suspensions, wherein pending jobs are
- always ready. *)
- #[local] Existing Instance basic_ready_instance.
-
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
@@ -31,6 +26,11 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
Context `{JobArrival Job}.
Context `{JobCost Job}.
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
(** We assume that jobs are limited-preemptive. *)
#[local] Existing Instance limited_preemptive_job_model.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index adae2bf93..2b8b0f5eb 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -19,11 +19,6 @@ Require Export prosa.analysis.facts.busy_interval.carry_in.
Section AbstractRTAforFIFOwithArrivalCurves.
- (** We assume the classic (i.e., Liu & Layland) model of readiness
- without jitter or self-suspensions, wherein pending jobs are
- always ready. *)
- #[local] Existing Instance basic_ready_instance.
-
(** Consider any type of tasks, each characterized by a WCET, a relative
deadline, and a run-to-completion threshold, ... *)
Context {Task : TaskType}.
@@ -39,6 +34,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
Context {Cost : JobCost Job}.
Context `{JobPreemptable Job}.
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
--
GitLab