Library prosa.behavior.time

• Model of Time

Library prosa.behavior.job

• Notion of a Job Type
• Notion of Work
• Basic Job Parameters — Cost, Arrival Time, and Absolute Deadline

Library prosa.behavior.schedule

• Generic Processor State Interface
• Schedule Representation

Library prosa.behavior.service

• Service of a Job
• Job Completion and Response Time
• Pending or Incomplete Jobs

Library prosa.behavior.arrival_sequence

• Notion of an Arrival Sequence
• Arrival of a Job
• Validity of an Arrival Sequence
• Arrival Time Predicates
• Finite Arrival Sequence Prefixes

Library prosa.behavior.ready

• Readiness of a Job
• Backlogged Jobs
• Validity of a Schedule

Library prosa.behavior.all

Library prosa.model.processor.ideal

• The Ideal Uniprocessor Model
  • Idle Instants

Library prosa.model.processor.multiprocessor

• Multiprocessor State

Library prosa.model.processor.platform_properties

Library prosa.model.processor.spin

Library prosa.model.processor.varspeed

Library prosa.model.readiness.basic

• Liu & Layland Readiness Model

Library prosa.model.readiness.jitter

• Job Model Parameter for Jobs Exhibiting Release Jitter
• Readiness of Jobs with Release Jitter

Library prosa.model.readiness.sequential

• Sequential Readiness Model

Library prosa.model.readiness.suspension

• Job Model Parameter for Jobs Exhibiting Self-Suspensions
• Readiness of Self-Suspending Jobs
• Total Suspension Time of a Job

Library prosa.model.preemption.fully_nonpreemptive

• Preemption Model: Fully Non-Preemptive Jobs

Library prosa.model.preemption.fully_preemptive

• Preemption Model: Fully Preemptive Jobs

Library prosa.model.preemption.limited_preemptive

• Job Model Parameter for Preemption Points
• Preemption Model: Limited-Preemptive Jobs
  • Model Validity

Library prosa.model.preemption.parameter

• Job-Level Preemption Model
• Maximum and Last Non-preemptive Segment of a Job
• Run-to-Completion Threshold of a Job
• Model Validity

Library prosa.model.task.absolute_deadline

Library prosa.model.task.arrival.curve_as_rbf

• Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF)

Library prosa.model.task.arrival.curves

• The Arbitrary Arrival Curves Model
  • Task Parameters for the Arrival Curves Model
  • Parameter Semantics
    • Definition of Arrival Curves
    • Definition of Minimum Distance Bounds
  • Model Validity

Library prosa.model.task.arrival.example

• Arrival Model Conversion
  • Periodic Tasks as Sporadic Tasks
  • Periodic Tasks as Arrival Curves
  • Periodic Tasks as RBFs

Library prosa.model.task.arrival.periodic

• The Periodic Task Model
  • Task Model Parameter for Periods
  • Model Validity

Library prosa.model.task.arrival.periodic_as_sporadic

• • Treating Periodic Tasks as Sporadic Tasks

Library prosa.model.task.arrival.request_bound_functions

• Request Bound Functions (RBF)
  • Task Parameters for the Request Bound Functions
  • Parameter Semantics
    • Definition of Request Bound Functions
  • Model Validity

Library prosa.model.task.arrival.sporadic

• The Sporadic Task Model
  • Task Parameter for the Sporadic Task Model
  • Model Validity

Library prosa.model.task.arrival.sporadic_as_curve

Library prosa.model.task.arrival.task_max_inter_arrival

• Task Max Inter-Arrival

Library prosa.model.task.arrivals

Library prosa.model.task.concept

• Task Type
• Task Model Core Parameters
• Task Model Validity
• Task Sets

Library prosa.model.task.offset

• Task Offset

Library prosa.model.task.preemption.floating_nonpreemptive

• Task Model with Floating Non-Preemptive Regions
  • Model Validity
  • Run-to-Completion Threshold

Library prosa.model.task.preemption.fully_nonpreemptive

• Fully Non-Preemptive Task Model
  • Run-to-Completion Threshold

Library prosa.model.task.preemption.fully_preemptive

• Fully Preemptive Task Model
  • Run-to-Completion Threshold

Library prosa.model.task.preemption.limited_preemptive

• Limited-Preemptive Task Model
  • Model Validity
  • Run-to-Completion Threshold

Library prosa.model.task.preemption.parameters

• Task Preemption Model
  • Preemption-Related Task Parameters
  • Derived Properties
  • Preemption Model Validity
  • Run-to-Completion Threshold Validity

Library prosa.model.task.sequentiality

Library prosa.model.task.suspension.dynamic

• Task Parameter for the Dynamic Self-Suspension Model
• Validity

Library prosa.model.priority.classes

• The FP, JLFP, and JLDP Priority Classes
  • Automatic FP ➔ JLFP ➔ JLDP Conversion
  • Properties of Priority Policies
  • Derived Priority Relations

Library prosa.model.priority.deadline_monotonic

• Deadline-Monotonic Fixed-Priority Policy

Library prosa.model.priority.edf

• EDF Priority Policy

Library prosa.model.priority.fifo

• FIFO Priority Policy

Library prosa.model.priority.gel

• GEL Priority Policy

Library prosa.model.priority.numeric_fixed_priority

• Numeric Fixed Task Priorities

Library prosa.model.priority.rate_monotonic

• Rate-Monotonic Fixed-Priority Policy

Library prosa.model.schedule.edf

• Fully-Preemptive EDF Schedules

Library prosa.model.schedule.limited_preemptive

• Preemption Model Compliance

Library prosa.model.schedule.nonpreemptive

• Nonpreemptive Schedules

Library prosa.model.schedule.preemption_time

• Preemption Times

Library prosa.model.schedule.priority_driven

• Priority-Driven Schedules

Library prosa.model.schedule.tdma

• TDMA Scheduling
  • Task Parameter for TDMA Scheduling
  • TDMA Policy Validity
  • TDMA Cycles, Sots, and Offsets
  • TDMA Schedule Validity

Library prosa.model.schedule.work_conserving

• Definition of Work Conservation

Library prosa.model.aggregate.service_of_jobs

• Service Received by Sets of Jobs

Library prosa.model.aggregate.workload

• Cumulative Workload of Sets of Jobs

Library prosa.results.edf.optimality

• Optimality of EDF on Ideal Uniprocessors
  • Optimality Theorem
  • Weak Optimality Theorem

Library prosa.results.edf.rta.bounded_nps

• RTA for EDF with Bounded Non-Preemptive Segments
  • Search Space
  • Priority inversion is bounded
  • Response-Time Bound

Library prosa.results.edf.rta.bounded_pi

• Abstract RTA for EDF-schedulers with Bounded Priority Inversion
  • Instantiation of Interference
  • Instantiation of Interfering Workload
  • Filling Out Hypothesis Of Abstract RTA Theorem
  • Final Theorem

Library prosa.results.edf.rta.floating_nonpreemptive

• RTA for EDF with Floating Non-Preemptive Regions
  • Setup and Assumptions
  • Total Workload and Length of Busy Interval
  • Response-Time Bound

Library prosa.results.edf.rta.fully_nonpreemptive

• RTA for Fully Non-Preemptive EDF
  • Setup and Assumptions
  • Total Workload and Length of Busy Interval
  • Response-Time Bound

Library prosa.results.edf.rta.fully_preemptive

• RTA for Fully Preemptive EDF
  • Setup and Assumptions
  • Total Workload and Length of Busy Interval
  • Response-Time Bound

Library prosa.results.edf.rta.limited_preemptive

• RTA for EDF with Fixed Preemption Points
  • Setup and Assumptions
  • Total Workload and Length of Busy Interval
  • Response-Time Bound

Library prosa.results.fifo.rta

• Response-Time Analysis for FIFO Schedulers
  • A. Defining the System Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
  • B. Encoding the Scheduling Policy and Preemption Model
  • C. Classic and Abstract Work Conservation
  • D. Bounding the Maximum Busy-Window Length
  • E. Defining the Interference Bound Function (IBF)
    • Absence of Priority Inversion
    • Higher- and Equal-Priority Interference
    • Correctness of IBF
  • F. Defining the Search Space
  • G. Stating the Response-Time Bound R
  • H. Soundness of the Response-Time Bound

Library prosa.results.fixed_priority.rta.bounded_nps

• RTA for FP-schedulers with Bounded Non-Preemptive Segments
  • Priority inversion is bounded
  • Response-Time Bound

Library prosa.results.fixed_priority.rta.bounded_pi

• Abstract RTA for FP-schedulers with Bounded Priority Inversion
  • Instantiation of Interference
  • Instantiation of Interfering Workload
  • Filling Out Hypotheses Of Abstract RTA Theorem
  • Final Theorem

Library prosa.results.fixed_priority.rta.comp.fully_preemptive

• RTA for Fully Preemptive FP Scheduling with Computed Fixpoints
  • Problem Setup and Analysis Context
  • Computation of the Fixpoints
  • Correctness of the Response-Time Bound

Library prosa.results.fixed_priority.rta.floating_nonpreemptive

• RTA for Model with Floating Non-Preemptive Regions
  • Setup and Assumptions
  • Total Workload and Length of Busy Interval
  • Response-Time Bound

Library prosa.results.fixed_priority.rta.fully_nonpreemptive

• RTA for Fully Non-Preemptive FP Model
  • Setup and Assumptions
  • Total Workload and Length of Busy Interval
  • Response-Time Bound

Library prosa.results.fixed_priority.rta.fully_preemptive

• RTA for Fully Preemptive FP Model
  • Setup and Assumptions
  • Total Workload and Length of Busy Interval
  • Response-Time Bound

Library prosa.results.fixed_priority.rta.limited_preemptive

• RTA for FP-schedulers with Fixed Preemption Points
  • Setup and Assumptions
  • Total Workload and Length of Busy Interval
  • Response-Time Bound

Library prosa.results.gel.rta.bounded_pi

• Abstract RTA for GEL-Schedulers with Bounded Priority Inversion
  • A. Defining the System Model
  • B. Encoding the Scheduling Policy and Preemption Model
  • C. Abstract Work Conservation
  • D. Bounding the Maximum Busy-Window Length
  • E. Defining IBF_other
  • F. Defining the Search Space
  • G. Stating the Response-Time Bound R
  • H. Soundness of the Response-Time Bound

Library prosa.analysis.abstract.abstract_rta

• Abstract Response-Time Analysis
• Proof of the Theorem
  • Case 1
  • Case 2
  • Case 3
    • Case 3.1
    • Case 3.2
• Response-Time Bound

Library prosa.analysis.abstract.busy_interval

• Lemmas About Abstract Busy Intervals

Library prosa.analysis.abstract.definitions

• Definitions for Abstract Response-Time Analysis
  • a) Interference
  • b) Interfering Workload

Library prosa.analysis.abstract.ideal.abstract_rta

• Abstract Response-Time Analysis For Processor State with Ideal Uni-Service Progress Model

Library prosa.analysis.abstract.ideal.abstract_seq_rta

• Abstract Response-Time Analysis with sequential tasks

Library prosa.analysis.abstract.ideal.iw_instantiation

• JLFP instantiation of Interference and Interfering Workload for ideal uni-processor.
• Interference and Interfering Workload
  • Instantiation of Interference
  • Instantiation of Interfering Workload
  • Auxiliary definitions
  • Equivalences

Library prosa.analysis.abstract.iw_auxiliary

• Auxiliary Lemmas About Interference and Interfering Workload.

Library prosa.analysis.abstract.lower_bound_on_service

• Lower Bound On Job Service

Library prosa.analysis.abstract.search_space

• Reduction of the search space for Abstract RTA

Library prosa.analysis.definitions.always_higher_priority

• Always Higher Priority

Library prosa.analysis.definitions.busy_interval

• Busy Interval for JLFP-models

Library prosa.analysis.definitions.carry_in

• No Carry-In

Library prosa.analysis.definitions.completion_sequence

• Notion of a Completion Sequence

Library prosa.analysis.definitions.hyperperiod

Library prosa.analysis.definitions.infinite_jobs

Library prosa.analysis.definitions.job_properties

Library prosa.analysis.definitions.job_response_time

Library prosa.analysis.definitions.priority_inversion

• Priority Inversion

Library prosa.analysis.definitions.progress

• Job Progress (or Lack Thereof)

Library prosa.analysis.definitions.readiness

• Properties of Readiness Models

Library prosa.analysis.definitions.request_bound_function

• Request Bound Function (RBF)
  • RBF of a Single Task
  • Total RBF of Multiple Tasks

Library prosa.analysis.definitions.schedulability

• Schedulability

Library prosa.analysis.definitions.schedule_prefix

Library prosa.analysis.definitions.tardiness

• Tardiness

Library prosa.analysis.definitions.task_schedule

• Schedule of task

Library prosa.analysis.definitions.work_bearing_readiness

• Work-Bearing Readiness

Library prosa.analysis.facts.behavior.all

Library prosa.analysis.facts.behavior.arrivals

• Arrival Sequence

Library prosa.analysis.facts.behavior.completion

• Completion

Library prosa.analysis.facts.behavior.deadlines

• Deadlines

Library prosa.analysis.facts.behavior.service

• Service

Library prosa.analysis.facts.busy_interval.busy_interval

• Existence of Busy Interval for JLFP-models

Library prosa.analysis.facts.busy_interval.carry_in

• Existence of No Carry-In Instant

Library prosa.analysis.facts.busy_interval.ideal.hep_job_scheduled

• Processor Executes HEP jobs at Preemption Point

Library prosa.analysis.facts.busy_interval.ideal.inequalities

Library prosa.analysis.facts.busy_interval.ideal.priority_inversion

• Lemmas about Priority Inversion for ideal uni-processors

Library prosa.analysis.facts.busy_interval.ideal.priority_inversion_bounded

• Priority inversion is bounded
• Processor Executes HEP jobs after Preemption Point
• Preemption Time Exists

Library prosa.analysis.facts.busy_interval.priority_inversion

• Lemma about Priority Inversion for arbitrary processors

Library prosa.analysis.facts.busy_interval.quiet_time

Library prosa.analysis.facts.edf_definitions

• Equivalence of EDF Definitions

Library prosa.analysis.facts.hyperperiod

Library prosa.analysis.facts.job_index

Library prosa.analysis.facts.model.arrival_curves

• Facts About Arrival Curves

Library prosa.analysis.facts.model.ideal.schedule

• Incremental Service in Ideal Schedule
• Automation

Library prosa.analysis.facts.model.ideal.service_of_jobs

• Service Received by Sets of Jobs in Ideal Uni-Processor Schedules

Library prosa.analysis.facts.model.offset

Library prosa.analysis.facts.model.preemption

Library prosa.analysis.facts.model.rbf

• Facts about Request Bound Functions (RBFs)
  • RBF is a Bound on Workload
  • RBF Properties
  • Monotonicity of the Total RBF
  • RBFs Equal to Zero for Duration ε

Library prosa.analysis.facts.model.sequential

Library prosa.analysis.facts.model.service_of_jobs

• Lemmas about Service Received by Sets of Jobs

Library prosa.analysis.facts.model.task_arrivals

Library prosa.analysis.facts.model.task_cost

Library prosa.analysis.facts.model.task_schedule

Library prosa.analysis.facts.model.workload

• Lemmas about Workload of Sets of Jobs

Library prosa.analysis.facts.periodic.arrival_separation

Library prosa.analysis.facts.periodic.arrival_times

Library prosa.analysis.facts.periodic.max_inter_arrival

• • Periodic Task Model respects the Task Max Inter-Arrival model.

Library prosa.analysis.facts.periodic.task_arrivals_size

Library prosa.analysis.facts.preemption.job.limited

• Platform for Models with Limited Preemptions

Library prosa.analysis.facts.preemption.job.nonpreemptive

• Platform for Fully Non-Preemptive model

Library prosa.analysis.facts.preemption.job.preemptive

• Preemptions in Fully Preemptive Model

Library prosa.analysis.facts.preemption.rtc_threshold.floating

• Task's Run to Completion Threshold

Library prosa.analysis.facts.preemption.rtc_threshold.job_preemptable

• Run-to-Completion Threshold

Library prosa.analysis.facts.preemption.rtc_threshold.limited

• Task's Run to Completion Threshold

Library prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive

• Task's Run to Completion Threshold

Library prosa.analysis.facts.preemption.rtc_threshold.preemptive

• Task's Run to Completion Threshold

Library prosa.analysis.facts.preemption.task.floating

• Platform for Floating Non-Preemptive Regions Model

Library prosa.analysis.facts.preemption.task.limited

• Platform for Models with Limited Preemptions

Library prosa.analysis.facts.preemption.task.nonpreemptive

• Platform for Fully Non-Preemptive Model

Library prosa.analysis.facts.preemption.task.preemptive

• Platform for Fully Preemptive Model

Library prosa.analysis.facts.priority.classes

Library prosa.analysis.facts.priority.edf

Library prosa.analysis.facts.priority.fifo

Library prosa.analysis.facts.priority.gel

Library prosa.analysis.facts.priority.sequential

Library prosa.analysis.facts.readiness.backlogged

Library prosa.analysis.facts.readiness.basic

Library prosa.analysis.facts.readiness.sequential

Library prosa.analysis.facts.shifted_job_costs

Library prosa.analysis.facts.sporadic.arrival_bound

• Sporadic Arrival Bound

Library prosa.analysis.facts.sporadic.arrival_sequence

• Job Arrival Sequence in the Sporadic Model

Library prosa.analysis.facts.sporadic.arrival_times

• Job Arrival Times in the Sporadic Model

Library prosa.analysis.facts.tdma

Library prosa.analysis.facts.transform.edf_opt

Library prosa.analysis.facts.transform.edf_wc

• Optimality of Work-Conserving EDF on Ideal Uniprocessors
  • Non-Idle Swaps
  • Work-Conserving Swap Candidates
  • Work-Conservation of the Point-Wise EDF Transformation
  • Work-Conserving EDF Prefix
  • Work-Conservation of the EDF Transformation

Library prosa.analysis.facts.transform.replace_at

Library prosa.analysis.facts.transform.swaps

Library prosa.analysis.facts.transform.wc_correctness

• Correctness of the work-conservation transformation

Library prosa.analysis.transform.edf_trans

Library prosa.analysis.transform.prefix

Library prosa.analysis.transform.swap

Library prosa.analysis.transform.wc_trans

Library prosa.util.all

Library prosa.util.bigcat

Library prosa.util.div_mod

Library prosa.util.epsilon

Library prosa.util.fixpoint

• Fixpoint Search
  • Least Positive Fixpoint
  • Maximal Fixpoint across a Search Space
  • Search Space Defined by a Predicate

Library prosa.util.lcmseq

Library prosa.util.list

Library prosa.util.minmax

Library prosa.util.nat

Library prosa.util.nondecreasing

• Non-Decreasing Sequence and Distances
• Properties of Increasing Sequence
• Properties of Non-Decreasing Sequence
• Properties of Undup of Non-Decreasing Sequence
• Properties of Distances
• Properties of Distances of Non-Decreasing Sequence

Library prosa.util.notation

Library prosa.util.rel

Library prosa.util.search_arg

Library prosa.util.seqset

Library prosa.util.setoid

Library prosa.util.subadditivity

Library prosa.util.sum

Library prosa.util.superadditivity

Library prosa.util.supremum

• Computation of a Sequence's Supremum

Library prosa.util.tactics

• • Exploiting a hypothesis
• Handier movement of inequalities.

Library prosa.util.unit_growth

Library prosa.implementation.definitions.arrival_bound

• Implementation of a Task's Arrival Bound

Library prosa.implementation.definitions.extrapolated_arrival_curve

Library prosa.implementation.definitions.generic_scheduler

• Generic Reference Scheduler

Library prosa.implementation.definitions.ideal_uni_scheduler

• Ideal Uniprocessor Reference Scheduler
  • Preemption-Aware Scheduler
  • Priority-Aware Scheduler

Library prosa.implementation.definitions.job_constructor

• Job Constructor

Library prosa.implementation.definitions.maximal_arrival_sequence

• A Maximal Arrival Sequence

Library prosa.implementation.definitions.task

• Implementation of Tasks and Jobs
  • Implementation of a Concrete Task
  • Implementation of a Concrete Job
  • Instances for Concrete Jobs and Tasks.

Library prosa.implementation.facts.extrapolated_arrival_curve

Library prosa.implementation.facts.generic_schedule

• Properties of the Generic Reference Scheduler

Library prosa.implementation.facts.ideal_uni.preemption_aware

• Properties of the Preemption-Aware Ideal Uniprocessor Scheduler

Library prosa.implementation.facts.ideal_uni.prio_aware

• Ideal Uniprocessor Scheduler Properties

Library prosa.implementation.facts.job_constructor

Library prosa.implementation.facts.maximal_arrival_sequence

Library prosa.implementation.refinements.EDF.fast_search_space

• Search Space Definitions
• Fast Search Space Computation Lemmas

Library prosa.implementation.refinements.EDF.nonpreemptive_sched

• • Fully-Nonpreemptive Earliest-Deadline-First Schedules

Library prosa.implementation.refinements.EDF.preemptive_sched

• • Fully-Preemptive Earliest-Deadline-First Schedules

Library prosa.implementation.refinements.EDF.refinements

• • Refinements

Library prosa.implementation.refinements.FP.fast_search_space

• Search Space Definitions

Library prosa.implementation.refinements.FP.nonpreemptive_sched

• • Fully-Nonpreemptive Fixed-Priority Schedules

Library prosa.implementation.refinements.FP.preemptive_sched

• • Fully-Preemptive Fixed-Priority Schedules

Library prosa.implementation.refinements.FP.refinements

• • Refinements

Library prosa.implementation.refinements.arrival_bound

Library prosa.implementation.refinements.arrival_curve

• • Arrival Curve Refinements.

Library prosa.implementation.refinements.arrival_curve_prefix

Library prosa.implementation.refinements.fast_search_space_computation

Library prosa.implementation.refinements.refinements

• Refinements Library
  • Brief Introduction
  • Auxiliary Definitions
• Basic Arithmetic
  • Definitions
  • Refinements
  • Supporting Lemmas
• Functions on Lists
  • Definitions
  • Refinements
  • Supporting Lemmas

Library prosa.implementation.refinements.task

• • Task Refinement