From 98e1a8977b0472de29147606836cf5985453785a Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <f20171026@goa.bits-pilani.ac.in>
Date: Thu, 24 Mar 2022 14:25:21 +0000
Subject: [PATCH] make the policy explicit in policy-compliance predicates
From a spec readability PoV, it's unfortunate that the policy that is
being respected doesn't show up in the code. The subject of definitions
should show up as an explicit argument, even if it is implicit
everywhere else. This is however difficult to realize for the current
`respects_policy_at_preemption_time` predicate due to difficulties with
coercion technicalities (see further details below).
Therefore, instead of `respects_policy_at_preemption_time`, we now have:
* `respects_JLDP_policy_at_preemption_point`
* `respects_JLFP_policy_at_preemption_point`
* `respects_FP_policy_at_preemption_point`
Further details: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/188#note_78569
Closes: #82
---
.../facts/busy_interval/priority_inversion.v | 4 +--
analysis/facts/edf_definitions.v | 6 ++--
analysis/facts/priority/edf.v | 2 +-
analysis/facts/priority/fifo.v | 2 +-
analysis/facts/priority/sequential.v | 4 +--
implementation/facts/ideal_uni/prio_aware.v | 4 +--
model/schedule/priority_driven.v | 29 ++++++++++++++-----
results/edf/optimality.v | 2 +-
results/edf/rta/bounded_nps.v | 2 +-
results/edf/rta/floating_nonpreemptive.v | 2 +-
results/edf/rta/fully_nonpreemptive.v | 2 +-
results/edf/rta/fully_preemptive.v | 2 +-
results/edf/rta/limited_preemptive.v | 2 +-
results/fifo/rta.v | 2 +-
results/fixed_priority/rta/bounded_nps.v | 4 +--
.../rta/floating_nonpreemptive.v | 4 +--
.../fixed_priority/rta/fully_nonpreemptive.v | 4 +--
results/fixed_priority/rta/fully_preemptive.v | 4 +--
.../fixed_priority/rta/limited_preemptive.v | 4 +--
19 files changed, 50 insertions(+), 35 deletions(-)
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 88c90824a..168d33a62 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -35,7 +35,7 @@ Section PriorityInversionIsBounded.
(** Consider a JLFP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Context `{JLFP_policy Job}.
+ Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive: reflexive_priorities.
Hypothesis H_priority_is_transitive: transitive_priorities.
@@ -68,7 +68,7 @@ Section PriorityInversionIsBounded.
predicate [job_preemptable] (i.e., bounded nonpreemptive
segments). *)
Hypothesis H_respects_policy:
- respects_policy_at_preemption_point arr_seq sched.
+ respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
(** Let's define some local names for clarity. *)
Let job_scheduled_at := scheduled_at sched.
diff --git a/analysis/facts/edf_definitions.v b/analysis/facts/edf_definitions.v
index a17c05415..e79404bf9 100644
--- a/analysis/facts/edf_definitions.v
+++ b/analysis/facts/edf_definitions.v
@@ -57,7 +57,7 @@ Section Equivalence.
predicate. *)
Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
EDF_schedule sched ->
- respects_policy_at_preemption_point arr_seq sched.
+ respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
Proof.
move=> EDF j' j t ARR PREEMPTION BL SCHED.
have suff: exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t'.
@@ -73,7 +73,7 @@ Section Equivalence.
the [respects_policy_at_preemption_point] predicate is also an EDF
schedule in the sense of [EDF_schedule]. *)
Lemma respects_policy_at_preemption_point_implies_EDF_schedule :
- respects_policy_at_preemption_point arr_seq sched ->
+ respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job) ->
EDF_schedule sched.
Proof.
move=> H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.
@@ -94,7 +94,7 @@ Section Equivalence.
definitions are indeed equivalent, which we note with the following
corollary. *)
Corollary EDF_schedule_equiv:
- EDF_schedule sched <-> respects_policy_at_preemption_point arr_seq sched.
+ EDF_schedule sched <-> respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
Proof.
split.
- by apply EDF_schedule_implies_respects_policy_at_preemption_point.
diff --git a/analysis/facts/priority/edf.v b/analysis/facts/priority/edf.v
index a9d7d2ebb..7de6b8dc2 100644
--- a/analysis/facts/priority/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -84,7 +84,7 @@ Section SequentialEDF.
(** Next, we assume that the schedule respects the policy defined by
the [job_preemptable] function (i.e., jobs have bounded
non-preemptive segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
(** To prove sequentiality, we use lemma
[early_hep_job_is_scheduled]. Clearly, under the EDF priority
diff --git a/analysis/facts/priority/fifo.v b/analysis/facts/priority/fifo.v
index 94941ff1d..9095e6540 100644
--- a/analysis/facts/priority/fifo.v
+++ b/analysis/facts/priority/fifo.v
@@ -32,7 +32,7 @@ Section BasicLemmas.
(** Assume that the schedule respects the FIFO scheduling policy whenever jobs
are preemptable. *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job).
(** We observe that there is no priority inversion in a
FIFO-compliant schedule. *)
diff --git a/analysis/facts/priority/sequential.v b/analysis/facts/priority/sequential.v
index 06bcf3ac4..5c6f8c24e 100644
--- a/analysis/facts/priority/sequential.v
+++ b/analysis/facts/priority/sequential.v
@@ -17,7 +17,7 @@ Section SequentialJLFP.
(** Consider a JLFP-policy that indicates a higher-or-equal priority
relation, and assume that this relation is transitive. *)
- Context `{JLFP_policy Job}.
+ Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_transitive : transitive_priorities.
(** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
@@ -40,7 +40,7 @@ Section SequentialJLFP.
(** Next, we assume that the schedule respects the policy defined by
the [job_preemptable] function (i.e., jobs have bounded
non-preemptive segments)... *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
(** ... and that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
diff --git a/implementation/facts/ideal_uni/prio_aware.v b/implementation/facts/ideal_uni/prio_aware.v
index 2b9b519ad..ab8e493df 100644
--- a/implementation/facts/ideal_uni/prio_aware.v
+++ b/implementation/facts/ideal_uni/prio_aware.v
@@ -30,7 +30,7 @@ Section PrioAwareUniprocessorScheduler.
Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM.
(** ... and reflexive, total, and transitive JLDP priority policy. *)
- Context `{JLDP_policy Job}.
+ Context `{JLDP : JLDP_policy Job}.
Hypothesis H_reflexive_priorities: reflexive_priorities.
Hypothesis H_total: total_priorities.
Hypothesis H_transitive: transitive_priorities.
@@ -118,7 +118,7 @@ Section PrioAwareUniprocessorScheduler.
(** From the preceding facts, we conclude that [uni_schedule arr_seq]
respects the priority policy at preemption times. *)
Theorem schedule_respects_policy :
- respects_policy_at_preemption_point arr_seq schedule.
+ respects_JLDP_policy_at_preemption_point arr_seq schedule JLDP.
Proof.
move=> j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.
case: (boolP (scheduled_at (uni_schedule arr_seq) j1 t)) => [SCHED_j1|NOT_SCHED_j1].
diff --git a/model/schedule/priority_driven.v b/model/schedule/priority_driven.v
index cb8d74027..e78273ab3 100644
--- a/model/schedule/priority_driven.v
+++ b/model/schedule/priority_driven.v
@@ -38,13 +38,28 @@ Section Priority.
(** ...and an ideal uniprocessor schedule of these jobs, *)
Variable sched : schedule (ideal.processor_state Job).
- (** we say that a JLDP policy ...*)
- Context `{JLDP_policy Job}.
-
- (** ...is respected by the schedule iff, at every preemption point, the
- priority of the scheduled job is higher than or equal to the priority of
- any backlogged job. *)
- Definition respects_policy_at_preemption_point :=
+ (** we say that a priority policy is respected by the schedule iff,
+ at every preemption point, the priority of the scheduled job is
+ higher than or equal to the priority of any backlogged job.
+ We define three separate notions of priority policy compliance
+ based on the three types of scheduling policies : [JLDP]... *)
+ Definition respects_JLDP_policy_at_preemption_point (policy: JLDP_policy Job) :=
+ forall j j_hp t,
+ arrives_in arr_seq j ->
+ preemption_time sched t ->
+ backlogged sched j t ->
+ scheduled_at sched j_hp t ->
+ hep_job_at t j_hp j.
+ (** ... [JLFP], and... *)
+ Definition respects_JLFP_policy_at_preemption_point (policy: JLFP_policy Job) :=
+ forall j j_hp t,
+ arrives_in arr_seq j ->
+ preemption_time sched t ->
+ backlogged sched j t ->
+ scheduled_at sched j_hp t ->
+ hep_job_at t j_hp j.
+ (** [FP]. *)
+ Definition respects_FP_policy_at_preemption_point (policy: FP_policy Task) :=
forall j j_hp t,
arrives_in arr_seq j ->
preemption_time sched t ->
diff --git a/results/edf/optimality.v b/results/edf/optimality.v
index 4450724d0..79abd84ee 100644
--- a/results/edf/optimality.v
+++ b/results/edf/optimality.v
@@ -111,7 +111,7 @@ Section Optimality.
valid_schedule priority_compliant_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq priority_compliant_sched /\
work_conserving arr_seq priority_compliant_sched /\
- respects_policy_at_preemption_point arr_seq priority_compliant_sched.
+ respects_JLFP_policy_at_preemption_point arr_seq priority_compliant_sched (EDF Job).
Proof.
move /EDF_WC_optimality => [edf_sched [[ARR READY] [DL_MET [WC EDF]]]].
exists edf_sched.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 123cb771c..648ddd82c 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -72,7 +72,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** ... and the schedule respects the policy defined by the [job_preemptable]
function (i.e., jobs have bounded non-preemptive segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched EDF.
(** Consider an arbitrary task set ts, ... *)
Variable ts : list Task.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 1c1bc8101..341a6543b 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -81,7 +81,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
(** ... and the schedule respects the policy defined by the
job_preemptable function (i.e., jobs have bounded non-preemptive
segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
(** ** Total Workload and Length of Busy Interval *)
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index ff4d924cc..e7277894c 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -71,7 +71,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
(** ... and the schedule respects the policy defined by the
job_preemptable function (i.e., jobs have bounded nonpreemptive
segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
(** ** Total Workload and Length of Busy Interval *)
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index aa060227e..dd9f0c512 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -71,7 +71,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
(** ... and the schedule respects the policy defined by the
[job_preemptable] function (i.e., jobs have bounded non-preemptive
segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
(** ** Total Workload and Length of Busy Interval *)
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 2004a0e5d..90c0c2ddc 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -82,7 +82,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
(** ... and the schedule respects the policy defined by the
[job_preemptable] function (i.e., jobs have bounded non-preemptive
segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
(** ** Total Workload and Length of Busy Interval *)
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 78b8099a2..61bb18bdf 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -89,7 +89,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
Hypothesis H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold arr_seq tsk.
(** We also assume that the schedule respects the policy defined by the preemption model. *)
- Hypothesis H_respects_policy_at_preemption_point : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job).
(** We introduce [rbf] as an abbreviation of the task request bound function,
which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a given task [T]. *)
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 1a7068ab5..02db6d99f 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -36,7 +36,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority
relation, and assume that the relation is reflexive and
transitive. *)
- Context `{FP_policy Task}.
+ Context {FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -69,7 +69,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** ... and the schedule respects the policy defined by the [job_preemptable]
function (i.e., jobs have bounded non-preemptive segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
(** Assume we have sequential tasks, i.e, jobs from the
same task execute in the order of their arrival. *)
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 73a987d3e..db79391cf 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -78,7 +78,7 @@ Section RTAforFloatingModelwithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Context `{FP_policy Task}.
+ Context {FP :FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -87,7 +87,7 @@ Section RTAforFloatingModelwithArrivalCurves.
(** ... and the schedule respects the policy defined by the [job_preemptable]
function (i.e., jobs have bounded non-preemptive segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
(** ** Total Workload and Length of Busy Interval *)
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index e3d35cf10..3baf51c5b 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -70,7 +70,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Context `{FP_policy Task}.
+ Context {FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -80,7 +80,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(** ... and the schedule respects the policy defined by the
[job_preemptable] function (i.e., jobs have bounded nonpreemptive
segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
(** ** Total Workload and Length of Busy Interval *)
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 31574f38f..8c8226866 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -70,7 +70,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Context `{FP_policy Task}.
+ Context {FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -79,7 +79,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
(** ... and the schedule respects the policy defined by the [job_preemptable]
function (i.e., jobs have bounded non-preemptive segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
(** ** Total Workload and Length of Busy Interval *)
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 4d39b8f32..c6a35f50f 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -78,7 +78,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Context `{FP_policy Task}.
+ Context {FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -87,7 +87,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
(** ... and the schedule respects the policy defined by the [job_preemptable]
function (i.e., jobs have bounded non-preemptive segments). *)
- Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+ Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
(** ** Total Workload and Length of Busy Interval *)
--
GitLab