Commit 1e45ddeb authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

disambiguate Require commands in rt.restructuring

This fixes all warnings about ambiguous module names and resolves #49.

It also highlights that we still need to cut down on superfluous
Require Import commands in recently ported files.
parent 4e04399a
From rt.util Require Export all.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Export all.
From rt.restructuring Require Export model.job model.task.
From rt.restructuring.model.schedule Require Export work_conserving priority_based.priorities.
From rt.restructuring.analysis.definitions Require Export no_carry_in busy_interval priority_inversion.
From rt.restructuring.analysis.facts Require Export busy_interval_exists.
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.model.job.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.model.schedule.priority_based.priorities.
Require Export rt.restructuring.analysis.definitions.no_carry_in.
Require Export rt.restructuring.analysis.definitions.busy_interval.
Require Export rt.restructuring.analysis.definitions.priority_inversion.
Require Export rt.restructuring.analysis.facts.busy_interval_exists.
(** Throughout the file we assume for the classic Liu & Layland model
of readiness without jitter and no self-suspensions, where prending
jobs are always ready. *)
From rt.restructuring.model Require Import readiness.basic.
Require Import rt.restructuring.model.readiness.basic.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
From rt.util Require Import all.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model.preemption Require Import
valid_model preemption_time job.parameters task.parameters.
From rt.restructuring.model.schedule Require Import priority_based.preemption_aware.
From rt.restructuring.analysis.definitions Require Export no_carry_in busy_interval priority_inversion.
From rt.restructuring.analysis.facts Require Export busy_interval_exists no_carry_in_exists.
Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.preemption_time.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
Require Export rt.restructuring.analysis.definitions.no_carry_in.
Require Export rt.restructuring.analysis.definitions.busy_interval.
Require Export rt.restructuring.analysis.definitions.priority_inversion.
Require Export rt.restructuring.analysis.facts.busy_interval_exists.
Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout the file we assume for the classic Liu & Layland model
of readiness without jitter and no self-suspensions, where
pending jobs are always ready. *)
From rt.restructuring.model Require Import readiness.basic.
Require Import rt.restructuring.model.readiness.basic.
(** * Priority inversion is bounded *)
(** In this module we prove that any priority inversion that occurs in the model with bounded
......
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.model Require Import preemption.floating.
From rt.restructuring.model.schedule Require Import
work_conserving priority_based.priorities priority_based.preemption_aware.
From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
From rt.restructuring.analysis.fixed_priority.rta Require Import nonpr_reg.response_time_bound.
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.floating.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.schedule.priority_based.priorities.
Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.model Require Import preemption.limited.
From rt.restructuring.model.schedule Require Import
work_conserving priority_based.priorities priority_based.preemption_aware.
From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
From rt.restructuring.analysis.fixed_priority.rta Require Import nonpr_reg.response_time_bound.
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.limited.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.schedule.priority_based.priorities.
Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.model.schedule Require Import
work_conserving priority_based.priorities priority_based.preemption_aware.
From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
From rt.restructuring.analysis.fixed_priority.rta Require Import nonpr_reg.response_time_bound.
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.schedule.priority_based.priorities.
Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
(** Assume we have a fully non-preemptive model. *)
From rt.restructuring.model Require Import preemption.nonpreemptive.
Require Import rt.restructuring.model.preemption.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.model.schedule Require Import
work_conserving priority_based.priorities priority_based.preemption_aware.
From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
From rt.restructuring.analysis.fixed_priority.rta Require Import nonpr_reg.response_time_bound.
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.schedule.priority_based.priorities.
Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
(** Assume we have a fully preemptive model. *)
From rt.restructuring.model Require Import preemption.preemptive.
Require Import rt.restructuring.model.preemption.preemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.model.preemption Require Import valid_model
job.parameters task.parameters rtc_threshold.valid_rtct.
From rt.restructuring.model.schedule Require Import
work_conserving priority_based.priorities priority_based.preemption_aware.
From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
From rt.restructuring.analysis.fixed_priority Require Export rta.response_time_bound.
From rt.restructuring.analysis.facts Require Import priority_inversion_is_bounded.
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.schedule.priority_based.priorities.
Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.model.preemption Require Import valid_model
job.parameters task.parameters rtc_threshold.valid_rtct.
From rt.restructuring.model.schedule Require Import
work_conserving priority_based.priorities priority_based.preemption_aware.
From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
From rt.restructuring.analysis Require Export schedulability.
From rt.restructuring.analysis.definitions Require Export busy_interval priority_inversion.
From rt.restructuring.analysis.facts Require Export busy_interval_exists.
From rt.restructuring.analysis.abstract Require Import
core.definitions core.abstract_seq_rta instantiations.ideal_processor.
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.schedule.priority_based.priorities.
Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Export rt.restructuring.analysis.schedulability.
Require Export rt.restructuring.analysis.definitions.busy_interval.
Require Export rt.restructuring.analysis.definitions.priority_inversion.
Require Export rt.restructuring.analysis.facts.busy_interval_exists.
Require Import rt.restructuring.analysis.abstract.core.definitions.
Require Import rt.restructuring.analysis.abstract.core.abstract_seq_rta.
Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export task job_deadline.
From rt.restructuring.analysis.basic_facts Require Export completion.
From rt.util Require Export seqset.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.job_deadline.
Require Export rt.restructuring.analysis.basic_facts.completion.
Require Export rt.util.seqset.
Section Task.
Context {Task : TaskType}.
......
From rt.restructuring.model Require Import task.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import ideal_schedule.
Require Import rt.restructuring.model.task.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
From rt.restructuring.analysis.transform Require Export prefix swap.
From rt.util Require Export search_arg.
Require Export rt.restructuring.analysis.transform.prefix.
Require Export rt.restructuring.analysis.transform.swap.
Require Export rt.util.search_arg.
(** In this file we define the "EDF-ification" of a schedule, the
operation at the core of the EDF optimality proof. *)
......
From mathcomp Require Import ssrnat ssrbool fintype.
From rt.restructuring.analysis Require Export basic_facts.all.
From rt.restructuring.model Require Export schedule.edf.
From rt.restructuring.analysis Require Export schedulability transform.edf_trans transform.facts.swaps.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.model.schedule.edf.
Require Export rt.restructuring.analysis.schedulability.
Require Export rt.restructuring.analysis.transform.edf_trans.
Require Export rt.restructuring.analysis.transform.facts.swaps.
From rt.util Require Import tactics nat.
Require Import rt.util.tactics.
Require Import rt.util.nat.
(** This file contains the main argument of the EDF optimality proof,
starting with an analysis of the individual functions that drive
......@@ -12,9 +15,9 @@ From rt.util Require Import tactics nat.
schedule. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
From rt.restructuring.model.processor Require Import ideal.
Require Import rt.restructuring.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
From rt.restructuring.model.readiness Require Import basic.
Require Import rt.restructuring.model.readiness.basic.
(** We start by analyzing the helper function [find_swap_candidate],
which is a problem-specific wrapper around [search_arg]. *)
......
From rt.restructuring.analysis.transform Require Export swap.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.util Require Import nat.
Require Export rt.restructuring.analysis.transform.swap.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.util.nat.
(** In this file, we make a few simple observations about schedules with
replacements. *)
......
From rt.restructuring.analysis.transform Require Export swap facts.replace_at.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.util Require Import nat.
Require Export rt.restructuring.analysis.transform.swap.
Require Export rt.restructuring.analysis.transform.facts.replace_at.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.util.nat.
(** In this file, we establish invariants about schedules in which two
allocations have been swapped, as for instance it is done in the
......
From mathcomp Require Import ssrnat ssrbool fintype.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis Require Import basic_facts.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
(** This file provides an operation that transforms a finite prefix of
a given schedule by applying a point-wise transformation to each
......
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
(** This file defines simple allocation substitutions and a swapping operation
as used for instance in the classic EDF optimality proof. *)
......
From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
From rt.restructuring.behavior Require Export time job.
From rt.util Require Import notation.
Require Export rt.restructuring.behavior.time.
Require Export rt.restructuring.behavior.job.
Require Import rt.util.notation.
(** This module contains basic definitions and properties of job arrival
sequences. *)
......
From rt.restructuring.behavior Require Export time.
Require Export rt.restructuring.behavior.time.
From mathcomp Require Export eqtype ssrnat.
(** * Notion of a Job Type *)
......
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From rt.restructuring.behavior Require Export service.
Require Export rt.restructuring.behavior.service.
(** * Readiness of a Job *)
......
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
From rt.restructuring.behavior Require Export arrival_sequence.
Require Export rt.restructuring.behavior.arrival_sequence.
(** * Generic Processor State *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment