Library prosa.behavior.time

• Model of Time

Library prosa.behavior.job

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

Library prosa.behavior.schedule

• Generic Processor State
• 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.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.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.periodic

• The Periodic Task Model
  • Task Model Parameter for Periods
  • Model Validity
  • Treating Periodic Tasks as Sporadic Tasks

Library prosa.model.task.arrival.sporadic

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

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.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

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.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
  • Priority inversion is bounded
  • Response-Time Bound

Library prosa.results.edf.rta.bounded_pi

• Abstract RTA for EDF-schedulers with Bounded Priority Inversion
  • 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.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
  • Filling Out Hypotheses Of Abstract RTA Theorem
  • Final Theorem

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.analysis.abstract.abstract_rta

• Abstract Response-Time Analysis

Library prosa.analysis.abstract.abstract_seq_rta

• Abstract Response-Time Analysis with sequential tasks

Library prosa.analysis.abstract.definitions

• Definitions for Abstract Response-Time Analysis

Library prosa.analysis.abstract.ideal_jlfp_rta

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

Library prosa.analysis.abstract.run_to_completion

• Run-to-Completion Threshold of a job

Library prosa.analysis.abstract.search_space

• Reduction of the search space for Abstract RTA

Library prosa.analysis.definitions.busy_interval

• Busy Interval for JLFP-models

Library prosa.analysis.definitions.carry_in

• No Carry-In

Library prosa.analysis.definitions.job_properties

Library prosa.analysis.definitions.priority_inversion

• Cumulative Priority Inversion for JLFP-models

Library prosa.analysis.definitions.progress

• Job Progress (or Lack Thereof)

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.task_schedule

• Schedule of task

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.priority_inversion

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

Library prosa.analysis.facts.edf

Library prosa.analysis.facts.model.ideal_schedule

• Incremental Service in Ideal Schedule
• Automation

Library prosa.analysis.facts.model.rbf

• Facts about Request Bound Functions (RBFs)
  • RBF is a Bound on Workload
  • RBF Properties

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.workload

• Lemmas about Workload of Sets of Jobs

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.readiness.basic

Library prosa.analysis.facts.tdma

Library prosa.analysis.facts.transform.edf_opt

Library prosa.analysis.facts.transform.replace_at

Library prosa.analysis.facts.transform.swaps

Library prosa.analysis.transform.edf_trans

Library prosa.analysis.transform.prefix

Library prosa.analysis.transform.swap

Library prosa.util.all

Library prosa.util.bigcat

Library prosa.util.counting

Library prosa.util.div_mod

Library prosa.util.epsilon

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.rewrite_facilities

• Rewriting

Library prosa.util.search_arg

Library prosa.util.seqset

Library prosa.util.ssromega

Library prosa.util.step_function

Library prosa.util.sum

Library prosa.util.supremum

• Computation of a Sequence's Supremum

Library prosa.util.tactics

• • Exploiting a hypothesis
• Handier movement of inequalities.