From bbefcd16d730b1f8befa43421568bc903123e05d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 29 Oct 2019 18:07:00 +0100
Subject: [PATCH] make a few cosmetic tweaks in the EDF optimality proof
As discussed in #57.
---
restructuring/analysis/edf/optimality.v | 12 ++++++++++--
restructuring/analysis/transform/edf_trans.v | 2 +-
restructuring/analysis/transform/facts/edf_opt.v | 4 ++--
3 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/restructuring/analysis/edf/optimality.v b/restructuring/analysis/edf/optimality.v
index bed07c60c..5f3c8e8a3 100644
--- a/restructuring/analysis/edf/optimality.v
+++ b/restructuring/analysis/edf/optimality.v
@@ -6,6 +6,12 @@ From rt.restructuring.analysis Require Import schedulability transform.facts.edf
(assuming an ideal uniprocessor), then there is also an EDF
schedule in which all deadlines are met. *)
+(** The following results assume ideal uniprocessor schedules... *)
+From rt.restructuring.model.processor Require ideal.
+(** ... and the basic (i.e., Liu & Layland) readiness model under which any
+ pending job is ready. *)
+From rt.restructuring.model.readiness Require basic.
+
Section Optimality.
(** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
@@ -40,8 +46,10 @@ Section Optimality.
End Optimality.
-(** We further state a weaker notion of the above optimality claim
- that avoids a dependency on a given arrival sequence. *)
+(** We further state a weaker notion of the above optimality claim that avoids
+ a dependency on a given arrival sequence. Specifically, it establishes
+ that, given a reference schedule without deadline misses, there exists an
+ EDF schedule of the same jobs in which no deadlines are missed. *)
Section WeakOptimality.
(** For any given type of jobs,... *)
diff --git a/restructuring/analysis/transform/edf_trans.v b/restructuring/analysis/transform/edf_trans.v
index 788533745..595bc8078 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/restructuring/analysis/transform/edf_trans.v
@@ -45,7 +45,7 @@ Section EDFTransformation.
t1. *)
Definition make_edf_at (sched: SchedType) (t1: instant): SchedType :=
match sched t1 with
- | None => sched (** leave idle instants alone *)
+ | None => sched (* leave idle instants alone *)
| Some j =>
let
t2 := find_swap_candidate sched t1 j
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/transform/facts/edf_opt.v
index 528467d90..0ced86adf 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/transform/facts/edf_opt.v
@@ -12,9 +12,9 @@ From rt.util Require Import tactics nat.
schedule. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
-From rt.restructuring.model.processor Require Export ideal.
+From rt.restructuring.model.processor Require Import ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-From rt.restructuring.model.readiness Require Export basic.
+From rt.restructuring.model.readiness Require Import basic.
(** We start by analyzing the helper function [find_swap_candidate],
which is a problem-specific wrapper around [search_arg]. *)
--
GitLab