Commit 0d8c78ae authored by Björn Brandenburg's avatar Björn Brandenburg

do the big rt->prosa move

Move everything into the new namespace starting with 'prosa' rather
than the bland 'rt'.
parent 9271931f
Pipeline #22292 passed with stages
in 5 minutes and 30 seconds
......@@ -143,7 +143,7 @@ proof-state:
dependencies:
- 1.9.0-coq-8.10
script:
- find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
- find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . prosa -w -notation-overriden,-parsing' --timeout 20
- scripts/intersperse-proof-state.py `find . -iname *.v ! -path './classic/*'`
- cd with-proof-state/
- ln -s ../scripts/
......
-R . rt -arg "-w -notation-overriden,-parsing"
-R . prosa -arg "-w -notation-overriden,-parsing"
Require Export rt.analysis.concepts.schedulability.
Require Export rt.analysis.abstract.search_space.
Require Export rt.analysis.abstract.run_to_completion.
Require Export prosa.analysis.concepts.schedulability.
Require Export prosa.analysis.abstract.search_space.
Require Export prosa.analysis.abstract.run_to_completion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
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.
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.rbf.
Require Export prosa.analysis.facts.behavior.task_arrivals.
Require Export prosa.analysis.abstract.abstract_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export rt.model.task.concept.
Require Export prosa.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.model.processor.ideal.
Require Import prosa.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.analysis.concepts.priority_inversion.
Require Export rt.analysis.abstract.abstract_seq_rta.
Require Export prosa.analysis.concepts.priority_inversion.
Require Export prosa.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.model.processor.ideal.
Require Import prosa.model.processor.ideal.
(** ... and classic model of readiness without jitter and no
self-suspensions, where pending jobs are always ready. *)
Require Import rt.model.readiness.basic.
Require Import prosa.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.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export rt.analysis.abstract.definitions.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.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.model.task.concept.
Require Import prosa.util.epsilon.
Require Import prosa.util.tactics.
Require Import prosa.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.model.priority.classes.
Require Export rt.analysis.facts.behavior.completion.
Require Export prosa.model.priority.classes.
Require Export prosa.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.model.processor.ideal.
Require Import prosa.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.analysis.concepts.busy_interval.
Require Export prosa.analysis.concepts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export rt.model.task.arrival.curves.
Require Export rt.model.priority.classes.
Require Export prosa.model.task.arrival.curves.
Require Export prosa.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.analysis.facts.behavior.ideal_schedule.
Require Import prosa.analysis.facts.behavior.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Export rt.analysis.facts.behavior.completion.
Require Import rt.model.task.absolute_deadline.
Require Export prosa.analysis.facts.behavior.completion.
Require Import prosa.model.task.absolute_deadline.
Section Task.
Context {Task : TaskType}.
......
Require Export rt.model.priority.classes.
Require Export prosa.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.model.processor.ideal.
Require Import prosa.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.behavior.all.
Require Export prosa.behavior.all.
From mathcomp Require Export eqtype ssrnat.
(** In this section, we introduce properties of a job. *)
......
Require Export rt.analysis.facts.behavior.service.
Require Export prosa.analysis.facts.behavior.service.
(** * Job Progress (or Lack Thereof) *)
......
Require Export rt.model.task.concept.
Require Export rt.analysis.facts.behavior.ideal_schedule.
Require Export prosa.model.task.concept.
Require Export prosa.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 prosa.analysis.facts.behavior.service.
Require Export prosa.analysis.facts.behavior.service_of_jobs.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.behavior.ideal_schedule.
Require Export prosa.analysis.facts.behavior.sequential.
Require Export prosa.analysis.facts.behavior.arrivals.
Require Export prosa.analysis.facts.behavior.deadlines.
Require Export prosa.analysis.facts.behavior.workload.
Require Export rt.behavior.all.
Require Export rt.util.all.
Require Export prosa.behavior.all.
Require Export prosa.util.all.
(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.
......
Require Export rt.analysis.facts.behavior.service.
Require Export rt.analysis.facts.behavior.arrivals.
Require Export prosa.analysis.facts.behavior.service.
Require Export prosa.analysis.facts.behavior.arrivals.
(** In this file, we establish basic facts about job completions. *)
......
Require Export rt.analysis.facts.behavior.completion.
Require Export prosa.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.model.processor.platform_properties.
Require Export rt.analysis.facts.behavior.service.
Require Export prosa.util.all.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.facts.behavior.service.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.model.processor.ideal.
Require Import prosa.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.model.task.sequentiality.
Require Export prosa.model.task.sequentiality.
Section ExecutionOrder.
(** Consider any type of job associated with any type of tasks... *)
......
Require Export rt.util.all.
Require Export rt.behavior.all.
Require Export rt.model.processor.platform_properties.
Require Export prosa.util.all.
Require Export prosa.behavior.all.
Require Export prosa.model.processor.platform_properties.
From mathcomp Require Import ssrnat ssrbool fintype.
......
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.
Require Export prosa.model.aggregate.workload.
Require Export prosa.model.aggregate.service_of_jobs.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.behavior.ideal_schedule.
Require Import prosa.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export rt.model.task.arrivals.
Require Export prosa.model.task.arrivals.
(** In this file we provide basic properties related to tasks on arrival sequences. *)
Section TaskArrivals.
......
Require Export rt.model.aggregate.workload.
Require Export rt.analysis.facts.behavior.arrivals.
Require Export prosa.model.aggregate.workload.
Require Export prosa.analysis.facts.behavior.arrivals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
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.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.concepts.priority_inversion.
Require Export prosa.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.model.processor.ideal.
Require Import prosa.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.model.readiness.basic.
Require Import prosa.model.readiness.basic.
(** * Existence of Busy Interval for JLFP-models *)
(** In this module we derive a sufficient condition for existence of
......
Require Export rt.analysis.definitions.carry_in.
Require Export rt.analysis.facts.busy_interval.
Require Export prosa.analysis.definitions.carry_in.
Require Export prosa.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.model.processor.ideal.
Require Import prosa.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.model.readiness.basic.
Require Import prosa.model.readiness.basic.
(** * Existence of No Carry-In Instant *)
......
Require Import rt.model.priority.edf.
Require Import rt.model.task.absolute_deadline.
Require Import prosa.model.priority.edf.
Require Import prosa.model.task.absolute_deadline.
(** In this section, we prove a few properties about EDF policy. *)
Section PropertiesOfEDF.
......
Require Export rt.analysis.facts.behavior.all.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.model.schedule.limited_preemptive.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.limited_preemptive.
Require Import rt.model.preemption.limited_preemptive.
Require Import prosa.model.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of predicate
......
Require Export rt.analysis.facts.behavior.all.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.model.schedule.nonpreemptive.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.nonpreemptive.
Require Import rt.model.preemption.fully_nonpreemptive.
Require Import prosa.model.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.model.task.preemption.parameters.
Require Import rt.model.preemption.fully_preemptive.
Require Export prosa.model.task.preemption.parameters.
Require Import prosa.model.preemption.fully_preemptive.
(** * Preemptions in Fully Preemptive Model *)
(** In this section, we prove that instantiation of predicate
......
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.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
Require Export prosa.analysis.facts.preemption.task.floating.
Require Export prosa.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.analysis.definitions.job_properties.
Require Export rt.analysis.facts.behavior.all.
Require Export rt.model.task.preemption.parameters.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.model.task.preemption.parameters.
(** * Run-to-Completion Threshold *)
(** In this section, we provide a few basic properties
......
Require Export rt.analysis.facts.preemption.task.limited.
Require Export rt.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.analysis.facts.preemption.task.limited.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.model.preemption.limited_preemptive.
Require Import rt.model.task.preemption.limited_preemptive.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.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.analysis.facts.preemption.job.nonpreemptive.
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
Require Import rt.model.preemption.fully_nonpreemptive.
Require Import rt.model.task.preemption.fully_nonpreemptive.
Require Import prosa.model.preemption.fully_nonpreemptive.
Require Import prosa.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
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.
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.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
......
Require Export rt.analysis.facts.preemption.job.limited.
Require Export prosa.analysis.facts.preemption.job.limited.
Require Import rt.model.preemption.limited_preemptive.
Require Import rt.model.task.preemption.floating_nonpreemptive.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.analysis.facts.preemption.job.limited.
Require Export prosa.analysis.facts.preemption.job.limited.
Require Import rt.model.preemption.limited_preemptive.
Require Import rt.model.task.preemption.limited_preemptive.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of functions
......
Require Export rt.analysis.facts.preemption.job.nonpreemptive.
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
Require Import rt.model.preemption.fully_nonpreemptive.
Require Import rt.model.task.preemption.fully_nonpreemptive.
Require Import prosa.model.preemption.fully_nonpreemptive.
Require Import prosa.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Export rt.analysis.definitions.job_properties.
Require Export rt.analysis.facts.preemption.job.preemptive.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.preemption.job.preemptive.
Require Import rt.model.task.preemption.fully_preemptive.
Require Import prosa.model.task.preemption.fully_preemptive.
(** * Platform for Fully Preemptive Model *)
(** In this section, we prove that instantiation of functions
......
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.
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.behavior.ideal_schedule.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.concepts.busy_interval.
Require Export prosa.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.model.processor.ideal.
Require Import prosa.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.model.readiness.basic.
Require Import prosa.model.readiness.basic.
(** In preparation of the derivation of the priority inversion bound, we
establish two basic facts on preemption times. *)
......@@ -83,7 +83,7 @@ End PreemptionTimes.
(** * Priority inversion is bounded *)
(** In this module we prove that any priority inversion that occurs in the model with bounded
nonpreemptive segments defined in module rt.model.schedule.uni.limited.platform.definitions
nonpreemptive segments defined in module prosa.model.schedule.uni.limited.platform.definitions
is bounded. *)
Section PriorityInversionIsBounded.
......
Require Export rt.analysis.facts.behavior.workload.
Require Export rt.analysis.definitions.job_properties.
Require Export rt.analysis.concepts.request_bound_function.
Require Export prosa.analysis.facts.behavior.workload.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.concepts.request_bound_function.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
......
Require Import rt.analysis.facts.behavior.completion.
Require Import prosa.analysis.facts.behavior.completion.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.model.readiness.basic.
Require Import prosa.model.readiness.basic.
Section LiuAndLaylandReadiness.
(** Consider any kind of jobs... *)
......
Require Export rt.model.schedule.tdma.
Require Import rt.util.all.
Require Export prosa.model.schedule.tdma.
Require Import prosa.util.all.
From mathcomp Require Import div.
(** In this section, we define the properties of TDMA and prove some basic lemmas. *)
......
From mathcomp Require Import ssrnat ssrbool fintype.
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.
Require Export prosa.model.schedule.edf.
Require Export prosa.analysis.concepts.schedulability.
Require Export prosa.analysis.transform.edf_trans.
Require Export prosa.analysis.facts.transform.swaps.