Commit 9271931f authored by Björn Brandenburg's avatar Björn Brandenburg

move restructured Prosa to top level

The main restructuring thrust is nearing completion, so let's get rid
of the `restructuring` namespace.
parent 4c91dcff
......@@ -143,8 +143,8 @@ proof-state:
dependencies:
- 1.9.0-coq-8.10
script:
- find restructuring util -iname *.v | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
- scripts/intersperse-proof-state.py `find restructuring util -iname *.v`
- find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
- scripts/intersperse-proof-state.py `find . -iname *.v ! -path './classic/*'`
- cd with-proof-state/
- ln -s ../scripts/
- ln -s ../_CoqProject
......
......@@ -16,12 +16,21 @@ Please see the [list of publications](http://prosa.mpi-sws.org/documentation.htm
## Directory and Module Structure
The directory and module structure is currently undergoing a fundamental reorganization.
The directory and module structure is organized as follows. First, the main parts, of which there are currently four.
- [behavior/](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module.
- [model/](model/): The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected "pick and choose" whatever definitions and assumptions are appropriate.
- [analysis/](analysis/): The `analysis` namespace collects all definitions and proof libraries needed to establish **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
- [results/](results/): The `results` namespace contains all **high-level analysis results**.
In future work, there will also (again) be an `implementation` or `examples` namespace in which important high-level results are instantiated (i.e., applied) in an assumption-free environment for concrete job and task types to establish the absence of any contradiction in assumptions.
Furthermore, there are a couple of additional folders and namespaces.
- [classic/](classic/): This module contains the "classic" version of Prosa as first presented at ECRTS'16.
All results published prior to 2020 build on this "classic" version of Prosa.
- [util/](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
- [restructuring/](restructuring/): The new, refactored version of Prosa. Currently still under heavy development. This part of Prosa will soon move out of the `restructuring` namespace.
- [scripts/](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
## Dependencies
......
Require Export rt.restructuring.analysis.concepts.schedulability.
Require Export rt.restructuring.analysis.abstract.search_space.
Require Export rt.restructuring.analysis.abstract.run_to_completion.
Require Export rt.analysis.concepts.schedulability.
Require Export rt.analysis.abstract.search_space.
Require Export rt.analysis.abstract.run_to_completion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export rt.restructuring.analysis.definitions.task_schedule.
Require Export rt.restructuring.analysis.facts.rbf.
Require Export rt.restructuring.analysis.facts.behavior.task_arrivals.
Require Export rt.restructuring.analysis.abstract.abstract_rta.
Require Export rt.analysis.definitions.task_schedule.
Require Export rt.analysis.facts.rbf.
Require Export rt.analysis.facts.behavior.task_arrivals.
Require Export rt.analysis.abstract.abstract_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export rt.restructuring.model.task.concept.
Require Export rt.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** * Definitions for Abstract Response-Time Analysis *)
(** In this module, we propose a set of definitions for the general framework for response-time analysis (RTA)
......
Require Export rt.restructuring.analysis.concepts.priority_inversion.
Require Export rt.restructuring.analysis.abstract.abstract_seq_rta.
Require Export rt.analysis.concepts.priority_inversion.
Require Export rt.analysis.abstract.abstract_seq_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** In this file we consider an ideal uni-processor ... *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** ... and classic model of readiness without jitter and no
self-suspensions, where pending jobs are always ready. *)
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.model.readiness.basic.
(** * JLFP instantiation of Interference and Interfering Workload for ideal uni-processor. *)
(** In this module we instantiate functions Interference and Interfering Workload
......
Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export rt.restructuring.analysis.abstract.definitions.
Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export rt.analysis.abstract.definitions.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Import rt.util.epsilon.
Require Import rt.util.tactics.
Require Import rt.restructuring.model.task.concept.
Require Import rt.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** * Reduction of the search space for Abstract RTA *)
......
Require Export rt.restructuring.model.priority.classes.
Require Export rt.restructuring.analysis.facts.behavior.completion.
Require Export rt.model.priority.classes.
Require Export rt.analysis.facts.behavior.completion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** * Busy Interval for JLFP-models *)
(** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
......
Require Export rt.restructuring.analysis.concepts.busy_interval.
Require Export rt.analysis.concepts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.model.task.arrival.curves.
Require Export rt.restructuring.model.priority.classes.
Require Export rt.model.task.arrival.curves.
Require Export rt.model.priority.classes.
(** The following definitions assume ideal uni-processor schedules. This
restriction exists for historic reasons; the defined concepts could be
generalized in future work. *)
Require Import rt.restructuring.analysis.facts.behavior.ideal_schedule.
Require Import rt.analysis.facts.behavior.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export rt.restructuring.analysis.facts.behavior.completion.
Require Import rt.restructuring.model.task.absolute_deadline.
Require Export rt.analysis.facts.behavior.completion.
Require Import rt.model.task.absolute_deadline.
Section Task.
Context {Task : TaskType}.
......
Require Export rt.restructuring.model.priority.classes.
Require Export rt.model.priority.classes.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** * No Carry-In *)
(** In this module we define the notion of no carry-in time for uni-processor schedulers. *)
......
Require Export rt.restructuring.behavior.all.
Require Export rt.behavior.all.
From mathcomp Require Export eqtype ssrnat.
(** In this section, we introduce properties of a job. *)
......
Require Export rt.restructuring.analysis.facts.behavior.service.
Require Export rt.analysis.facts.behavior.service.
(** * Job Progress (or Lack Thereof) *)
......
Require Export rt.restructuring.model.task.concept.
Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
Require Export rt.model.task.concept.
Require Export rt.analysis.facts.behavior.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export rt.analysis.facts.behavior.service.
Require Export rt.analysis.facts.behavior.service_of_jobs.
Require Export rt.analysis.facts.behavior.completion.
Require Export rt.analysis.facts.behavior.ideal_schedule.
Require Export rt.analysis.facts.behavior.sequential.
Require Export rt.analysis.facts.behavior.arrivals.
Require Export rt.analysis.facts.behavior.deadlines.
Require Export rt.analysis.facts.behavior.workload.
Require Export rt.restructuring.behavior.all.
Require Export rt.behavior.all.
Require Export rt.util.all.
(** In this section, we relate job readiness to [has_arrived]. *)
......
Require Export rt.restructuring.analysis.facts.behavior.service.
Require Export rt.restructuring.analysis.facts.behavior.arrivals.
Require Export rt.analysis.facts.behavior.service.
Require Export rt.analysis.facts.behavior.arrivals.
(** In this file, we establish basic facts about job completions. *)
......
Require Export rt.restructuring.analysis.facts.behavior.completion.
Require Export rt.analysis.facts.behavior.completion.
(** In this file, we observe basic properties of the behavioral job
model w.r.t. deadlines. *)
......
From mathcomp Require Import all_ssreflect.
Require Export rt.util.all.
Require Export rt.restructuring.model.processor.platform_properties.
Require Export rt.restructuring.analysis.facts.behavior.service.
Require Export rt.model.processor.platform_properties.
Require Export rt.analysis.facts.behavior.service.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances. *)
......
Require Export rt.restructuring.model.task.sequentiality.
Require Export rt.model.task.sequentiality.
Section ExecutionOrder.
(** Consider any type of job associated with any type of tasks... *)
......
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.model.processor.platform_properties.
Require Export rt.behavior.all.
Require Export rt.model.processor.platform_properties.
From mathcomp Require Import ssrnat ssrbool fintype.
......
Require Export rt.restructuring.model.aggregate.workload.
Require Export rt.restructuring.model.aggregate.service_of_jobs.
Require Export rt.restructuring.analysis.facts.behavior.completion.
Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
Require Import rt.restructuring.model.processor.ideal.
Require Export rt.model.aggregate.workload.
Require Export rt.model.aggregate.service_of_jobs.
Require Export rt.analysis.facts.behavior.completion.
Require Export rt.analysis.facts.behavior.ideal_schedule.
Require Import rt.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.model.task.arrivals.
Require Export rt.model.task.arrivals.
(** In this file we provide basic properties related to tasks on arrival sequences. *)
Section TaskArrivals.
......
Require Export rt.restructuring.model.aggregate.workload.
Require Export rt.restructuring.analysis.facts.behavior.arrivals.
Require Export rt.model.aggregate.workload.
Require Export rt.analysis.facts.behavior.arrivals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.analysis.concepts.priority_inversion.
Require Export rt.restructuring.analysis.facts.behavior.all.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.model.schedule.work_conserving.
Require Export rt.analysis.concepts.priority_inversion.
Require Export rt.analysis.facts.behavior.all.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.model.readiness.basic.
(** * Existence of Busy Interval for JLFP-models *)
(** In this module we derive a sufficient condition for existence of
......
Require Export rt.restructuring.analysis.definitions.carry_in.
Require Export rt.restructuring.analysis.facts.busy_interval.
Require Export rt.analysis.definitions.carry_in.
Require Export rt.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.model.readiness.basic.
(** * Existence of No Carry-In Instant *)
......
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.model.task.absolute_deadline.
Require Import rt.model.priority.edf.
Require Import rt.model.task.absolute_deadline.
(** In this section, we prove a few properties about EDF policy. *)
Section PropertiesOfEDF.
......
Require Export rt.restructuring.analysis.facts.behavior.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.analysis.facts.behavior.all.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.model.schedule.limited_preemptive.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.model.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of predicate
......
Require Export rt.restructuring.analysis.facts.behavior.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.schedule.nonpreemptive.
Require Export rt.analysis.facts.behavior.all.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
Require Import rt.model.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.fully_preemptive.
Require Export rt.model.task.preemption.parameters.
Require Import rt.model.preemption.fully_preemptive.
(** * Preemptions in Fully Preemptive Model *)
(** In this section, we prove that instantiation of predicate
......
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Export rt.restructuring.analysis.facts.preemption.task.floating.
Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.model.preemption.limited_preemptive.
Require Import rt.model.task.preemption.floating_nonpreemptive.
Require Export rt.analysis.facts.preemption.task.floating.
Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
......
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.analysis.facts.behavior.all.
Require Export rt.restructuring.model.task.preemption.parameters.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.analysis.facts.behavior.all.
Require Export rt.model.task.preemption.parameters.
(** * Run-to-Completion Threshold *)
(** In this section, we provide a few basic properties
......
Require Export rt.restructuring.analysis.facts.preemption.task.limited.
Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export rt.analysis.facts.preemption.task.limited.
Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.model.preemption.limited_preemptive.
Require Import rt.model.task.preemption.limited_preemptive.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
......
Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
Require Export rt.analysis.facts.preemption.job.nonpreemptive.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Import rt.model.preemption.fully_nonpreemptive.
Require Import rt.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Import rt.restructuring.model.preemption.fully_preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
Require Import rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.model.preemption.fully_preemptive.
Require Import rt.model.task.preemption.fully_preemptive.
Require Import rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
......
Require Export rt.restructuring.analysis.facts.preemption.job.limited.
Require Export rt.analysis.facts.preemption.job.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Import rt.model.preemption.limited_preemptive.
Require Import rt.model.task.preemption.floating_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.analysis.facts.preemption.job.limited.
Require Export rt.analysis.facts.preemption.job.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.model.preemption.limited_preemptive.
Require Import rt.model.task.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of functions
......
Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
Require Export rt.analysis.facts.preemption.job.nonpreemptive.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Import rt.model.preemption.fully_nonpreemptive.
Require Import rt.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.analysis.facts.preemption.job.preemptive.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.analysis.facts.preemption.job.preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
Require Import rt.model.task.preemption.fully_preemptive.
(** * Platform for Fully Preemptive Model *)
(** In this section, we prove that instantiation of functions
......
Require Export rt.restructuring.model.task.preemption.parameters.
Require Export rt.restructuring.model.schedule.priority_driven.
Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.analysis.concepts.busy_interval.
Require Export rt.restructuring.analysis.facts.busy_interval.
Require Export rt.model.task.preemption.parameters.
Require Export rt.model.schedule.priority_driven.
Require Export rt.analysis.facts.behavior.ideal_schedule.
Require Export rt.model.schedule.work_conserving.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.analysis.concepts.busy_interval.
Require Export rt.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** 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. *)
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.model.readiness.basic.
(** In preparation of the derivation of the priority inversion bound, we
establish two basic facts on preemption times. *)
......
Require Export rt.restructuring.analysis.facts.behavior.workload.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.analysis.concepts.request_bound_function.
Require Export rt.analysis.facts.behavior.workload.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.analysis.concepts.request_bound_function.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Import rt.restructuring.analysis.facts.behavior.completion.
Require Import rt.analysis.facts.behavior.completion.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.model.readiness.basic.
Section LiuAndLaylandReadiness.
(** Consider any kind of jobs... *)
......
Require Export rt.restructuring.model.schedule.tdma.
Require Export rt.model.schedule.tdma.
Require Import rt.util.all.
From mathcomp Require Import div.
......
From mathcomp Require Import ssrnat ssrbool fintype.
Require Export rt.restructuring.model.schedule.edf.
Require Export rt.restructuring.analysis.concepts.schedulability.
Require Export rt.restructuring.analysis.transform.edf_trans.
Require Export rt.restructuring.analysis.facts.transform.swaps.
Require Export rt.restructuring.analysis.facts.readiness.basic.
Require Export rt.model.schedule.edf.
Require Export rt.analysis.concepts.schedulability.
Require Export rt.analysis.transform.edf_trans.
Require Export rt.analysis.facts.transform.swaps.
Require Export rt.analysis.facts.readiness.basic.
(** This file contains the main argument of the EDF optimality proof,
starting with an analysis of the individual functions that drive
......@@ -12,9 +12,9 @@ Require Export rt.restructuring.analysis.facts.readiness.basic.
the obtained EDF schedule. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
Require Import rt.model.readiness.basic.
(** We start by analyzing the helper function [find_swap_candidate],
which is a problem-specific wrapper around [search_arg]. *)
......
Require Export rt.restructuring.analysis.transform.swap.
Require Export rt.restructuring.analysis.facts.behavior.completion.
Require Export rt.analysis.transform.swap.
Require Export rt.analysis.facts.behavior.completion.
(** In this file, we make a few simple observations about schedules with
replacements. *)
......
Require Export rt.restructuring.analysis.facts.transform.replace_at.
Require Export rt.restructuring.analysis.facts.behavior.deadlines.
Require Export rt.analysis.facts.transform.replace_at.
Require Export rt.analysis.facts.behavior.deadlines.
(** In this file, we establish invariants about schedules in which two
allocations have been swapped, as for instance it is done in the
......
Require Export rt.restructuring.analysis.transform.prefix.
Require Export rt.restructuring.analysis.transform.swap.
Require Export rt.analysis.transform.prefix.
Require Export rt.analysis.transform.swap.
(** In this file we define the EDF transformation of a schedule, which turns a
(finite prefix of a) schedule into an EDF schedule. This operation is at
......
From mathcomp Require Import ssrnat ssrbool fintype.
Require Export rt.restructuring.analysis.facts.behavior.all.
Require Export rt.analysis.facts.behavior.all.
(** This file provides an operation that transforms a finite prefix of
a given schedule by applying a point-wise transformation to each
......
Require Export rt.restructuring.behavior.all.
Require Export rt.behavior.all.
(** This file defines simple allocation substitutions and a swapping operation
as used for instance in the classic EDF optimality proof. *)
......
Require Export rt.behavior.time.
Require Export rt.behavior.job.
Require Export rt.behavior.arrival_sequence.
Require Export rt.behavior.schedule.
Require Export rt.behavior.service.
Require Export rt.behavior.ready.
From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
Require Export rt.restructuring.behavior.job.
Require Export rt.behavior.job.
Require Export <