restructuring/analysis/basic_facts/arrivals.v

 Require Export rt.restructuring.behavior.all.
-Require Import rt.util.all.
+Require Export rt.util.all.
 
 (** In this section, we relate job readiness to [has_arrived]. *)
 Section Arrived.

restructuring/analysis/basic_facts/completion.v

@@ -2,7 +2,7 @@ Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.analysis.basic_facts.service.
 Require Export rt.restructuring.analysis.basic_facts.arrivals.
 
-Require Import rt.util.nat.
+Require Export rt.util.nat.
 
 (** In this file, we establish basic facts about job completions. *)
 

restructuring/analysis/edf/optimality.v

-Require Export rt.restructuring.model.schedule.edf.
-Require Import rt.restructuring.analysis.schedulability.
-Require Import rt.restructuring.analysis.transform.facts.edf_opt.
+Require Export rt.restructuring.analysis.transform.facts.edf_opt.
 
 (** This file contains the theorem that states the famous EDF
     optimality result: if there is any way to meet all deadlines
@@ -8,10 +6,10 @@ Require Import rt.restructuring.analysis.transform.facts.edf_opt.
     schedule in which all deadlines are met. *)
 
 (** The following results assume ideal uniprocessor schedules... *)
-From rt.restructuring.model.processor Require ideal.
+Require rt.restructuring.model.processor.ideal.
 (** ... and the basic (i.e., Liu & Layland) readiness model under which any
     pending job is ready. *)
-From rt.restructuring.model.readiness Require basic.
+Require rt.restructuring.model.readiness.basic.
 
 Section Optimality.
   (** For any given type of jobs... *)

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v

@@ -15,6 +15,11 @@ Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+
+Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v

@@ -15,6 +15,9 @@ Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v

@@ -14,6 +14,9 @@ Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
 
 (** Assume we have a fully non-preemptive model. *)
 Require Import rt.restructuring.model.preemption.nonpreemptive.

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v

@@ -14,6 +14,9 @@ Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
 
 (** Assume we have a fully preemptive model. *)
 Require Import rt.restructuring.model.preemption.preemptive.

restructuring/analysis/facts/priority_inversion_is_bounded.v

@@ -18,6 +18,72 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     pending jobs are always ready. *)
 Require Import rt.restructuring.model.readiness.basic.
 
+(** In preparation of the derivation of the priority inversion bound, we
+    establish two basic facts on preemption times. *)
+Section PreemptionTimes.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** In addition, we assume the existence of a function mapping a
+      task to its maximal non-preemptive segment ... *)
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** ... and the existence of a function mapping a job and
+      its progress to a boolean value saying whether this job is
+      preemptable at its current point of execution. *)
+  Context `{JobPreemptable Job}.
+
+  (** Consider any arrival sequence with consistent arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+
+  (** Next, consider 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 a valid model with bounded nonpreemptive segments. *)
+  Hypothesis H_model_with_bounded_nonpreemptive_segments:
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Then, we show that time 0 is a preemption time. *)
+  Lemma zero_is_pt: preemption_time sched 0.
+  Proof.
+    unfold preemption_time.
+    case SCHED: (sched 0) => [j | ]; last by done.
+    move: (SCHED) => /eqP; rewrite -scheduled_at_def; move => ARR.
+    apply H_jobs_come_from_arrival_sequence in ARR.
+    rewrite /service /service_during big_geq; last by done.
+    destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
+    by move: (T1 j ARR) => [PP _].
+  Qed.
+
+  (** Also, we show that the first instant of execution is a preemption time. *)
+  Lemma first_moment_is_pt:
+    forall j prt,
+      arrives_in arr_seq j ->
+      ~~ scheduled_at sched j prt ->
+      scheduled_at sched j prt.+1 ->
+      preemption_time sched prt.+1.
+  Proof.
+    intros s pt ARR NSCHED SCHED.
+    unfold preemption_time.
+    move: (SCHED); rewrite scheduled_at_def; move => /eqP SCHED2; rewrite SCHED2; clear SCHED2.
+    destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
+    by move: (T1 s ARR) => [_ [_ [_ P]]]; apply P.
+  Qed.
+
+End PreemptionTimes.
+
 (** * Priority inversion is bounded *)
 (** In this module we prove that any priority inversion that occurs in the model with bounded 
     nonpreemptive segments defined in module rt.model.schedule.uni.limited.platform.definitions 

restructuring/analysis/facts/readiness/basic.v

+Require Export rt.restructuring.model.readiness.basic.
+Require Import rt.restructuring.analysis.basic_facts.completion.
+
+Section LiuAndLaylandReadiness.
+  (** Consider any kind of jobs... *)
+  Context {Job : JobType}.
+
+  (** ... and any kind of processor state. *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** Supose jobs have an arrival time and a cost. *)
+  Context `{JobArrival Job} `{JobCost Job}.
+
+  (** In the basic Liu & Layland model, a schedule satisfies that only ready 
+      jobs execute as long as jobs must arrive to execute and completed jobs
+      don't execute, which we note with the following theorem. *)
+  Lemma basic_readiness_compliance:
+    forall sched,
+      jobs_must_arrive_to_execute sched ->
+      completed_jobs_dont_execute sched ->
+      jobs_must_be_ready_to_execute sched.
+  Proof.
+    move=> sched ARR COMP.
+    rewrite /jobs_must_be_ready_to_execute =>  j t SCHED.
+    rewrite /job_ready /basic_ready_instance /pending.
+    apply /andP; split.
+    - by apply ARR.
+    - rewrite -less_service_than_cost_is_incomplete.
+      by apply COMP.
+  Qed.
+
+End LiuAndLaylandReadiness.

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v

@@ -14,6 +14,10 @@ Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v

@@ -14,6 +14,9 @@ Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.limited.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.limited.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v

@@ -13,6 +13,9 @@ Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
 
 (** Assume we have a fully non-preemptive model. *)
 Require Import rt.restructuring.model.preemption.nonpreemptive.

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v

@@ -13,6 +13,9 @@ Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
+Require Export rt.restructuring.analysis.basic_facts.preemption.job.preemptive.
+Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
+Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
 
 (** Assume we have a fully preemptive model. *)
 Require Import rt.restructuring.model.preemption.preemptive.

restructuring/analysis/schedulability.v

-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.job_deadline.
 Require Export rt.restructuring.analysis.basic_facts.completion.
-Require Export rt.util.seqset.
 
 Section Task.
   Context {Task : TaskType}.

restructuring/analysis/task_schedule.v

-Require Import rt.restructuring.model.task.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 

restructuring/analysis/transform/edf_trans.v

 Require Export rt.restructuring.analysis.transform.prefix.
 Require Export rt.restructuring.analysis.transform.swap.
-Require Export rt.util.search_arg.
 
 (** In this file we define the "EDF-ification" of a schedule, the
     operation at the core of the EDF optimality proof. *)

restructuring/analysis/transform/facts/edf_opt.v

 From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.schedule.edf.
 Require Export rt.restructuring.analysis.schedulability.
 Require Export rt.restructuring.analysis.transform.edf_trans.
 Require Export rt.restructuring.analysis.transform.facts.swaps.
-
-Require Import rt.util.tactics.
-Require Import rt.util.nat.
+Require Export rt.restructuring.analysis.facts.readiness.basic.
 
 (** This file contains the main argument of the EDF optimality proof,
     starting with an analysis of the individual functions that drive

restructuring/analysis/transform/facts/replace_at.v

 Require Export rt.restructuring.analysis.transform.swap.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.util.nat.
 
 (** In this file, we make a few simple observations about schedules with
     replacements. *)

restructuring/analysis/transform/prefix.v

 From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.basic_facts.all.
 
 (** This file provides an operation that transforms a finite prefix of
     a given schedule by applying a point-wise transformation to each

restructuring/analysis/transform/swap.v

-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.basic_facts.all.
 
 (** This file defines simple allocation substitutions and a swapping operation
     as used for instance in the classic EDF optimality proof. *)