diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/abstract_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/core/abstract_rta.v
rename to restructuring/analysis/abstract/abstract_rta.v
index 467bf8b6c6fefe143531f25804aa46292e0f7f08..088b34a7f838d397d488c73933854b1b7a63fca0 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/abstract_rta.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.schedulability.
-Require Export rt.restructuring.analysis.abstract.core.reduction_of_search_space.
-Require Export rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
+Require Export rt.restructuring.analysis.concepts.schedulability.
+Require Export rt.restructuring.analysis.abstract.search_space.
+Require Export rt.restructuring.analysis.abstract.run_to_completion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/abstract_seq_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/core/abstract_seq_rta.v
rename to restructuring/analysis/abstract/abstract_seq_rta.v
index 5cef8756827286d0975c9b09aba60e9054799082..41c01f68161f5efa43e2344b9168bd86091cda32 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/abstract_seq_rta.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.task_schedule.
-Require Export rt.restructuring.analysis.arrival.rbf.
-Require Export rt.restructuring.analysis.basic_facts.task_arrivals.
-Require Export rt.restructuring.analysis.abstract.core.abstract_rta.
+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.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/core/run_to_completion_threshold.v b/restructuring/analysis/abstract/core/run_to_completion_threshold.v
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/definitions.v
similarity index 100%
rename from restructuring/analysis/abstract/core/definitions.v
rename to restructuring/analysis/abstract/definitions.v
diff --git a/restructuring/analysis/abstract/instantiations/ideal_processor.v b/restructuring/analysis/abstract/ideal_jlfp_rta.v
similarity index 99%
rename from restructuring/analysis/abstract/instantiations/ideal_processor.v
rename to restructuring/analysis/abstract/ideal_jlfp_rta.v
index f8bb0094128a93e8bbb2eb4926239a0ba2b95e16..535e0b06cd37893e51884e301ce457cad276b6b3 100644
--- a/restructuring/analysis/abstract/instantiations/ideal_processor.v
+++ b/restructuring/analysis/abstract/ideal_jlfp_rta.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
-Require Export rt.restructuring.analysis.abstract.core.abstract_seq_rta.
+Require Export rt.restructuring.analysis.concepts.priority_inversion.
+Require Export rt.restructuring.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 ... *)
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/run_to_completion.v
similarity index 98%
rename from restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
rename to restructuring/analysis/abstract/run_to_completion.v
index faf66a2b10e0dcdd90205246b46b5a0437979942..63f0ef08d9f68ec655b8a0ed44c7f4d0bc7555e4 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/run_to_completion.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
-Require Export rt.restructuring.analysis.abstract.core.definitions.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.abstract.definitions.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/core/reduction_of_search_space.v b/restructuring/analysis/abstract/search_space.v
similarity index 100%
rename from restructuring/analysis/abstract/core/reduction_of_search_space.v
rename to restructuring/analysis/abstract/search_space.v
diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
deleted file mode 100644
index e9c18f44565063ee8952ce59d4232593ecde5d18..0000000000000000000000000000000000000000
--- a/restructuring/analysis/arrival/rbf.v
+++ /dev/null
@@ -1,92 +0,0 @@
-Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.arrival.workload_bound.
-
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
-(** * Request Bound Functions (RBF) *)
-(** In this section, we prove some properties of Request Bound Functions (RBF). *)
-Section RequestBoundFunctions.
-
- (** Consider any type of tasks ... *)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
-
- (** ... and any type of jobs associated with these tasks. *)
- Context {Job : JobType}.
- Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
-
- (** Consider any arrival sequence. *)
- Variable arr_seq : arrival_sequence Job.
- Hypothesis H_arrival_times_are_consistent:
- consistent_arrival_times arr_seq.
-
- (** Let tsk be any task. *)
- Variable tsk : Task.
-
- (** Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts
- [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function
- that equals 0 for the empty interval delta = 0. *)
- Context `{MaxArrivals Task}.
- Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
- Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
-
- (** Let's define some local names for clarity. *)
- Let task_rbf := task_request_bound_function tsk.
-
- (** We prove that [task_rbf 0] is equal to 0. *)
- Lemma task_rbf_0_zero:
- task_rbf 0 = 0.
- Proof.
- rewrite /task_rbf /task_request_bound_function.
- apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.
- by move: H_valid_arrival_curve => [T1 T2].
- Qed.
-
- (** We prove that task_rbf is monotone. *)
- Lemma task_rbf_monotone:
- monotone task_rbf leq.
- Proof.
- rewrite /monotone; intros ? ? LE.
- rewrite /task_rbf /task_request_bound_function leq_mul2l.
- apply/orP; right.
- by move: H_valid_arrival_curve => [_ T]; apply T.
- Qed.
-
- (** Consider any job j of tsk. This guarantees that
- there exists at least one job of task tsk. *)
- Variable j : Job.
- Hypothesis H_j_arrives : arrives_in arr_seq j.
- Hypothesis H_job_of_tsk : job_task j = tsk.
-
- (** Then we prove that task_rbf 1 is greater than or equal to task cost. *)
- Lemma task_rbf_1_ge_task_cost:
- task_rbf 1 >= task_cost tsk.
- Proof.
- have ALT: forall n, n = 0 \/ n > 0.
- { by clear; intros n; destruct n; [left | right]. }
- specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.
- rewrite leqNgt; apply/negP; intros CONTR.
- move: H_is_arrival_curve => ARRB.
- specialize (ARRB (job_arrival j) (job_arrival j + 1)).
- feed ARRB; first by rewrite leq_addr.
- rewrite addKn in ARRB.
- move: CONTR; rewrite /task_rbf /task_request_bound_function; move => CONTR.
- move: CONTR; rewrite -{2}[task_cost tsk]muln1 ltn_mul2l; move => /andP [_ CONTR].
- move: CONTR; rewrite -addn1 -{3}[1]add0n leq_add2r leqn0; move => /eqP CONTR.
- move: ARRB; rewrite CONTR leqn0 eqn0Ngt; move => /negP T; apply: T.
- rewrite /number_of_task_arrivals -has_predT.
- rewrite /task_arrivals_between.
- apply/hasP; exists j; last by done.
- rewrite /arrivals_between addn1 big_nat_recl; last by done.
- rewrite big_geq ?cats0; last by done.
- rewrite mem_filter.
- apply/andP; split.
- - by apply/eqP.
- - move: H_j_arrives => [t ARR].
- move: (ARR) => CONS.
- apply H_arrival_times_are_consistent in CONS.
- by rewrite CONS.
- Qed.
-
-End RequestBoundFunctions.
\ No newline at end of file
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
deleted file mode 100644
index 98471fce2d2ec76c77e051e42b8ecc53bca7ea49..0000000000000000000000000000000000000000
--- a/restructuring/analysis/arrival/workload_bound.v
+++ /dev/null
@@ -1,291 +0,0 @@
-Require Export rt.restructuring.analysis.basic_facts.workload.
-Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Export rt.restructuring.model.arrival.arrival_curves.
-
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
-(** * Task Workload Bounded by Arrival Curves *)
-Section TaskWorkloadBoundedByArrivalCurves.
-
- (** Consider any type of tasks ... *)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
-
- (** ... and any type of jobs associated with these tasks. *)
- Context {Job : JobType}.
- Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
- Context `{JobCost Job}.
-
- (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
- Variable arr_seq : arrival_sequence Job.
- Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
-
- (** ... and any ideal uniprocessor schedule of this arrival sequence.*)
- Variable sched : schedule (ideal.processor_state Job).
- Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
-
- (** Consider an FP policy that indicates a higher-or-equal priority relation. *)
- Variable higher_eq_priority : FP_policy Task.
- Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.
-
- (** For simplicity, let's define some local names. *)
- Let arrivals_between := arrivals_between arr_seq.
-
- (** We define the notion of request bound function. *)
- Section RequestBoundFunction.
-
- (** Let MaxArrivals denote any function that takes a task and an interval length
- and returns the associated number of job arrivals of the task. *)
- Context `{MaxArrivals Task}.
-
- (** In this section, we define a bound for the workload of a single task
- under uniprocessor FP scheduling. *)
- Section SingleTask.
-
- (** Consider any task tsk that is to be scheduled in an interval of length delta. *)
- Variable tsk : Task.
- Variable delta : duration.
-
- (** We define the following workload bound for the task. *)
- Definition task_request_bound_function := task_cost tsk * max_arrivals tsk delta.
-
- End SingleTask.
-
- (** In this section, we define a bound for the workload of multiple tasks. *)
- Section AllTasks.
-
- (** Consider a task set ts... *)
- Variable ts : list Task.
-
- (** ...and let tsk be any task in task set. *)
- Variable tsk : Task.
-
- (** Let delta be the length of the interval of interest. *)
- Variable delta : duration.
-
- (** Recall the definition of higher-or-equal-priority task and
- the per-task workload bound for FP scheduling. *)
- Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
- Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
-
- (** Using the sum of individual workload bounds, we define the following bound
- for the total workload of tasks in any interval of length delta. *)
- Definition total_request_bound_function :=
- \sum_(tsk <- ts) task_request_bound_function tsk delta.
-
- (** Similarly, we define the following bound for the total workload of tasks of
- higher-or-equal priority (with respect to tsk) in any interval of length delta. *)
- Definition total_hep_request_bound_function_FP :=
- \sum_(tsk_other <- ts | is_hep_task tsk_other)
- task_request_bound_function tsk_other delta.
-
- (** We also define a bound for the total workload of higher-or-equal
- priority tasks other than tsk in any interval of length delta. *)
- Definition total_ohep_request_bound_function_FP :=
- \sum_(tsk_other <- ts | is_other_hep_task tsk_other)
- task_request_bound_function tsk_other delta.
-
- End AllTasks.
-
- End RequestBoundFunction.
-
- (** In this section we prove some lemmas about request bound functions. *)
- Section ProofWorkloadBound.
-
- (** Consider a task set ts... *)
- Variable ts : list Task.
-
- (** ...and let tsk be any task in ts. *)
- Variable tsk : Task.
- Hypothesis H_tsk_in_ts : tsk \in ts.
-
- (** Assume that the job costs are no larger than the task costs. *)
- Hypothesis H_job_cost_le_task_cost :
- cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
-
- (** Next, we assume that all jobs come from the task set. *)
- Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
-
- (** Let max_arrivals be any arrival bound for taskset ts. *)
- Context `{MaxArrivals Task}.
- Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
-
- (** Let's define some local names for clarity. *)
- Let task_rbf := task_request_bound_function tsk.
- Let total_rbf := total_request_bound_function ts.
- Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
- Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
-
- (** Next, we consider any job j of tsk. *)
- Variable j : Job.
- Hypothesis H_j_arrives : arrives_in arr_seq j.
- Hypothesis H_job_of_tsk : job_task j = tsk.
-
- (** Next, we say that two jobs j1 and j2 are in relation other_higher_eq_priority, iff
- j1 has higher or equal priority than j2 and is produced by a different task. *)
- Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
-
- (** Next, we recall the notions of total workload of jobs... *)
- Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between t1 t2).
-
- (** ...notions of workload of higher or equal priority jobs... *)
- Let total_hep_workload t1 t2 :=
- workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between t1 t2).
-
- (** ... workload of other higher or equal priority jobs... *)
- Let total_ohep_workload t1 t2 :=
- workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between t1 t2).
-
- (** ... and the workload of jobs of the same task as job j. *)
- Let task_workload t1 t2 :=
- workload_of_jobs (job_of_task tsk) (arrivals_between t1 t2).
-
- (** In this section we prove that the workload of any jobs is
- no larger than the request bound function. *)
- Section WorkloadIsBoundedByRBF.
-
- (** Consider any time t and any interval of length delta. *)
- Variable t : instant.
- Variable delta : instant.
-
- (** First, we show that workload of task tsk is bounded by
- the number of arrivals of the task times the cost of the task. *)
- Lemma task_workload_le_num_of_arrivals_times_cost:
- task_workload t (t + delta)
- <= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta).
- Proof.
- rewrite // /number_of_task_arrivals -sum1_size big_distrr /= big_filter.
- rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs.
- rewrite /same_task -H_job_of_tsk muln1.
- apply leq_sum_seq; move => j0 IN0 /eqP EQ.
- rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto.
- by apply H_job_cost_le_task_cost.
- Qed.
-
- (** As a corollary, we prove that workload of task is
- no larger the than task request bound function. *)
- Corollary task_workload_le_task_rbf:
- task_workload t (t + delta) <= task_rbf delta.
- Proof.
- apply leq_trans with
- (task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta));
- first by apply task_workload_le_num_of_arrivals_times_cost.
- rewrite leq_mul2l; apply/orP; right.
- rewrite -{2}[delta](addKn t).
- by apply H_is_arrival_bound; last rewrite leq_addr.
- Qed.
-
- (** Next, we prove that total workload of other tasks with
- higher-or-equal priority is no larger than the total
- request bound function. *)
- Lemma total_workload_le_total_rbf:
- total_ohep_workload t (t + delta) <= total_ohep_rbf delta.
- Proof.
- set l := arrivals_between t (t + delta).
- set hep := higher_eq_priority.
- apply leq_trans with
- (\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
- (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
- { intros.
- rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
- rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
- have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk && (job_task x != tsk)).
- rewrite EXCHANGE /=; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
- rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
- apply leq_sum; move => j0 /andP [IN0 HP0].
- rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
- by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
- }
- apply leq_sum_seq; intros tsk0 INtsk0 HP0.
- apply leq_trans with
- (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
- { rewrite -sum1_size big_distrr /= big_filter.
- rewrite /workload_of_jobs.
- rewrite muln1 /l /arrivals_between /arrival_sequence.arrivals_between.
- apply leq_sum_seq; move => j0 IN0 /eqP EQ.
- by rewrite -EQ; apply H_job_cost_le_task_cost; apply in_arrivals_implies_arrived in IN0.
- }
- { rewrite leq_mul2l; apply/orP; right.
- rewrite -{2}[delta](addKn t).
- by apply H_is_arrival_bound; last rewrite leq_addr.
- }
- Qed.
-
- (** Next, we prove that total workload of tasks with higher-or-equal
- priority is no larger than the total request bound function. *)
- Lemma total_workload_le_total_rbf':
- total_hep_workload t (t + delta) <= total_hep_rbf delta.
- Proof.
- set l := arrivals_between t (t + delta).
- set hep := higher_eq_priority.
- apply leq_trans with
- (n := \sum_(tsk' <- ts | hep tsk' tsk)
- (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
- { rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.
- have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk).
- rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
- rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
- apply leq_sum; move => j0 /andP [IN0 HP0].
- rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
- by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
- }
- apply leq_sum_seq; intros tsk0 INtsk0 HP0.
- apply leq_trans with
- (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
- { rewrite -sum1_size big_distrr /= big_filter.
- rewrite -/l /workload_of_jobs.
- rewrite muln1.
- apply leq_sum_seq; move => j0 IN0 /eqP EQ.
- rewrite -EQ.
- apply H_job_cost_le_task_cost.
- by apply in_arrivals_implies_arrived in IN0.
- }
- { rewrite leq_mul2l; apply/orP; right.
- rewrite -{2}[delta](addKn t).
- by apply H_is_arrival_bound; last rewrite leq_addr.
- }
- Qed.
-
- (** Next, we prove that total workload of tasks is
- no larger than the total request bound function. *)
- Lemma total_workload_le_total_rbf'':
- total_workload t (t + delta) <= total_rbf delta.
- Proof.
- set l := arrivals_between t (t + delta).
- apply leq_trans with
- (n := \sum_(tsk' <- ts)
- (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
- { rewrite /total_workload.
- have EXCHANGE := exchange_big_dep predT.
- rewrite EXCHANGE /=; clear EXCHANGE; last by done.
- rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
- apply leq_sum; move => j0 /andP [IN0 HP0].
- rewrite big_mkcond (big_rem (job_task j0)) /=.
- rewrite eq_refl; apply leq_addr.
- by apply in_arrivals_implies_arrived in IN0;
- apply H_all_jobs_from_taskset.
- }
- apply leq_sum_seq; intros tsk0 INtsk0 HP0.
- apply leq_trans with
- (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
- { rewrite -sum1_size big_distrr /= big_filter.
- rewrite -/l /workload_of_jobs.
- rewrite muln1.
- apply leq_sum_seq; move => j0 IN0 /eqP EQ.
- rewrite -EQ.
- apply H_job_cost_le_task_cost.
- by apply in_arrivals_implies_arrived in IN0.
- }
- { rewrite leq_mul2l; apply/orP; right.
- rewrite -{2}[delta](addKn t).
- by apply H_is_arrival_bound; last rewrite leq_addr.
- }
- Qed.
-
- End WorkloadIsBoundedByRBF.
-
- End ProofWorkloadBound.
-
-End TaskWorkloadBoundedByArrivalCurves.
\ No newline at end of file
diff --git a/restructuring/analysis/basic_facts/all.v b/restructuring/analysis/basic_facts/all.v
deleted file mode 100644
index 51567b1bfec272072e32608a9b5fa5b0f8643ba6..0000000000000000000000000000000000000000
--- a/restructuring/analysis/basic_facts/all.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Require Export rt.restructuring.analysis.basic_facts.service.
-Require Export rt.restructuring.analysis.basic_facts.service_of_jobs.
-Require Export rt.restructuring.analysis.basic_facts.completion.
-Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
-Require Export rt.restructuring.analysis.basic_facts.sequential.
-Require Export rt.restructuring.analysis.basic_facts.arrivals.
-Require Export rt.restructuring.analysis.basic_facts.deadlines.
-Require Export rt.restructuring.analysis.basic_facts.workload.
diff --git a/restructuring/analysis/basic_facts/ideal_schedule.v b/restructuring/analysis/basic_facts/ideal_schedule.v
deleted file mode 100644
index 4759a455b0015159e26ff37accbe96401318711f..0000000000000000000000000000000000000000
--- a/restructuring/analysis/basic_facts/ideal_schedule.v
+++ /dev/null
@@ -1,113 +0,0 @@
-From mathcomp Require Import all_ssreflect.
-Require Export rt.restructuring.model.processor.platform_properties.
-
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
-
-(** Note: we do not re-export the basic definitions to avoid littering the global
- namespace with type class instances. *)
-
-(** In this section we estlish the classes to which an ideal schedule belongs. *)
-Section ScheduleClass.
-
- Local Transparent service_in scheduled_in scheduled_on.
- (** Consider any job type and the ideal processor model. *)
- Context {Job: JobType}.
- Context `{JobArrival Job}.
- Context `{JobCost Job}.
-
- (** We note that the ideal processor model is indeed a uniprocessor
- model. *)
- Lemma ideal_proc_model_is_a_uniprocessor_model:
- uniprocessor_model (processor_state Job).
- Proof.
- move=> j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].
- by move: E1 E2=>->[].
- Qed.
-
- (** We observe that the ideal processor model falls into the category
- of ideal-progress models, i.e., a scheduled job always receives
- service. *)
- Lemma ideal_proc_model_ensures_ideal_progress:
- ideal_progress_proc_model (processor_state Job).
- Proof.
- move=> j s /existsP[[]/eqP->]/=.
- by rewrite eqxx.
- Qed.
-
- (** The ideal processor model is a unit-service model. *)
- Lemma ideal_proc_model_provides_unit_service:
- unit_service_proc_model (processor_state Job).
- Proof.
- move=> j s.
- rewrite /service_in/=/nat_of_bool.
- by case:ifP.
- Qed.
-
- Lemma scheduled_in_def (j : Job) s :
- scheduled_in j s = (s == Some j).
- Proof.
- rewrite /scheduled_in/scheduled_on/=.
- case: existsP=>[[_->]//|].
- case: (s == Some j)=>//=[[]].
- by exists.
- Qed.
-
- Lemma scheduled_at_def sched (j : Job) t :
- scheduled_at sched j t = (sched t == Some j).
- Proof.
- by rewrite /scheduled_at scheduled_in_def.
- Qed.
-
- Lemma service_in_is_scheduled_in (j : Job) s :
- service_in j s = scheduled_in j s.
- Proof.
- by rewrite /service_in scheduled_in_def/=.
- Qed.
-
- Lemma service_at_is_scheduled_at sched (j : Job) t :
- service_at sched j t = scheduled_at sched j t.
- Proof.
- by rewrite /service_at service_in_is_scheduled_in.
- Qed.
-
- (** Next we prove a lemma which helps us to do a case analysis on
- the state of an ideal schedule. *)
- Lemma ideal_proc_model_sched_case_analysis:
- forall (sched : schedule (ideal.processor_state Job)) (t : instant),
- is_idle sched t \/ exists j, scheduled_at sched j t.
- Proof.
- intros.
- unfold is_idle; simpl; destruct (sched t) eqn:EQ.
- - by right; exists s; auto; rewrite scheduled_at_def EQ.
- - by left; auto.
- Qed.
-
-End ScheduleClass.
-
-(** * Automation *)
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
- will be able to apply them automatically. *)
-Hint Resolve ideal_proc_model_is_a_uniprocessor_model
- ideal_proc_model_ensures_ideal_progress
- ideal_proc_model_provides_unit_service : basic_facts.
-
-(** We also provide tactics for case analysis on ideal processor state. *)
-
-(** The first tactic generates two subgoals: one with idle processor and
- the other with processor executing a job named JobName. *)
-Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
- let Idle := fresh "Idle" in
- let Sched := fresh "Sched_" JobName in
- destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].
-
-(** The second tactic is similar to the first, but it additionally generates
- two equalities: [sched t = None] and [sched t = Some j]. *)
-Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
- let Idle := fresh "Idle" in
- let IdleEq := fresh "Eq" Idle in
- let Sched := fresh "Sched_" JobName in
- let SchedEq := fresh "Eq" Sched in
- destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
- [move: (Idle) => /eqP IdleEq; rewrite ?IdleEq
- | move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].
diff --git a/restructuring/analysis/definitions/busy_interval.v b/restructuring/analysis/concepts/busy_interval.v
similarity index 98%
rename from restructuring/analysis/definitions/busy_interval.v
rename to restructuring/analysis/concepts/busy_interval.v
index bb1fff380744394263ee947200a1ea5b747358e3..f2cde4cd59feafbbc1eac0e121ee50aadebb9879 100644
--- a/restructuring/analysis/definitions/busy_interval.v
+++ b/restructuring/analysis/concepts/busy_interval.v
@@ -1,5 +1,5 @@
Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/definitions/priority_inversion.v b/restructuring/analysis/concepts/priority_inversion.v
similarity index 97%
rename from restructuring/analysis/definitions/priority_inversion.v
rename to restructuring/analysis/concepts/priority_inversion.v
index a868dba5cf986fe8fd5b01483bdb668321c2ee7c..bc5271e686528297e428ad187a5746a9272377b2 100644
--- a/restructuring/analysis/definitions/priority_inversion.v
+++ b/restructuring/analysis/concepts/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.definitions.busy_interval.
+Require Export rt.restructuring.analysis.concepts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/concepts/request_bound_function.v b/restructuring/analysis/concepts/request_bound_function.v
new file mode 100644
index 0000000000000000000000000000000000000000..f4401de560019e50f3624c3a81f4d3e14ebefbcf
--- /dev/null
+++ b/restructuring/analysis/concepts/request_bound_function.v
@@ -0,0 +1,94 @@
+Require Export rt.restructuring.model.arrival.arrival_curves.
+Require Export rt.restructuring.model.priority.classes.
+
+(** The following definitions assume ideal uniprocessor 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.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * Request Bound Function (RBF) *)
+
+(** We define the notion of a task's request-bound function (RBF), as well as
+ the total request bound function of a set of tasks. *)
+
+Section TaskWorkloadBoundedByArrivalCurves.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** ... and any type of jobs associated with these tasks, where each task has
+ a cost. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+
+ (** Consider any ideal uniprocessor schedule of these jobs... *)
+ Variable sched : schedule (ideal.processor_state Job).
+
+ (** ... and an FP policy that indicates a higher-or-equal priority
+ relation. *)
+ Variable higher_eq_priority : FP_policy Task.
+
+ (** Let MaxArrivals denote any function that takes a task and an interval length
+ and returns the associated number of job arrivals of the task. *)
+ Context `{MaxArrivals Task}.
+
+ (** ** RBF of a Single Task *)
+
+ (** In this section, we define a bound for the workload of a single task
+ under uniprocessor FP scheduling. *)
+ Section SingleTask.
+
+ (** Consider any task tsk that is to be scheduled in an interval of length delta. *)
+ Variable tsk : Task.
+ Variable delta : duration.
+
+ (** We define the following workload bound for the task. *)
+ Definition task_request_bound_function := task_cost tsk * max_arrivals tsk delta.
+
+ End SingleTask.
+
+ (** ** Total RBF of Multiple Tasks *)
+
+ (** In this section, we define a bound for the workload of multiple tasks. *)
+ Section AllTasks.
+
+ (** Consider a task set ts... *)
+ Variable ts : list Task.
+
+ (** ...and let tsk be any task in task set. *)
+ Variable tsk : Task.
+
+ (** Let delta be the length of the interval of interest. *)
+ Variable delta : duration.
+
+ (** Recall the definition of higher-or-equal-priority task and the per-task
+ workload bound for FP scheduling. *)
+ Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
+ Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
+
+ (** Using the sum of individual workload bounds, we define the following
+ bound for the total workload of tasks in any interval of length
+ delta. *)
+ Definition total_request_bound_function :=
+ \sum_(tsk <- ts) task_request_bound_function tsk delta.
+
+ (** Similarly, we define the following bound for the total workload of
+ tasks of higher-or-equal priority (with respect to tsk) in any interval
+ of length delta. *)
+ Definition total_hep_request_bound_function_FP :=
+ \sum_(tsk_other <- ts | is_hep_task tsk_other)
+ task_request_bound_function tsk_other delta.
+
+ (** We also define a bound for the total workload of higher-or-equal
+ priority tasks other than tsk in any interval of length delta. *)
+ Definition total_ohep_request_bound_function_FP :=
+ \sum_(tsk_other <- ts | is_other_hep_task tsk_other)
+ task_request_bound_function tsk_other delta.
+
+ End AllTasks.
+
+End TaskWorkloadBoundedByArrivalCurves.
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/concepts/schedulability.v
similarity index 98%
rename from restructuring/analysis/schedulability.v
rename to restructuring/analysis/concepts/schedulability.v
index a3de0ced0c3dbcffad206ca9174b477b1a5bf2ef..eaa3f136be86bc98009404b739cab8a893d6f75c 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/concepts/schedulability.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
Require Import rt.restructuring.model.task.absolute_deadline.
Section Task.
diff --git a/restructuring/analysis/definitions/no_carry_in.v b/restructuring/analysis/definitions/carry_in.v
similarity index 100%
rename from restructuring/analysis/definitions/no_carry_in.v
rename to restructuring/analysis/definitions/carry_in.v
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/definitions/task_schedule.v
similarity index 96%
rename from restructuring/analysis/task_schedule.v
rename to restructuring/analysis/definitions/task_schedule.v
index 2f7eb103e49e347c085393f1a0c54177b7c6f4ba..abd2757e60b7bdc36bca2613f23b3f62817c37f6 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/definitions/task_schedule.v
@@ -1,5 +1,5 @@
Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/behavior/all.v b/restructuring/analysis/facts/behavior/all.v
new file mode 100644
index 0000000000000000000000000000000000000000..dbd7016f99146b49c88cfe95ce6e9da2f92b37a7
--- /dev/null
+++ b/restructuring/analysis/facts/behavior/all.v
@@ -0,0 +1,8 @@
+Require Export rt.restructuring.analysis.facts.behavior.service.
+Require Export rt.restructuring.analysis.facts.behavior.service_of_jobs.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
+Require Export rt.restructuring.analysis.facts.behavior.sequential.
+Require Export rt.restructuring.analysis.facts.behavior.arrivals.
+Require Export rt.restructuring.analysis.facts.behavior.deadlines.
+Require Export rt.restructuring.analysis.facts.behavior.workload.
diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/facts/behavior/arrivals.v
similarity index 100%
rename from restructuring/analysis/basic_facts/arrivals.v
rename to restructuring/analysis/facts/behavior/arrivals.v
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/facts/behavior/completion.v
similarity index 98%
rename from restructuring/analysis/basic_facts/completion.v
rename to restructuring/analysis/facts/behavior/completion.v
index 35d507ff8947f1e91182c0ce72b3ad8f64e258cf..d32bb55fb100e7eba08aa4ea46cdfedf0e6adc33 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/facts/behavior/completion.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.basic_facts.service.
-Require Export rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.facts.behavior.service.
+Require Export rt.restructuring.analysis.facts.behavior.arrivals.
(** In this file, we establish basic facts about job completions. *)
diff --git a/restructuring/analysis/basic_facts/deadlines.v b/restructuring/analysis/facts/behavior/deadlines.v
similarity index 97%
rename from restructuring/analysis/basic_facts/deadlines.v
rename to restructuring/analysis/facts/behavior/deadlines.v
index fb80bdae30201642d29c4f6c01efc4420ac31dd4..777c92c79cdf3e8de02a1053364b8fd390b0fe62 100644
--- a/restructuring/analysis/basic_facts/deadlines.v
+++ b/restructuring/analysis/facts/behavior/deadlines.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
(** In this file, we observe basic properties of the behavioral job
model w.r.t. deadlines. *)
diff --git a/restructuring/analysis/facts/behavior/ideal_schedule.v b/restructuring/analysis/facts/behavior/ideal_schedule.v
new file mode 100644
index 0000000000000000000000000000000000000000..2435af2fcbd058eeb9db7bf1f13052130b381a3b
--- /dev/null
+++ b/restructuring/analysis/facts/behavior/ideal_schedule.v
@@ -0,0 +1,222 @@
+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.
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
+(** Note: we do not re-export the basic definitions to avoid littering the global
+ namespace with type class instances. *)
+
+(** In this section we estlish the classes to which an ideal schedule belongs. *)
+Section ScheduleClass.
+
+ Local Transparent service_in scheduled_in scheduled_on.
+ (** Consider any job type and the ideal processor model. *)
+ Context {Job: JobType}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** We note that the ideal processor model is indeed a uniprocessor
+ model. *)
+ Lemma ideal_proc_model_is_a_uniprocessor_model:
+ uniprocessor_model (processor_state Job).
+ Proof.
+ move=> j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].
+ by move: E1 E2=>->[].
+ Qed.
+
+ (** We observe that the ideal processor model falls into the category
+ of ideal-progress models, i.e., a scheduled job always receives
+ service. *)
+ Lemma ideal_proc_model_ensures_ideal_progress:
+ ideal_progress_proc_model (processor_state Job).
+ Proof.
+ move=> j s /existsP[[]/eqP->]/=.
+ by rewrite eqxx.
+ Qed.
+
+ (** The ideal processor model is a unit-service model. *)
+ Lemma ideal_proc_model_provides_unit_service:
+ unit_service_proc_model (processor_state Job).
+ Proof.
+ move=> j s.
+ rewrite /service_in/=/nat_of_bool.
+ by case:ifP.
+ Qed.
+
+ Lemma scheduled_in_def (j : Job) s :
+ scheduled_in j s = (s == Some j).
+ Proof.
+ rewrite /scheduled_in/scheduled_on/=.
+ case: existsP=>[[_->]//|].
+ case: (s == Some j)=>//=[[]].
+ by exists.
+ Qed.
+
+ Lemma scheduled_at_def sched (j : Job) t :
+ scheduled_at sched j t = (sched t == Some j).
+ Proof.
+ by rewrite /scheduled_at scheduled_in_def.
+ Qed.
+
+ Lemma service_in_is_scheduled_in (j : Job) s :
+ service_in j s = scheduled_in j s.
+ Proof.
+ by rewrite /service_in scheduled_in_def/=.
+ Qed.
+
+ Lemma service_at_is_scheduled_at sched (j : Job) t :
+ service_at sched j t = scheduled_at sched j t.
+ Proof.
+ by rewrite /service_at service_in_is_scheduled_in.
+ Qed.
+
+ (** Next we prove a lemma which helps us to do a case analysis on
+ the state of an ideal schedule. *)
+ Lemma ideal_proc_model_sched_case_analysis:
+ forall (sched : schedule (ideal.processor_state Job)) (t : instant),
+ is_idle sched t \/ exists j, scheduled_at sched j t.
+ Proof.
+ intros.
+ unfold is_idle; simpl; destruct (sched t) eqn:EQ.
+ - by right; exists s; auto; rewrite scheduled_at_def EQ.
+ - by left; auto.
+ Qed.
+
+End ScheduleClass.
+
+(** * Automation *)
+(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+ will be able to apply them automatically. *)
+Hint Resolve ideal_proc_model_is_a_uniprocessor_model
+ ideal_proc_model_ensures_ideal_progress
+ ideal_proc_model_provides_unit_service : basic_facts.
+
+(** We also provide tactics for case analysis on ideal processor state. *)
+
+(** The first tactic generates two subgoals: one with idle processor and
+ the other with processor executing a job named JobName. *)
+Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
+ let Idle := fresh "Idle" in
+ let Sched := fresh "Sched_" JobName in
+ destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].
+
+(** The second tactic is similar to the first, but it additionally generates
+ two equalities: [sched t = None] and [sched t = Some j]. *)
+Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
+ let Idle := fresh "Idle" in
+ let IdleEq := fresh "Eq" Idle in
+ let Sched := fresh "Sched_" JobName in
+ let SchedEq := fresh "Eq" Sched in
+ destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
+ [move: (Idle) => /eqP IdleEq; rewrite ?IdleEq
+ | move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].
+
+(** * Incremental Service in Ideal Schedule *)
+(** In the following section we prove a few facts about service in ideal schedeule. *)
+(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
+Section IncrementalService.
+
+ (** Consider any job type, ... *)
+ Context {Job : JobType}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** ... any arrival sequence, ... *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
+ Variable sched : schedule (ideal.processor_state Job).
+
+ (** As a base case, we prove that if a job j receives service in
+ some time interval [t1,t2), then there exists a time instant t
+ ∈ [t1,t2) such that j is scheduled at time t and t is the first
+ instant where j receives service. *)
+ Lemma positive_service_during:
+ forall j t1 t2,
+ 0 < service_during sched j t1 t2 ->
+ exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0.
+ Proof.
+ intros j t1 t2 SERV.
+ have LE: t1 <= t2.
+ { rewrite leqNgt; apply/negP; intros CONTR.
+ by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.
+ }
+ destruct (scheduled_at sched j t1) eqn:SCHED.
+ { exists t1; repeat split; try done.
+ - apply/andP; split; first by done.
+ rewrite ltnNge; apply/negP; intros CONTR.
+ by move: SERV; rewrite/service_during big_geq.
+ - by rewrite /service_during big_geq.
+ }
+ { apply negbT in SCHED.
+ move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [t [IN SCHEDt]].
+ rewrite lt0b in SCHEDt.
+ rewrite mem_iota subnKC in IN; last by done.
+ move: IN => /andP [IN1 IN2].
+ move: (exists_first_intermediate_point
+ ((fun t => scheduled_at sched j t)) t1 t IN1 SCHED) => A.
+ feed A; first by rewrite scheduled_at_def/=.
+ move: A => [x [/andP [T1 T4] [T2 T3]]].
+ exists x; repeat split; try done.
+ - apply/andP; split; first by apply ltnW.
+ by apply leq_ltn_trans with t.
+ - apply/eqP; rewrite big_nat_cond big1 //.
+ move => y /andP [T5 _].
+ by apply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.
+ }
+ Qed.
+
+ (** Next, we prove that if in some time interval [t1,t2) a job j
+ receives k units of service, then there exists a time instant t ∈
+ [t1,t2) such that j is scheduled at time t and service of job j
+ within interval [t1,t) is equal to k. *)
+ Lemma incremental_service_during:
+ forall j t1 t2 k,
+ service_during sched j t1 t2 > k ->
+ exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.
+ Proof.
+ intros j t1 t2 k SERV.
+ have LE: t1 <= t2.
+ { rewrite leqNgt; apply/negP; intros CONTR.
+ by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.
+ }
+ induction k; first by apply positive_service_during in SERV.
+ feed IHk; first by apply ltn_trans with k.+1.
+ move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].
+ have SERVk1: service_during sched j t1 t.+1 = k.+1.
+ { rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.
+ rewrite SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.
+ by rewrite /service_during big_nat1 /service_at eqb1 -scheduled_at_def/=.
+ }
+ move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.
+ { by apply/andP; split; first apply leq_trans with t. }
+ rewrite SERVk1 -addn1 leq_add2l; move => SERV.
+ destruct (scheduled_at sched j t.+1) eqn:SCHED.
+ - exists t.+1; repeat split; try done. apply/andP; split.
+ + apply leq_trans with t; by done.
+ + rewrite ltnNge; apply/negP; intros CONTR.
+ by move: SERV; rewrite /service_during big_geq.
+ - apply negbT in SCHED.
+ move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [x [INx SCHEDx]].
+ rewrite lt0b in SCHEDx.
+ rewrite mem_iota subnKC in INx; last by done.
+ move: INx => /andP [INx1 INx2].
+ move: (exists_first_intermediate_point _ _ _ INx1 SCHED) => A.
+ feed A; first by rewrite scheduled_at_def/=.
+ move: A => [y [/andP [T1 T4] [T2 T3]]].
+ exists y; repeat split; try done.
+ + apply/andP; split.
+ apply leq_trans with t; first by done.
+ apply ltnW, ltn_trans with t.+1; by done.
+ by apply leq_ltn_trans with x.
+ + rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].
+ unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.
+ rewrite -{2}[k.+1]addn0 eqn_add2l.
+ rewrite big_nat_cond big1 //; move => z /andP [H5 _].
+ by apply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.
+ Qed.
+
+End IncrementalService.
diff --git a/restructuring/analysis/basic_facts/sequential.v b/restructuring/analysis/facts/behavior/sequential.v
similarity index 100%
rename from restructuring/analysis/basic_facts/sequential.v
rename to restructuring/analysis/facts/behavior/sequential.v
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/facts/behavior/service.v
similarity index 79%
rename from restructuring/analysis/basic_facts/service.v
rename to restructuring/analysis/facts/behavior/service.v
index 543fcdf4b93df4768a3280e0a06901167559aaef..77d36351f9c5b45e37b3b6245daf5bc5152404c3 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/facts/behavior/service.v
@@ -1,5 +1,6 @@
Require Export rt.util.all.
-Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.behavior.all.
+Require Export rt.restructuring.model.processor.platform_properties.
From mathcomp Require Import ssrnat ssrbool fintype.
@@ -576,111 +577,3 @@ Section RelationToScheduled.
End RelationToScheduled.
-Require Import rt.restructuring.model.processor.ideal.
-
-(** * Incremental Service in Ideal Schedule *)
-(** In the following section we prove a few facts about service in ideal schedeule. *)
-(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
-Section IncrementalService.
-
- (** Consider any job type, ... *)
- Context {Job : JobType}.
- Context `{JobArrival Job}.
- Context `{JobCost Job}.
-
- (** ... any arrival sequence, ... *)
- Variable arr_seq : arrival_sequence Job.
-
- (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
- Variable sched : schedule (ideal.processor_state Job).
-
- (** As a base case, we prove that if a job j receives service in
- some time interval [t1,t2), then there exists a time instant t
- ∈ [t1,t2) such that j is scheduled at time t and t is the first
- instant where j receives service. *)
- Lemma positive_service_during:
- forall j t1 t2,
- 0 < service_during sched j t1 t2 ->
- exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0.
- Proof.
- intros j t1 t2 SERV.
- have LE: t1 <= t2.
- { rewrite leqNgt; apply/negP; intros CONTR.
- by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.
- }
- destruct (scheduled_at sched j t1) eqn:SCHED.
- { exists t1; repeat split; try done.
- - apply/andP; split; first by done.
- rewrite ltnNge; apply/negP; intros CONTR.
- by move: SERV; rewrite/service_during big_geq.
- - by rewrite /service_during big_geq.
- }
- { apply negbT in SCHED.
- move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [t [IN SCHEDt]].
- rewrite lt0b in SCHEDt.
- rewrite mem_iota subnKC in IN; last by done.
- move: IN => /andP [IN1 IN2].
- move: (exists_first_intermediate_point
- ((fun t => scheduled_at sched j t)) t1 t IN1 SCHED) => A.
- feed A; first by rewrite scheduled_at_def/=.
- move: A => [x [/andP [T1 T4] [T2 T3]]].
- exists x; repeat split; try done.
- - apply/andP; split; first by apply ltnW.
- by apply leq_ltn_trans with t.
- - apply/eqP; rewrite big_nat_cond big1 //.
- move => y /andP [T5 _].
- by apply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.
- }
- Qed.
-
- (** Next, we prove that if in some time interval [t1,t2) a job j
- receives k units of service, then there exists a time instant t ∈
- [t1,t2) such that j is scheduled at time t and service of job j
- within interval [t1,t) is equal to k. *)
- Lemma incremental_service_during:
- forall j t1 t2 k,
- service_during sched j t1 t2 > k ->
- exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.
- Proof.
- intros j t1 t2 k SERV.
- have LE: t1 <= t2.
- { rewrite leqNgt; apply/negP; intros CONTR.
- by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.
- }
- induction k; first by apply positive_service_during in SERV.
- feed IHk; first by apply ltn_trans with k.+1.
- move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].
- have SERVk1: service_during sched j t1 t.+1 = k.+1.
- { rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.
- rewrite SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.
- by rewrite /service_during big_nat1 /service_at eqb1 -scheduled_at_def/=.
- }
- move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.
- { by apply/andP; split; first apply leq_trans with t. }
- rewrite SERVk1 -addn1 leq_add2l; move => SERV.
- destruct (scheduled_at sched j t.+1) eqn:SCHED.
- - exists t.+1; repeat split; try done. apply/andP; split.
- + apply leq_trans with t; by done.
- + rewrite ltnNge; apply/negP; intros CONTR.
- by move: SERV; rewrite /service_during big_geq.
- - apply negbT in SCHED.
- move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [x [INx SCHEDx]].
- rewrite lt0b in SCHEDx.
- rewrite mem_iota subnKC in INx; last by done.
- move: INx => /andP [INx1 INx2].
- move: (exists_first_intermediate_point _ _ _ INx1 SCHED) => A.
- feed A; first by rewrite scheduled_at_def/=.
- move: A => [y [/andP [T1 T4] [T2 T3]]].
- exists y; repeat split; try done.
- + apply/andP; split.
- apply leq_trans with t; first by done.
- apply ltnW, ltn_trans with t.+1; by done.
- by apply leq_ltn_trans with x.
- + rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].
- unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.
- rewrite -{2}[k.+1]addn0 eqn_add2l.
- rewrite big_nat_cond big1 //; move => z /andP [H5 _].
- by apply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.
- Qed.
-
-End IncrementalService.
\ No newline at end of file
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/facts/behavior/service_of_jobs.v
similarity index 98%
rename from restructuring/analysis/basic_facts/service_of_jobs.v
rename to restructuring/analysis/facts/behavior/service_of_jobs.v
index 2d10fa54b2a3d6ea80b7b34303a29e8433c98d5d..706ff2a146063b4f8d6c6c673c752b834ec179ef 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/facts/behavior/service_of_jobs.v
@@ -1,7 +1,7 @@
Require Export rt.restructuring.model.aggregate.workload.
Require Export rt.restructuring.model.aggregate.service_of_jobs.
-Require Export rt.restructuring.analysis.basic_facts.completion.
-
+Require Export rt.restructuring.analysis.facts.behavior.completion.
+Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
Require Import rt.restructuring.model.processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
@@ -371,4 +371,4 @@ Section IdealModelLemmas.
End WorkloadServiceAndCompletion.
-End IdealModelLemmas.
\ No newline at end of file
+End IdealModelLemmas.
diff --git a/restructuring/analysis/basic_facts/task_arrivals.v b/restructuring/analysis/facts/behavior/task_arrivals.v
similarity index 100%
rename from restructuring/analysis/basic_facts/task_arrivals.v
rename to restructuring/analysis/facts/behavior/task_arrivals.v
diff --git a/restructuring/analysis/basic_facts/workload.v b/restructuring/analysis/facts/behavior/workload.v
similarity index 94%
rename from restructuring/analysis/basic_facts/workload.v
rename to restructuring/analysis/facts/behavior/workload.v
index 942bd65826d11848c034177461812fa27a86476e..f8286ab2bdbd927eb7f4ff6271e68ccc96e76231 100644
--- a/restructuring/analysis/basic_facts/workload.v
+++ b/restructuring/analysis/facts/behavior/workload.v
@@ -1,5 +1,5 @@
Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.facts.behavior.arrivals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval.v
similarity index 99%
rename from restructuring/analysis/facts/busy_interval_exists.v
rename to restructuring/analysis/facts/busy_interval.v
index d97ca3841ebd13e3fc86871f17f53103fabfefae..739f2f4922d42021f7b9113c898436f120857b05 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval.v
@@ -1,7 +1,7 @@
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.analysis.definitions.priority_inversion.
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.concepts.priority_inversion.
+Require Export rt.restructuring.analysis.facts.behavior.all.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/carry_in.v
similarity index 99%
rename from restructuring/analysis/facts/no_carry_in_exists.v
rename to restructuring/analysis/facts/carry_in.v
index 26c4bdaf9381a9ca63792212226a7d6e0b67b426..2b036253eb5bf7e22b202bd5b26ec39b0a0db113 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/carry_in.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.definitions.no_carry_in.
-Require Export rt.restructuring.analysis.facts.busy_interval_exists.
+Require Export rt.restructuring.analysis.definitions.carry_in.
+Require Export rt.restructuring.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/facts/preemption/job/limited.v
similarity index 99%
rename from restructuring/analysis/basic_facts/preemption/job/limited.v
rename to restructuring/analysis/facts/preemption/job/limited.v
index 392482c93f18d6973b3d99fb3511379dd6420959..909f35c5cb7f15ba326c215b8a5ab749c9baed75 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/facts/preemption/job/limited.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.facts.behavior.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.schedule.limited_preemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/facts/preemption/job/nonpreemptive.v
similarity index 98%
rename from restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
rename to restructuring/analysis/facts/preemption/job/nonpreemptive.v
index efa8ad2f52566c4295efe03a29a690b49895bc82..8ac8a82782da01e72b9c596513e849b9911b684b 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/job/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.facts.behavior.all.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.schedule.nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/facts/preemption/job/preemptive.v
similarity index 100%
rename from restructuring/analysis/basic_facts/preemption/job/preemptive.v
rename to restructuring/analysis/facts/preemption/job/preemptive.v
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
similarity index 90%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/floating.v
index 4a2d046f7f65fae448de76fbc07e192545501b67..bba9d81279797c21eb83dd23c3ba88bdc910a23f 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/floating.v
@@ -1,7 +1,7 @@
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.facts.preemption.task.floating.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v b/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
similarity index 99%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 8ea77ec19d16d33b6b2ae0ce9fd92e6f35b6cee1..ef91d3329a2b4301664bba6b4245ba26ad2fe718 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -1,5 +1,5 @@
Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.facts.behavior.all.
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Run-to-Completion Threshold *)
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/facts/preemption/rtc_threshold/limited.v
similarity index 97%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/limited.v
index f515e6358616c052713f1d6c625c67af04287f96..0d1606ed3a22ef2ff70c9c39b9862d3ba105a8ff 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/limited.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Export rt.restructuring.analysis.facts.preemption.task.limited.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
similarity index 97%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 8875e0e6feac0c3174ad3d3245ce308263c6bd01..335c6df92e953fce398d9d2728d0ce94deb84b96 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
similarity index 94%
rename from restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
rename to restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
index 25f5ab7fe14ec75a1c43a138a49dd1ac28f5f2fe..d8b601ffad28d6bf2e679bd8edc7edc77325095c 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -1,6 +1,6 @@
Require Import rt.restructuring.model.preemption.fully_preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
-Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
+Require Import rt.restructuring.analysis.facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/facts/preemption/task/floating.v
similarity index 98%
rename from restructuring/analysis/basic_facts/preemption/task/floating.v
rename to restructuring/analysis/facts/preemption/task/floating.v
index 286e8d2e23f6070fd974956b3dff2e189db435b5..28c39720c8b18f77bd73eb9ca95c1c7c69c8c439 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/facts/preemption/task/floating.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
+Require Export rt.restructuring.analysis.facts.preemption.job.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/facts/preemption/task/limited.v
similarity index 98%
rename from restructuring/analysis/basic_facts/preemption/task/limited.v
rename to restructuring/analysis/facts/preemption/task/limited.v
index fb3661327163aed67e27734101b6b5afb65b2077..a3d9a686274ea4402a9231702b51c130dd85da58 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/facts/preemption/task/limited.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
+Require Export rt.restructuring.analysis.facts.preemption.job.limited.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v b/restructuring/analysis/facts/preemption/task/nonpreemptive.v
similarity index 97%
rename from restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
rename to restructuring/analysis/facts/preemption/task/nonpreemptive.v
index 717d7cdde85b9a6bb3f686c7d84bb70841b24013..fd3ba3548d369adfd1ef531269faf27602e8d384 100644
--- a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/task/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+Require Export rt.restructuring.analysis.facts.preemption.job.nonpreemptive.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/facts/preemption/task/preemptive.v
similarity index 96%
rename from restructuring/analysis/basic_facts/preemption/task/preemptive.v
rename to restructuring/analysis/facts/preemption/task/preemptive.v
index 1a33d34bbc01692bc0cce0d9ea131945701af2b6..f04b0de7e803af1d52e60fb4a1b1fd6362933aa4 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/facts/preemption/task/preemptive.v
@@ -1,5 +1,5 @@
Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
+Require Export rt.restructuring.analysis.facts.preemption.job.preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion.v
similarity index 99%
rename from restructuring/analysis/facts/priority_inversion_is_bounded.v
rename to restructuring/analysis/facts/priority_inversion.v
index 93c89d784982f9741f7c725455da8da15f224f94..16e07b07b757e698f18f5f17f0b1863a90935900 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion.v
@@ -1,6 +1,10 @@
Require Export rt.restructuring.model.task.preemption.parameters.
Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
+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.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/facts/rbf.v b/restructuring/analysis/facts/rbf.v
new file mode 100644
index 0000000000000000000000000000000000000000..93dad5fd070428715469310251ac83d45db6c5ca
--- /dev/null
+++ b/restructuring/analysis/facts/rbf.v
@@ -0,0 +1,323 @@
+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.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+
+(** * Facts about Request Bound Functions (RBFs) *)
+
+
+(** In this file, we prove some lemmas about request bound functions. *)
+
+
+(** ** RBF is a Bound on Workload *)
+
+(** First, we show that a task's RBF is indeed an upper bound on its
+ workload. *)
+Section ProofWorkloadBound.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+ Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+
+ (** ... and any ideal uniprocessor schedule of this arrival sequence.*)
+ Variable sched : schedule (ideal.processor_state Job).
+ Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
+
+ (** Consider an FP policy that indicates a higher-or-equal priority relation. *)
+ Variable higher_eq_priority : FP_policy Task.
+ Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.
+
+ (** Consider a task set ts... *)
+ Variable ts : list Task.
+
+ (** ...and let tsk be any task in ts. *)
+ Variable tsk : Task.
+ Hypothesis H_tsk_in_ts : tsk \in ts.
+
+ (** Assume that the job costs are no larger than the task costs. *)
+ Hypothesis H_job_cost_le_task_cost :
+ cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+ (** Next, we assume that all jobs come from the task set. *)
+ Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+ (** Let max_arrivals be any arrival bound for taskset ts. *)
+ Context `{MaxArrivals Task}.
+ Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
+
+ (** Let's define some local names for clarity. *)
+ Let task_rbf := task_request_bound_function tsk.
+ Let total_rbf := total_request_bound_function ts.
+ Let total_hep_rbf := total_hep_request_bound_function_FP higher_eq_priority ts tsk.
+ Let total_ohep_rbf := total_ohep_request_bound_function_FP higher_eq_priority ts tsk.
+
+ (** Next, we consider any job j of tsk. *)
+ Variable j : Job.
+ Hypothesis H_j_arrives : arrives_in arr_seq j.
+ Hypothesis H_job_of_tsk : job_task j = tsk.
+
+ (** Next, we say that two jobs j1 and j2 are in relation
+ other_higher_eq_priority, iff j1 has higher or equal priority than j2 and
+ is produced by a different task. *)
+ Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
+
+ (** Next, we recall the notions of total workload of jobs... *)
+ Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2).
+
+ (** ...notions of workload of higher or equal priority jobs... *)
+ Let total_hep_workload t1 t2 :=
+ workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2).
+
+ (** ... workload of other higher or equal priority jobs... *)
+ Let total_ohep_workload t1 t2 :=
+ workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2).
+
+ (** ... and the workload of jobs of the same task as job j. *)
+ Let task_workload t1 t2 :=
+ workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).
+
+ (** In this section we prove that the workload of any jobs is
+ no larger than the request bound function. *)
+ Section WorkloadIsBoundedByRBF.
+
+ (** Consider any time t and any interval of length delta. *)
+ Variable t : instant.
+ Variable delta : instant.
+
+ (** First, we show that workload of task tsk is bounded by the number of
+ arrivals of the task times the cost of the task. *)
+ Lemma task_workload_le_num_of_arrivals_times_cost:
+ task_workload t (t + delta)
+ <= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta).
+ Proof.
+ rewrite // /number_of_task_arrivals -sum1_size big_distrr /= big_filter.
+ rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs.
+ rewrite /same_task -H_job_of_tsk muln1.
+ apply leq_sum_seq; move => j0 IN0 /eqP EQ.
+ rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto.
+ by apply H_job_cost_le_task_cost.
+ Qed.
+
+ (** As a corollary, we prove that workload of task is no larger the than
+ task request bound function. *)
+ Corollary task_workload_le_task_rbf:
+ task_workload t (t + delta) <= task_rbf delta.
+ Proof.
+ apply leq_trans with
+ (task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta));
+ first by apply task_workload_le_num_of_arrivals_times_cost.
+ rewrite leq_mul2l; apply/orP; right.
+ rewrite -{2}[delta](addKn t).
+ by apply H_is_arrival_bound; last rewrite leq_addr.
+ Qed.
+
+ (** Next, we prove that total workload of other tasks with higher-or-equal
+ priority is no larger than the total request bound function. *)
+ Lemma total_workload_le_total_rbf:
+ total_ohep_workload t (t + delta) <= total_ohep_rbf delta.
+ Proof.
+ set l := arrivals_between arr_seq t (t + delta).
+ set hep := higher_eq_priority.
+ apply leq_trans with
+ (\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
+ (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
+ { intros.
+ rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
+ rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
+ have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk && (job_task x != tsk)).
+ rewrite EXCHANGE /=; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
+ rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
+ apply leq_sum; move => j0 /andP [IN0 HP0].
+ rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
+ by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
+ }
+ apply leq_sum_seq; intros tsk0 INtsk0 HP0.
+ apply leq_trans with
+ (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
+ { rewrite -sum1_size big_distrr /= big_filter.
+ rewrite /workload_of_jobs.
+ rewrite muln1 /l /arrivals_between /arrival_sequence.arrivals_between.
+ apply leq_sum_seq; move => j0 IN0 /eqP EQ.
+ by rewrite -EQ; apply H_job_cost_le_task_cost; apply in_arrivals_implies_arrived in IN0.
+ }
+ { rewrite leq_mul2l; apply/orP; right.
+ rewrite -{2}[delta](addKn t).
+ by apply H_is_arrival_bound; last rewrite leq_addr.
+ }
+ Qed.
+
+ (** Next, we prove that total workload of tasks with higher-or-equal
+ priority is no larger than the total request bound function. *)
+ Lemma total_workload_le_total_rbf':
+ total_hep_workload t (t + delta) <= total_hep_rbf delta.
+ Proof.
+ set l := arrivals_between arr_seq t (t + delta).
+ set hep := higher_eq_priority.
+ apply leq_trans with
+ (n := \sum_(tsk' <- ts | hep tsk' tsk)
+ (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
+ { rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.
+ have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk).
+ rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
+ rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
+ apply leq_sum; move => j0 /andP [IN0 HP0].
+ rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
+ by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
+ }
+ apply leq_sum_seq; intros tsk0 INtsk0 HP0.
+ apply leq_trans with
+ (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
+ { rewrite -sum1_size big_distrr /= big_filter.
+ rewrite -/l /workload_of_jobs.
+ rewrite muln1.
+ apply leq_sum_seq; move => j0 IN0 /eqP EQ.
+ rewrite -EQ.
+ apply H_job_cost_le_task_cost.
+ by apply in_arrivals_implies_arrived in IN0.
+ }
+ { rewrite leq_mul2l; apply/orP; right.
+ rewrite -{2}[delta](addKn t).
+ by apply H_is_arrival_bound; last rewrite leq_addr.
+ }
+ Qed.
+
+ (** Next, we prove that total workload of tasks is no larger than the total
+ request bound function. *)
+ Lemma total_workload_le_total_rbf'':
+ total_workload t (t + delta) <= total_rbf delta.
+ Proof.
+ set l := arrivals_between arr_seq t (t + delta).
+ apply leq_trans with
+ (n := \sum_(tsk' <- ts)
+ (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
+ { rewrite /total_workload.
+ have EXCHANGE := exchange_big_dep predT.
+ rewrite EXCHANGE /=; clear EXCHANGE; last by done.
+ rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
+ apply leq_sum; move => j0 /andP [IN0 HP0].
+ rewrite big_mkcond (big_rem (job_task j0)) /=.
+ rewrite eq_refl; apply leq_addr.
+ by apply in_arrivals_implies_arrived in IN0;
+ apply H_all_jobs_from_taskset.
+ }
+ apply leq_sum_seq; intros tsk0 INtsk0 HP0.
+ apply leq_trans with
+ (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
+ { rewrite -sum1_size big_distrr /= big_filter.
+ rewrite -/l /workload_of_jobs.
+ rewrite muln1.
+ apply leq_sum_seq; move => j0 IN0 /eqP EQ.
+ rewrite -EQ.
+ apply H_job_cost_le_task_cost.
+ by apply in_arrivals_implies_arrived in IN0.
+ }
+ { rewrite leq_mul2l; apply/orP; right.
+ rewrite -{2}[delta](addKn t).
+ by apply H_is_arrival_bound; last rewrite leq_addr.
+ }
+ Qed.
+
+ End WorkloadIsBoundedByRBF.
+
+End ProofWorkloadBound.
+
+(** ** RBF Properties *)
+(** In this section, we prove simple properties and identities of RBFs. *)
+Section RequestBoundFunctions.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobArrival Job}.
+
+ (** Consider any arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent:
+ consistent_arrival_times arr_seq.
+
+ (** Let tsk be any task. *)
+ Variable tsk : Task.
+
+ (** Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts
+ [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function
+ that equals 0 for the empty interval delta = 0. *)
+ Context `{MaxArrivals Task}.
+ Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
+ Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
+
+ (** Let's define some local names for clarity. *)
+ Let task_rbf := task_request_bound_function tsk.
+
+ (** We prove that [task_rbf 0] is equal to 0. *)
+ Lemma task_rbf_0_zero:
+ task_rbf 0 = 0.
+ Proof.
+ rewrite /task_rbf /task_request_bound_function.
+ apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.
+ by move: H_valid_arrival_curve => [T1 T2].
+ Qed.
+
+ (** We prove that task_rbf is monotone. *)
+ Lemma task_rbf_monotone:
+ monotone task_rbf leq.
+ Proof.
+ rewrite /monotone; intros ? ? LE.
+ rewrite /task_rbf /task_request_bound_function leq_mul2l.
+ apply/orP; right.
+ by move: H_valid_arrival_curve => [_ T]; apply T.
+ Qed.
+
+ (** Consider any job j of tsk. This guarantees that there exists at least one
+ job of task tsk. *)
+ Variable j : Job.
+ Hypothesis H_j_arrives : arrives_in arr_seq j.
+ Hypothesis H_job_of_tsk : job_task j = tsk.
+
+ (** Then we prove that task_rbf 1 is greater than or equal to task cost. *)
+ Lemma task_rbf_1_ge_task_cost:
+ task_rbf 1 >= task_cost tsk.
+ Proof.
+ have ALT: forall n, n = 0 \/ n > 0
+ by clear; intros n; destruct n; [left | right].
+ specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.
+ rewrite leqNgt; apply/negP; intros CONTR.
+ move: H_is_arrival_curve => ARRB.
+ specialize (ARRB (job_arrival j) (job_arrival j + 1)).
+ feed ARRB; first by rewrite leq_addr.
+ rewrite addKn in ARRB.
+ move: CONTR; rewrite /task_rbf /task_request_bound_function; move => CONTR.
+ move: CONTR; rewrite -{2}[task_cost tsk]muln1 ltn_mul2l; move => /andP [_ CONTR].
+ move: CONTR; rewrite -addn1 -{3}[1]add0n leq_add2r leqn0; move => /eqP CONTR.
+ move: ARRB; rewrite CONTR leqn0 eqn0Ngt; move => /negP T; apply: T.
+ rewrite /number_of_task_arrivals -has_predT.
+ rewrite /task_arrivals_between.
+ apply/hasP; exists j; last by done.
+ rewrite /arrivals_between addn1 big_nat_recl; last by done.
+ rewrite big_geq ?cats0; last by done.
+ rewrite mem_filter.
+ apply/andP; split.
+ - by apply/eqP.
+ - move: H_j_arrives => [t ARR].
+ move: (ARR) => CONS.
+ apply H_arrival_times_are_consistent in CONS.
+ by rewrite CONS.
+ Qed.
+
+End RequestBoundFunctions.
diff --git a/restructuring/analysis/facts/readiness/basic.v b/restructuring/analysis/facts/readiness/basic.v
index c10e406bb5320b6f51eb5635aee3c80d6edd2799..29eb01ede9a7984ec12dd96e10d2a551e5f77036 100644
--- a/restructuring/analysis/facts/readiness/basic.v
+++ b/restructuring/analysis/facts/readiness/basic.v
@@ -1,4 +1,4 @@
-Require Import rt.restructuring.analysis.basic_facts.completion.
+Require Import rt.restructuring.analysis.facts.behavior.completion.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/facts/transform/edf_opt.v
similarity index 99%
rename from restructuring/analysis/transform/facts/edf_opt.v
rename to restructuring/analysis/facts/transform/edf_opt.v
index 1be7c88f964b2e54d5db8d7739cfdd017f971f1c..2536c0ca6c8fbe5809c7a3c77395e8ca38aad628 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/facts/transform/edf_opt.v
@@ -1,8 +1,8 @@
From mathcomp Require Import ssrnat ssrbool fintype.
Require Export rt.restructuring.model.schedule.edf.
-Require Export rt.restructuring.analysis.schedulability.
+Require Export rt.restructuring.analysis.concepts.schedulability.
Require Export rt.restructuring.analysis.transform.edf_trans.
-Require Export rt.restructuring.analysis.transform.facts.swaps.
+Require Export rt.restructuring.analysis.facts.transform.swaps.
Require Export rt.restructuring.analysis.facts.readiness.basic.
(** This file contains the main argument of the EDF optimality proof,
diff --git a/restructuring/analysis/transform/facts/replace_at.v b/restructuring/analysis/facts/transform/replace_at.v
similarity index 98%
rename from restructuring/analysis/transform/facts/replace_at.v
rename to restructuring/analysis/facts/transform/replace_at.v
index 5e22b2dfee24d5e0db8587a0225502aaa6f591de..20a2fe23bf116e90f4b162f7ca432843ba23780a 100644
--- a/restructuring/analysis/transform/facts/replace_at.v
+++ b/restructuring/analysis/facts/transform/replace_at.v
@@ -1,4 +1,5 @@
Require Export rt.restructuring.analysis.transform.swap.
+Require Export rt.restructuring.analysis.facts.behavior.completion.
(** In this file, we make a few simple observations about schedules with
replacements. *)
diff --git a/restructuring/analysis/transform/facts/swaps.v b/restructuring/analysis/facts/transform/swaps.v
similarity index 99%
rename from restructuring/analysis/transform/facts/swaps.v
rename to restructuring/analysis/facts/transform/swaps.v
index d59d6035c3d84be426919ecdb21cd1965b2b3d92..7529e887a2c4adf55829d172485478a497dc6519 100644
--- a/restructuring/analysis/transform/facts/swaps.v
+++ b/restructuring/analysis/facts/transform/swaps.v
@@ -1,4 +1,5 @@
-Require Export rt.restructuring.analysis.transform.facts.replace_at.
+Require Export rt.restructuring.analysis.facts.transform.replace_at.
+Require Export rt.restructuring.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
diff --git a/restructuring/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index 288b202d8884478db2adc3b95715834e6c575a96..90e5ee75d71704bed5db777a99bc0b3bc3f52c2c 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -1,5 +1,5 @@
From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.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
diff --git a/restructuring/analysis/transform/swap.v b/restructuring/analysis/transform/swap.v
index 96dc092d24c9975ebfb64cb766ba76749ec20296..443aa3987a10bb41c3f1b2942449be7278ca86b1 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.behavior.all.
(** This file defines simple allocation substitutions and a swapping operation
as used for instance in the classic EDF optimality proof. *)
diff --git a/restructuring/analysis/edf/optimality.v b/restructuring/results/edf/optimality.v
similarity index 98%
rename from restructuring/analysis/edf/optimality.v
rename to restructuring/results/edf/optimality.v
index 121c124f0a96fe23384a2c67555036434a0e80fc..619b70358121065d3d0811aeaba69b0d761d2773 100644
--- a/restructuring/analysis/edf/optimality.v
+++ b/restructuring/results/edf/optimality.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.analysis.transform.facts.edf_opt.
+Require Export rt.restructuring.analysis.facts.transform.edf_opt.
(** This file contains the theorem that states the famous EDF
optimality result: if there is any way to meet all deadlines
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/results/edf/rta/bounded_nps.v
similarity index 99%
rename from restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
rename to restructuring/results/edf/rta/bounded_nps.v
index 6c59465f208da3fc317590b11ccfbb4827daecea..2b49af5b437f2db3551f83deb7a347d2bc0e4577 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/results/edf/rta/bounded_nps.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
-Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
-Require Export rt.restructuring.analysis.arrival.rbf.
+Require Export rt.restructuring.analysis.facts.priority_inversion.
+Require Export rt.restructuring.results.edf.rta.bounded_pi.
+Require Export rt.restructuring.analysis.facts.rbf.
Require Import rt.restructuring.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/results/edf/rta/bounded_pi.v
similarity index 98%
rename from restructuring/analysis/edf/rta/response_time_bound.v
rename to restructuring/results/edf/rta/bounded_pi.v
index fda9c51b8b3bec439b442c0ad580f62cc2e921c4..50b5a53ff680ad94164d1132a86473dad8189750 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/results/edf/rta/bounded_pi.v
@@ -1,10 +1,11 @@
Require Export rt.restructuring.analysis.facts.edf.
Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
-Require Export rt.restructuring.analysis.schedulability.
+Require Export rt.restructuring.analysis.facts.priority_inversion.
+Require Export rt.restructuring.analysis.facts.carry_in.
+Require Export rt.restructuring.analysis.concepts.schedulability.
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.model.task.absolute_deadline.
-Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+Require Import rt.restructuring.analysis.abstract.ideal_jlfp_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
@@ -195,13 +196,13 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** We say that job j incurs interference at time t iff it cannot execute due to
a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion. *)
Let interference (j : Job) (t : instant) :=
- ideal_processor.interference sched EDF j t.
+ ideal_jlfp_rta.interference sched EDF j t.
(** Instantiation of Interfering Workload *)
(** The interfering workload, in turn, is defined as the sum of the priority inversion
function and interfering workload of jobs with higher or equal priority. *)
Let interfering_workload (j : Job) (t : instant) :=
- ideal_processor.interfering_workload arr_seq sched EDF j t.
+ ideal_jlfp_rta.interfering_workload arr_seq sched EDF j t.
(** Finally, we define the interference bound function as the sum of the priority
interference bound and the higher-or-equal-priority workload. *)
@@ -242,7 +243,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
}
}
{ apply/negP;
- rewrite /interference /ideal_processor.interference /is_priority_inversion
+ rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
/is_interference_from_another_hep_job
HYP negb_or; apply/andP; split.
- by rewrite Bool.negb_involutive /edf.EDF.
@@ -608,7 +609,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** Next, consider any A from the search space (in abstract sense). *)
Variable A : duration.
Hypothesis H_A_is_in_abstract_search_space:
- reduction_of_search_space.is_in_search_space tsk L total_interference_bound A.
+ search_space.is_in_search_space tsk L total_interference_bound A.
(** We prove that A is also in the concrete search space. *)
Lemma A_is_in_concrete_search_space:
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/results/edf/rta/floating_nonpreemptive.v
similarity index 97%
rename from restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
rename to restructuring/results/edf/rta/floating_nonpreemptive.v
index 693cb2e7ee765af3df85fcd1a994994a0ec8d157..9ef9185f94efb4d192e5beec4c09d7ea5d998949 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/results/edf/rta/floating_nonpreemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+Require Export rt.restructuring.results.edf.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating.
Require Import rt.restructuring.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/results/edf/rta/fully_nonpreemptive.v
similarity index 96%
rename from restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
rename to restructuring/results/edf/rta/fully_nonpreemptive.v
index e72bc1c60c338062d5518e771d657de3b88e9506..551691c93f5a7287dc43ef4d8c98fa6efca5d10d 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/results/edf/rta/fully_nonpreemptive.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
+Require Export rt.restructuring.results.edf.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.task.nonpreemptive.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreemptive.
Require Import rt.restructuring.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/results/edf/rta/fully_preemptive.v
similarity index 96%
rename from restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
rename to restructuring/results/edf/rta/fully_preemptive.v
index 07c5ebf84182b63b0806682dcac005c78458d321..e0c91fd412a7621da72dcd7d27689eb2e18ce04e 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/results/edf/rta/fully_preemptive.v
@@ -1,6 +1,6 @@
-Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
+Require Import rt.restructuring.results.edf.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.task.preemptive.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preemptive.
Require Import rt.restructuring.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/results/edf/rta/limited_preemptive.v
similarity index 98%
rename from restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
rename to restructuring/results/edf/rta/limited_preemptive.v
index 1b646474b50bce71dfed74a705e765b093694709..637feff567571cfcd4834d0f08a524852edc0ac9 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/results/edf/rta/limited_preemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+Require Export rt.restructuring.results.edf.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
Require Import rt.restructuring.model.priority.edf.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/results/fixed_priority/rta/bounded_nps.v
similarity index 97%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
rename to restructuring/results/fixed_priority/rta/bounded_nps.v
index 6f39f334dadf53fcdf410435d29227d5014ca2d7..8ee2c95889e242a26cf117c1be1c00b08383d7bc 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/results/fixed_priority/rta/bounded_nps.v
@@ -1,7 +1,7 @@
-Require Export rt.restructuring.analysis.schedulability.
-Require Export rt.restructuring.analysis.arrival.workload_bound.
-Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
-Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
+Require Export rt.restructuring.analysis.concepts.schedulability.
+Require Export rt.restructuring.analysis.concepts.request_bound_function.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_pi.
+Require Export rt.restructuring.analysis.facts.priority_inversion.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
@@ -139,7 +139,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Proof.
intros j t ARR TSK.
rewrite /max_length_of_priority_inversion /blocking_bound /FP_to_JLFP
- /priority_inversion_is_bounded.max_length_of_priority_inversion.
+ /priority_inversion.max_length_of_priority_inversion.
apply leq_trans with
(\max_(j_lp <- arrivals_between arr_seq 0 t
| ~~ higher_eq_priority (job_task j_lp) tsk)
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/results/fixed_priority/rta/bounded_pi.v
similarity index 97%
rename from restructuring/analysis/fixed_priority/rta/response_time_bound.v
rename to restructuring/results/fixed_priority/rta/bounded_pi.v
index 3d2122480a364ee8d48d143d6db53e91d0e67c4a..b095665288bf4d0ac5158760c6c9c0452968155b 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/results/fixed_priority/rta/bounded_pi.v
@@ -1,6 +1,6 @@
Require Export rt.restructuring.model.schedule.priority_driven.
-Require Export rt.restructuring.analysis.facts.busy_interval_exists.
-Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+Require Export rt.restructuring.analysis.facts.busy_interval.
+Require Import rt.restructuring.analysis.abstract.ideal_jlfp_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
@@ -164,14 +164,14 @@ Section AbstractRTAforFPwithArrivalCurves.
(** We say that job j incurs interference at time t iff it cannot execute due to
a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion. *)
Let interference (j : Job) (t : instant) :=
- ideal_processor.interference sched hep_job j t.
+ ideal_jlfp_rta.interference sched hep_job j t.
(** Instantiation of Interfering Workload *)
(** The interfering workload, in turn, is defined as the sum of the
priority inversion function and interfering workload of jobs
with higher or equal priority. *)
Let interfering_workload (j : Job) (t : instant) :=
- ideal_processor.interfering_workload
+ ideal_jlfp_rta.interfering_workload
arr_seq sched (@FP_to_JLFP Job Task H1 higher_eq_priority) j t.
(** Finally, we define the interference bound function as the sum of the priority
@@ -205,7 +205,7 @@ Section AbstractRTAforFPwithArrivalCurves.
by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle;
eauto 2 using eqprop_to_eqbool.
- move: (HYP); rewrite scheduled_at_def; move => /eqP HYP2; apply/negP.
- rewrite /interference /ideal_processor.interference /is_priority_inversion
+ rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
/is_interference_from_another_hep_job HYP2 negb_or.
apply/andP; split.
+ rewrite Bool.negb_involutive; eauto 2.
@@ -317,7 +317,7 @@ Section AbstractRTAforFPwithArrivalCurves.
(** Next, consider any A from the search space (in the abstract sence). *)
Variable A : duration.
Hypothesis H_A_is_in_abstract_search_space :
- reduction_of_search_space.is_in_search_space tsk L total_interference_bound A.
+ search_space.is_in_search_space tsk L total_interference_bound A.
(** We prove that A is also in the concrete search space. *)
Lemma A_is_in_concrete_search_space:
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
similarity index 97%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
rename to restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
index 6b9a836ac0dc30f258051e174906a3d5be9a35fa..fdd53ef23225271f26b7a7460a9cae0b641f257a 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
similarity index 95%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
rename to restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
index 853e69903d2ba46a098e375020187f92eca56842..67e67c4cd072dc7731b847f3e517548054d12871 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.task.nonpreemptive.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/results/fixed_priority/rta/fully_preemptive.v
similarity index 95%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
rename to restructuring/results/fixed_priority/rta/fully_preemptive.v
index b67faa581ec39bdafb6e1ec353185b6d7f637004..31d333f37bf211d2aa59ad076f9a31e8da2290ec 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_preemptive.v
@@ -1,6 +1,6 @@
-Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.task.preemptive.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/results/fixed_priority/rta/limited_preemptive.v
similarity index 97%
rename from restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
rename to restructuring/results/fixed_priority/rta/limited_preemptive.v
index 7ce643664c90421f168addf7e1d36b8e07677061..867d8f6f3deb0604055c7c0cc6e0ddf624965474 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/results/fixed_priority/rta/limited_preemptive.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
-Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+Require Export rt.restructuring.results.fixed_priority.rta.bounded_nps.
+Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)