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

Library prosa.model.readiness.basic

• Liu & Layland Readiness Model

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

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

Library prosa.model.priority.edf

• EDF 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.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.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.util.all

Library prosa.util.bigcat

Library prosa.util.counting

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

Library prosa.util.step_function

Library prosa.util.sum

Library prosa.util.tactics

• • Exploiting a hypothesis
• Handier movement of inequalities.