Make the ideal uniprocessor hypothesis more explicit

analysis/facts/model/ideal_schedule.v

 Require Export prosa.util.all.
 Require Export prosa.model.processor.platform_properties.
 Require Export prosa.analysis.facts.behavior.service.
-
-(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
 
 (** Note: we do not re-export the basic definitions to avoid littering the global
@@ -11,6 +9,9 @@ Require Import prosa.model.processor.ideal.
 (** In this section we establish the classes to which an ideal schedule belongs. *)
 Section ScheduleClass.
 
+  (** We assume ideal uni-processor schedules. *)
+  #[local] Existing Instance ideal.processor_state.
+
   Local Transparent scheduled_in scheduled_on.
   (** Consider any job type and the ideal processor model. *)
   Context {Job: JobType}.

analysis/facts/transform/wc_correctness.v

@@ -6,6 +6,7 @@ Require Export prosa.analysis.transform.wc_trans.
 Require Export prosa.analysis.facts.transform.swaps.
 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.util.list.
+Require Import prosa.model.processor.ideal.
 
 (** * Correctness of the work-conservation transformation *)
 (** This file contains the main argument of the work-conservation proof,
@@ -14,16 +15,17 @@ Require Export prosa.util.list.
     and ending with the proofs of individual properties of the obtained
     work-conserving schedule. *)
 
-(** Throughout this file, we assume ideal uniprocessor schedules and
-    the basic (i.e., Liu & Layland) readiness model under which any
-    pending job is ready. *)
-Require Import prosa.model.processor.ideal.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland)
+    readiness model under which any pending job is ready. *)
 Require Import prosa.model.readiness.basic.
 
 (** In order to discuss the correctness of the work-conservation transformation at a high level,
     we first need a set of lemmas about the inner parts of the procedure. *)
 Section AuxiliaryLemmasWorkConservingTransformation.
-  
+
+  (** We assume ideal uni-processor schedules. *)
+  #[local] Existing Instance ideal.processor_state.
+
   (** Consider any type of jobs with arrival times, costs, and deadlines... *)
   Context {Job : JobType}.
   Context `{JobArrival Job}.

analysis/transform/wc_trans.v

@@ -2,8 +2,6 @@ Require Export prosa.analysis.transform.swap.
 Require Export prosa.analysis.transform.prefix.
 Require Export prosa.util.search_arg.
 Require Export prosa.util.list.
-
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Export prosa.model.processor.ideal.
 
 (** In this file we define the transformation from any ideal uniprocessor schedule 
@@ -12,7 +10,10 @@ Require Export prosa.model.processor.ideal.
     its arrival, therefore there could still exist idle instants between any two
     job allocations. *)
 Section WCTransformation.
-  
+
+  (** We assume ideal uni-processor schedules. *)
+  #[local] Existing Instance ideal.processor_state.
+
   (** Consider any type of jobs with arrival times, costs, and deadlines... *)
   Context {Job : JobType}.
   Context `{JobArrival Job}.

model/processor/ideal.v

@@ -20,8 +20,8 @@ Section State.
   (** We connect the notion of an ideal processor state with
       the generic interface for the processor-state abstraction in Prosa by
       declaring a so-called instance of the [ProcessorState] typeclass. *)
-  Global Program Instance processor_state : ProcessorState Job :=
-    {
+  Program Definition processor_state : ProcessorState Job :=
+    {|
       (** We define the ideal "processor state" as an [option Job],
           which means that it is either [Some j] (where [j] is a
           [Job]) or [None] (which we use to indicate an idle
@@ -35,7 +35,7 @@ Section State.
       (** Similarly, we say that a given job [j] receives service in a
           given state [s] iff [s] is [Some j]. *)
       service_on j s (_ : unit) := if s == Some j then 1 else 0;
-    }.
+    |}.
   Next Obligation. by rewrite /nat_of_bool; case: ifP H => // ? /negP[]. Qed.
 
 End State.

results/fixed_priority/rta/floating_nonpreemptive.v

@@ -3,14 +3,13 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
 Require Export prosa.analysis.facts.readiness.sequential.
-
+Require Import prosa.model.processor.ideal.
 
 (** * RTA for Model with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions FP model. *)
 
-(** Throughout this file, we assume the FP priority policy, ideal uni-processor 
+(** Throughout this file, we assume the FP priority policy,
     schedules, and the sequential readiness model. *)
-Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.sequential.
 
 (** Furthermore, we assume the task model with floating non-preemptive regions. *)
@@ -21,6 +20,9 @@ Require Import prosa.model.task.preemption.floating_nonpreemptive.
 
 Section RTAforFloatingModelwithArrivalCurves.
 
+  (** We assume ideal uni-processor schedules. *)
+  #[local] Existing Instance ideal.processor_state.
+
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.

results/fixed_priority/rta/fully_nonpreemptive.v

@@ -4,14 +4,13 @@ Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 Require Export prosa.analysis.facts.readiness.sequential.
-
+Require Import prosa.model.processor.ideal.
 
 (** * RTA for Fully Non-Preemptive FP Model *)
 (** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
 
-(** Throughout this file, we assume the FP priority policy, ideal uni-processor 
+(** Throughout this file, we assume the FP priority policy,
     schedules, and the sequential readiness model. *)
-Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.sequential.
 
 (** Furthermore, we assume the fully non-preemptive task model. *)
@@ -21,6 +20,9 @@ Require Import prosa.model.task.preemption.fully_nonpreemptive.
 
 Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
 
+  (** We assume ideal uni-processor schedules. *)
+  #[local] Existing Instance ideal.processor_state.
+
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.

results/fixed_priority/rta/fully_preemptive.v

@@ -4,14 +4,13 @@ Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
 Require Export prosa.analysis.facts.readiness.sequential.
-
+Require Import prosa.model.processor.ideal.
 
 (** * RTA for Fully Preemptive FP Model *)
 (** In this section we prove the RTA theorem for the fully preemptive FP model *)
 
-(** Throughout this file, we assume the FP priority policy, ideal uni-processor 
+(** Throughout this file, we assume the FP priority policy,
     schedules, and the sequential readiness model. *)
-Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.sequential.
 
 (** Furthermore, we assume the fully preemptive task model. *)
@@ -21,6 +20,9 @@ Require Import prosa.model.task.preemption.fully_preemptive.
 
 Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
 
+  (** We assume ideal uni-processor schedules. *)
+  #[local] Existing Instance ideal.processor_state.
+
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.

results/fixed_priority/rta/limited_preemptive.v

@@ -3,15 +3,14 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.sequential.
-
+Require Import prosa.model.processor.ideal.
 
 (** * RTA for FP-schedulers with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for FP-schedulers with
     fixed preemption points. *)
 
-(** Throughout this file, we assume the FP priority policy, ideal uni-processor 
+(** Throughout this file, we assume the FP priority policy,
     schedules, and the sequential readiness model. *)
-Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.sequential.
 
 (** Furthermore, we assume the task model with fixed preemption points. *)
@@ -22,6 +21,9 @@ Require Import prosa.model.task.preemption.limited_preemptive.
 
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
 
+  (** We assume ideal uni-processor schedules. *)
+  #[local] Existing Instance ideal.processor_state.
+
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.