import and comment tweaks in results & analysis

analysis/facts/preemption/rtc_threshold/floating.v

@@ -7,9 +7,6 @@ Require Export prosa.model.task.preemption.floating_nonpreemptive.
     threshold] for the model with floating non-preemptive regions. *)
 Section TaskRTCThresholdFloatingNonPreemptiveRegions.
 
-  (** Furthermore, we assume the task model with floating non-preemptive regions. *)
-  #[local] Existing Instance floating_preemptive_rtc_threshold.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -19,7 +16,10 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
   Context `{JobTask Job Task}.
   Context `{JobCost Job}.
   Context `{JobPreemptable Job}.
-  
+
+  (** We assume a task model with floating non-preemptive regions. *)
+  #[local] Existing Instance floating_preemptive_rtc_threshold.
+
   (** Consider any arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
 

analysis/facts/preemption/rtc_threshold/limited.v

 Require Export prosa.analysis.facts.preemption.task.limited.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
-Require Import prosa.model.task.preemption.limited_preemptive.
-
-(** Furthermore, we assume the task model with fixed preemption points. *)
-Require Import prosa.model.preemption.limited_preemptive.
+Require Export prosa.model.task.preemption.limited_preemptive.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we prove that instantiation of function [task run
@@ -11,10 +8,6 @@ Require Import prosa.model.preemption.limited_preemptive.
     indeed defines a valid run-to-completion threshold function. *)
 Section TaskRTCThresholdLimitedPreemptions.
 
-  (** We assume the task model with fixed preemption points. *)
-  #[local] Existing Instance limited_preemptive_job_model.
-  #[local] Existing Instance limited_preemptions_rtc_threshold.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -26,6 +19,10 @@ Section TaskRTCThresholdLimitedPreemptions.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
   Context `{JobPreemptionPoints Job}.
+
+  (** We assume a task model with fixed preemption points. *)
+  #[local] Existing Instance limited_preemptive_job_model.
+  #[local] Existing Instance limited_preemptions_rtc_threshold.
   
   (** Consider any arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.

analysis/facts/preemption/rtc_threshold/nonpreemptive.v

 Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
-Require Import prosa.model.preemption.fully_nonpreemptive.
-Require Import prosa.model.task.preemption.fully_nonpreemptive.
+Require Export prosa.model.task.preemption.fully_nonpreemptive.
  
 (** * Task's Run to Completion Threshold *)
 (** In this section, we prove that instantiation of function [task run
@@ -8,11 +7,6 @@ Require Import prosa.model.task.preemption.fully_nonpreemptive.
     indeed defines a valid run-to-completion threshold function. *)
 Section TaskRTCThresholdFullyNonPreemptive.
 
-  (** We assume the fully non-preemptive task model. *)
-  #[local] Existing Instance fully_nonpreemptive_job_model.
-  #[local] Existing Instance fully_nonpreemptive_task_model.
-  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
-  
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}. 
   Context `{TaskCost Task}.
@@ -22,6 +16,11 @@ Section TaskRTCThresholdFullyNonPreemptive.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
+
+  (** We assume a fully non-preemptive task model. *)
+  #[local] Existing Instance fully_nonpreemptive_job_model.
+  #[local] Existing Instance fully_nonpreemptive_task_model.
+  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
   
   (** Consider any arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.

analysis/facts/preemption/rtc_threshold/preemptive.v

-(** Furthermore, we assume the fully preemptive task model. *)
-Require Import prosa.model.preemption.fully_preemptive.
-Require Import prosa.model.task.preemption.fully_preemptive.
-Require Import prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export prosa.model.preemption.fully_preemptive.
+Require Export prosa.model.task.preemption.fully_preemptive.
 
 (** * Task's Run to Completion Threshold *)
-(** In this section, we prove that instantiation of function [task run
-    to completion threshold] to the fully preemptive model
-    indeed defines a valid run-to-completion threshold function. *)
-Section TaskRTCThresholdFullyPreemptiveModel.
 
-  (** We assume that jobs and tasks are fully preemptive. *)
-  #[local] Existing Instance fully_preemptive_job_model.
-  #[local] Existing Instance fully_preemptive_task_model.
-  #[local] Existing Instance fully_preemptive_rtc_threshold.
+(** In this section, we prove that the instantiation of the task
+    run-to-completion threshold for the fully preemptive model is valid. *)
+Section TaskRTCThresholdFullyPreemptiveModel.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
@@ -22,7 +16,12 @@ Section TaskRTCThresholdFullyPreemptiveModel.
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
   Context `{JobCost Job}.
-  
+
+  (** Assume that jobs and tasks are fully preemptive. *)
+  #[local] Existing Instance fully_preemptive_job_model.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.  
+
   (** Next, consider any arrival sequence ... *)
   Variable arr_seq : arrival_sequence Job.
 

analysis/facts/preemption/task/floating.v

 Require Export prosa.analysis.facts.preemption.job.limited.
-Require Import prosa.model.task.preemption.floating_nonpreemptive.
-Require Import prosa.model.preemption.limited_preemptive.
-
+Require Export prosa.model.task.preemption.floating_nonpreemptive.
+Require Export prosa.model.preemption.limited_preemptive.
 
 (** * Platform for Floating Non-Preemptive Regions Model *)
+
 (** In this section, we prove that instantiation of functions
-    [job_preemptable and task_max_nonpreemptive_segment] to the model
+    [job_preemptable] and [task_max_nonpreemptive_segment] for the model
     with floating non-preemptive regions indeed defines a valid
     preemption model with bounded non-preemptive regions. *)
 Section FloatingNonPreemptiveRegionsModel.

analysis/facts/preemption/task/nonpreemptive.v

 Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
-Require Import prosa.model.preemption.fully_nonpreemptive.
-Require Import prosa.model.task.preemption.fully_nonpreemptive.
+Require Export prosa.model.task.preemption.fully_nonpreemptive.
 
 (** * Platform for Fully Non-Preemptive Model *)
+
 (** In this section, we prove that instantiation of functions
-    [job_preemptable and task_max_nonpreemptive_segment] to the fully
+    [job_preemptable] and [task_max_nonpreemptive_segment] to the fully
     non-preemptive model indeed defines a valid preemption model with
     bounded non-preemptive regions. *)
 Section FullyNonPreemptiveModel.
 
-  (** We assume the fully non-preemptive task model. *)
-  #[local] Existing Instance fully_nonpreemptive_job_model.  
-  #[local] Existing Instance fully_nonpreemptive_task_model.
-  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -24,6 +19,11 @@ Section FullyNonPreemptiveModel.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
+  (** Assume a fully non-preemptive task model. *)
+  #[local] Existing Instance fully_nonpreemptive_job_model.  
+  #[local] Existing Instance fully_nonpreemptive_task_model.
+  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
+
   (** Consider any arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
@@ -40,7 +40,7 @@ Section FullyNonPreemptiveModel.
   Hypothesis H_valid_job_cost:
     arrivals_have_valid_job_costs arr_seq.
 
-  (** Then we prove that [fully_nonpreemptive_model] function
+  (** Then we prove that the [fully_nonpreemptive_model] function
       defines a model with bounded non-preemptive regions.*) 
   Lemma fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions: 
     model_with_bounded_nonpreemptive_segments arr_seq.

analysis/facts/preemption/task/preemptive.v

-Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.analysis.facts.preemption.job.preemptive.
-Require Import prosa.model.task.preemption.fully_preemptive.
+Require Export prosa.model.task.preemption.fully_preemptive.
 
 (** * Platform for Fully Preemptive Model *)
-(** In this section, we prove that instantiation of functions
-    [job_preemptable and task_max_nonpreemptive_segment] to the fully
+
+(** In this section, we prove that the instantiations of the functions
+    [job_preemptable] and [task_max_nonpreemptive_segment] for the fully
     preemptive model indeed defines a valid preemption model with
     bounded non-preemptive regions. *)
 Section FullyPreemptiveModel.
 
-  (** We assume that jobs and tasks are fully preemptive. *)
-  #[local] Existing Instance fully_preemptive_job_model.
-  #[local] Existing Instance fully_preemptive_task_model.
-  #[local] Existing Instance fully_preemptive_rtc_threshold.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -24,6 +19,11 @@ Section FullyPreemptiveModel.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
+  (** Assume that jobs and tasks are fully preemptive. *)
+  #[local] Existing Instance fully_preemptive_job_model.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
+
   (** Consider any kind of processor state model, ... *)
   Context {PState : ProcessorState Job}.
 
@@ -33,7 +33,7 @@ Section FullyPreemptiveModel.
   (** ... and any given schedule. *)
   Variable sched : schedule PState.
 
-  (** We prove that [fully_preemptive_model] function
+  (** We prove that the [fully_preemptive_model] function
       defines a model with bounded non-preemptive regions.*)
   Lemma fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions:
     model_with_bounded_nonpreemptive_segments arr_seq.

results/edf/optimality.v

@@ -3,6 +3,7 @@ Require Import prosa.model.preemption.fully_preemptive.
 Require Export prosa.analysis.facts.transform.edf_opt.
 Require Export prosa.analysis.facts.transform.edf_wc.
 Require Export prosa.analysis.facts.edf_definitions.
+Require prosa.model.priority.edf.
 
 (** * Optimality of EDF on Ideal Uniprocessors *)
 
@@ -11,13 +12,18 @@ Require Export prosa.analysis.facts.edf_definitions.
     schedule), then there is also an (ideal) EDF schedule in which all
     deadlines are met. *)
 
-(** The following results assume the EDF priority policy, ... *)
-Require prosa.model.priority.edf.
-
 (** ** Optimality Theorem *)
 
 Section Optimality.
 
+  (** Consider any given type of jobs, each characterized by execution
+      costs, an arrival time, and an absolute deadline,... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (** ... and any valid arrival sequence of such jobs. *)
+  Variable arr_seq: arrival_sequence Job.
+  Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
+
   (** We assume the classic (i.e., Liu & Layland) model of readiness
       without jitter or self-suspensions, wherein pending jobs are
       always ready. *)
@@ -26,18 +32,9 @@ Section Optimality.
   (** We assume that jobs are fully preemptive. *)
   #[local] Existing Instance fully_preemptive_job_model.
 
-  (** For any given type of jobs, each characterized by execution
-      costs, an arrival time, and an absolute deadline,... *)
-  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
-
-  (** ... and any valid job arrival sequence. *)
-  Variable arr_seq: arrival_sequence Job.
-  Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
-
-  (** We observe that EDF is optimal in the sense that, if there exists
-     any schedule in which all jobs of [arr_seq] meet their deadline,
-     then there also exists an EDF schedule in which all deadlines are
-     met. *)
+  (** Under these assumptions, EDF is optimal in the sense that, if there
+      exists any schedule in which all jobs of [arr_seq] meet their deadline,
+      then there also exists an EDF schedule in which all deadlines are met. *)
   Theorem EDF_optimality:
     (exists any_sched : schedule (ideal.processor_state Job),
         valid_schedule any_sched arr_seq /\

results/edf/rta/bounded_nps.v

@@ -20,11 +20,6 @@ Require Export prosa.analysis.facts.busy_interval.priority_inversion.
     RTA for EDF-schedulers is applicable to this instantiation. *)
 Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
 
-  (** We assume the classic (i.e., Liu & Layland) model of readiness
-      without jitter or self-suspensions, wherein pending jobs are
-      always ready. *)
-  #[local] Existing Instance basic_ready_instance.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -38,6 +33,11 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Context `{Arrival : JobArrival Job}.
   Context `{Cost : JobCost Job}.
 
+  (** We assume the classic (i.e., Liu & Layland) model of readiness
+      without jitter or self-suspensions, wherein pending jobs are
+      always ready. *)
+  #[local] Existing Instance basic_ready_instance.
+
   (** For clarity, let's denote the relative deadline of a task as [D]. *)
   Let D tsk := task_deadline tsk.
 

results/edf/rta/bounded_pi.v

@@ -29,11 +29,6 @@ Require Import prosa.analysis.facts.readiness.basic.
 
 Section AbstractRTAforEDFwithArrivalCurves.
 
-  (** We assume the classic (i.e., Liu & Layland) model of readiness
-      without jitter or self-suspensions, wherein pending jobs are
-      always ready. *)
-  #[local] Existing Instance basic_ready_instance.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -47,6 +42,11 @@ Section AbstractRTAforEDFwithArrivalCurves.
   Context {Cost : JobCost Job}.
   Context `{JobPreemptable Job}. 
   
+  (** We assume the classic (i.e., Liu & Layland) model of readiness
+      without jitter or self-suspensions, wherein pending jobs are
+      always ready. *)
+  #[local] Existing Instance basic_ready_instance.
+
   (** For clarity, let's denote the relative deadline of a task as D. *)
   Let D tsk := task_deadline tsk.
   

results/edf/rta/floating_nonpreemptive.v

@@ -13,11 +13,6 @@ Require Import prosa.model.priority.edf.
 
 Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   
-  (** We assume the classic (i.e., Liu & Layland) model of readiness
-      without jitter or self-suspensions, wherein pending jobs are
-      always ready. *)
-  #[local] Existing Instance basic_ready_instance.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -29,6 +24,11 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
+  (** We assume the classic (i.e., Liu & Layland) model of readiness
+      without jitter or self-suspensions, wherein pending jobs are
+      always ready. *)
+  #[local] Existing Instance basic_ready_instance.
+
   (** We assume that jobs are limited-preemptive. *)
   #[local] Existing Instance limited_preemptive_job_model.
   

results/edf/rta/fully_nonpreemptive.v

@@ -15,11 +15,6 @@ Require Import prosa.model.priority.edf.
 
 Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   
-  (** We assume the classic (i.e., Liu & Layland) model of readiness
-      without jitter or self-suspensions, wherein pending jobs are
-      always ready. *)
-  #[local] Existing Instance basic_ready_instance.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -31,6 +26,11 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
+  (** We assume the classic (i.e., Liu & Layland) model of readiness
+      without jitter or self-suspensions, wherein pending jobs are
+      always ready. *)
+  #[local] Existing Instance basic_ready_instance.
+
   (** We assume that jobs and tasks are fully nonpreemptive. *)
   #[local] Existing Instance fully_nonpreemptive_job_model.
   #[local] Existing Instance fully_nonpreemptive_task_model.

results/edf/rta/fully_preemptive.v

@@ -15,11 +15,6 @@ Require Import prosa.model.priority.edf.
 
 Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
 
-  (** We assume the classic (i.e., Liu & Layland) model of readiness
-      without jitter or self-suspensions, wherein pending jobs are
-      always ready. *)
-  #[local] Existing Instance basic_ready_instance.
-
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance fully_preemptive_job_model.
   #[local] Existing Instance fully_preemptive_task_model.
@@ -36,6 +31,11 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
+  (** We assume the classic (i.e., Liu & Layland) model of readiness
+      without jitter or self-suspensions, wherein pending jobs are
+      always ready. *)
+  #[local] Existing Instance basic_ready_instance.
+
   (** 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.

results/edf/rta/limited_preemptive.v

@@ -15,11 +15,6 @@ Require Export prosa.model.priority.edf.
 
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   
-  (** We assume the classic (i.e., Liu & Layland) model of readiness
-      without jitter or self-suspensions, wherein pending jobs are
-      always ready. *)
-  #[local] Existing Instance basic_ready_instance.
-
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
@@ -31,6 +26,11 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
+  (** We assume the classic (i.e., Liu & Layland) model of readiness
+      without jitter or self-suspensions, wherein pending jobs are
+      always ready. *)
+  #[local] Existing Instance basic_ready_instance.
+
   (** We assume that jobs are limited-preemptive. *)
   #[local] Existing Instance limited_preemptive_job_model.
    

results/fifo/rta.v

@@ -19,11 +19,6 @@ Require Export prosa.analysis.facts.busy_interval.carry_in.
 
 Section AbstractRTAforFIFOwithArrivalCurves.
 
-  (** We assume the classic (i.e., Liu & Layland) model of readiness
-      without jitter or self-suspensions, wherein pending jobs are
-      always ready. *)
-  #[local] Existing Instance basic_ready_instance.
-
   (** Consider any type of tasks, each characterized by a WCET, a relative
       deadline, and a run-to-completion threshold, ... *)
   Context {Task : TaskType}.
@@ -39,6 +34,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
   Context {Cost : JobCost Job}.
   Context `{JobPreemptable Job}.
 
+  (** We assume the classic (i.e., Liu & Layland) model of readiness
+      without jitter or self-suspensions, wherein pending jobs are
+      always ready. *)
+  #[local] Existing Instance basic_ready_instance.
+
   (** 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.