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

• The Restricted Supply Model

Library prosa.model.processor.spin

Library prosa.model.processor.supply

• Supply

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

• Task Release Jitter Bound

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

Library prosa.model.priority.coercion

• • Automatic FP ➔ JLFP ➔ JLDP Conversion

Library prosa.model.priority.deadline_monotonic

• Deadline-Monotonic Fixed-Priority Policy

Library prosa.model.priority.definitions

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

Library prosa.model.priority.edf

• EDF Priority Policy

Library prosa.model.priority.elf

• ELF 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 on a Uniprocessor

Library prosa.model.schedule.priority_driven

• Priority-Driven Uniprocessor Schedules

Library prosa.model.schedule.scheduled

• The Scheduled Job(s)

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
  • 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.elf.generality

• Generality of ELF
  • ELF Generalizes GEL
  • ELF Generalizes Fixed-Priority Scheduling

Library prosa.results.elf.rta.bounded_pi

• Response-Time Analysis for the ELF Scheduling Policy
  • 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. Interference and Interfering Workload
  • C. Classic and Abstract Work Conservation
  • D. The Priority Inversion Bound and its Validity
  • E. Maximum Busy-Window Length
  • F. The Interference-Bound Function
  • G. Defining the Search Space
  • H. The Response-Time Bound R
  • I. Soundness of the 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.generality

• Generality of GEL
  • GEL Generalizes EDF
  • GEL Generalizes FIFO
  • GEL Conditionally Generalizes FP

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 task_IBF
  • F. Defining the Search Space
  • G. Stating the Response-Time Bound R
  • H. Soundness of the Response-Time Bound

Library prosa.results.rs.edf.floating_nonpreemptive

• RTA for EDF Scheduling with Floating Non-Preemptive Regions on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
    • Supply-Bound Function
  • Workload Abbreviation
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.results.rs.edf.fully_nonpreemptive

• RTA for Fully Non-Preemptive EDF Scheduling on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
    • Supply-Bound Function
  • Workload Abbreviation
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.results.rs.edf.fully_preemptive

• RTA for Fully Preemptive EDF Scheduling on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
    • Supply-Bound Function
  • Workload Abbreviation
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.results.rs.edf.limited_preemptive

• RTA for EDF Scheduling with Fixed Preemption Points on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
    • Supply-Bound Function
  • Workload Abbreviation
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.results.rs.fifo.bounded_nps

• RTA for FIFO Scheduling on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Schedule
    • The Task Under Analysis
    • Supply-Bound Function
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.results.rs.fp.floating_nonpreemptive

• RTA for FP Scheduling with Floating Non-Preemptive Regions on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
    • Supply-Bound Function
  • Workload Abbreviation
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.results.rs.fp.fully_nonpreemptive

• RTA for Fully Non-Preemptive FP Scheduling on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
    • Supply-Bound Function
  • Workload Abbreviation
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.results.rs.fp.fully_preemptive

• RTA for Fully Preemptive FP Scheduling on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
    • Supply-Bound Function
  • Workload Abbreviation
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.results.rs.fp.limited_preemptive

• RTA for FP Scheduling with Fixed Preemption Points on Restricted-Supply Uniprocessors
  • Defining the System Model
    • Processor Model
    • Tasks and Jobs
    • The Job Arrival Sequence
    • Absence of Self-Suspensions and WCET Compliance
    • The Task Set
    • The Task Under Analysis
    • The Schedule
    • Supply-Bound Function
  • Workload Abbreviation
  • Length of Busy Interval
  • Response-Time Bound

Library prosa.analysis.abstract.IBF.supply

Library prosa.analysis.abstract.IBF.supply_task

Library prosa.analysis.abstract.IBF.task

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

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
  • 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.restricted_supply.abstract_rta

• Abstract Response-Time Analysis for Restricted-Supply Processors (aRSA)

Library prosa.analysis.abstract.restricted_supply.abstract_seq_rta

• Abstract Response-Time Analysis for Restricted-Supply Processors with Sequential Tasks

Library prosa.analysis.abstract.restricted_supply.bounded_bi.aux

• Helper Lemmas for Bounded Busy Interval Lemmas

Library prosa.analysis.abstract.restricted_supply.bounded_bi.edf

• Sufficient Condition for Bounded Busy Intervals for RS EDF

Library prosa.analysis.abstract.restricted_supply.bounded_bi.fp

• Sufficient Condition for Bounded Busy Intervals for RS FP

Library prosa.analysis.abstract.restricted_supply.bounded_bi.jlfp

• Sufficient Condition for Bounded Busy Intervals for RS JLFP

Library prosa.analysis.abstract.restricted_supply.busy_prefix

• Service Inversion Bounded

Library prosa.analysis.abstract.restricted_supply.busy_sbf

• SBF within Abstract Busy Interval

Library prosa.analysis.abstract.restricted_supply.iw_instantiation

• JLFP Instantiation of Interference and Interfering Workload for Restricted-Supply Uniprocessor
• Interference and Interfering Workload
  • Instantiation of Interference
  • Instantiation of Interfering Workload
  • Equivalences

Library prosa.analysis.abstract.restricted_supply.search_space.edf

• Abstract Search Space is a Subset of Restricted Supply EDF Search Space

Library prosa.analysis.abstract.restricted_supply.search_space.fifo

• The Abstract Search Space is a Subset of the FIFO Search Space

Library prosa.analysis.abstract.restricted_supply.search_space.fifo_fixpoint

• Concrete to Abstract Fixpoint Reduction

Library prosa.analysis.abstract.restricted_supply.search_space.fp

• Abstract Search Space is a Subset of Restricted Supply FP Search Space

Library prosa.analysis.abstract.restricted_supply.task_intra_interference_bound

• Task Intra-Supply Interference is Bounded

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

• Blocking Bound for EDF

Library prosa.analysis.definitions.blocking_bound.fp

• Blocking Bound for FP

Library prosa.analysis.definitions.busy_interval.classical

• Busy Interval for JLFP-models

Library prosa.analysis.definitions.busy_interval.edf_pi_bound

• Bound for a Busy-Interval Starting with Priority Inversion under EDF Scheduling

Library prosa.analysis.definitions.carry_in

• No Carry-In

Library prosa.analysis.definitions.completion_sequence

• Notion of a Completion Sequence

Library prosa.analysis.definitions.delay_propagation

• Arrival Curve Propagation
  • Propagation Validity
  • Derived Arrival Curve
  • Derived Arrival Sequence
• Release Jitter Propagation

Library prosa.analysis.definitions.demand_bound_function

• Demand Bound Function (DBF)

Library prosa.analysis.definitions.hyperperiod

Library prosa.analysis.definitions.infinite_jobs

Library prosa.analysis.definitions.interference

• Interference and Interfering Workload

Library prosa.analysis.definitions.job_properties

Library prosa.analysis.definitions.job_response_time

Library prosa.analysis.definitions.priority.classes

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

• SBF within Busy Interval

Library prosa.analysis.definitions.sbf.plain

• Plain Supply Bound Functions (SBFs)
  • Parameter Semantics

Library prosa.analysis.definitions.sbf.pred

• • SBF Parameter Semantics

Library prosa.analysis.definitions.sbf.sbf

• Supply Bound Functions (SBF)

Library prosa.analysis.definitions.schedulability

• Schedulability

Library prosa.analysis.definitions.schedule_prefix

Library prosa.analysis.definitions.service

• Service Definitions

Library prosa.analysis.definitions.service_inversion.busy_prefix

• Service Inversion Bounded

Library prosa.analysis.definitions.service_inversion.pred

• Service Inversion

Library prosa.analysis.definitions.tardiness

• Tardiness

Library prosa.analysis.definitions.task_schedule

• Schedule and Service of task

Library prosa.analysis.definitions.work_bearing_readiness

• Work-Bearing Readiness

Library prosa.analysis.definitions.workload.bounded

• Workload Bound in an Interval Starting with Quiet Time

Library prosa.analysis.definitions.workload.edf_athep_bound

• Bound on Higher-or-Equal Priority Workload under EDF Scheduling

Library prosa.analysis.facts.SBF

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
• Incremental Service in Unit-Service Schedules

Library prosa.analysis.facts.behavior.supply

• Supply

Library prosa.analysis.facts.blocking_bound.edf

• Lower-Priority Non-Preemptive Segment is Bounded

Library prosa.analysis.facts.blocking_bound.fp

• Lower-Priority Non-Preemptive Segment is Bounded

Library prosa.analysis.facts.busy_interval.all

Library prosa.analysis.facts.busy_interval.arrival

Library prosa.analysis.facts.busy_interval.carry_in

• Busy Interval From Workload Bound
  • Times without Carry-In
  • Bounded-Workload Assumption
  • Existence of a No-Carry-In Instant
  • Busy Interval Existence

Library prosa.analysis.facts.busy_interval.existence

• Existence of Busy Interval for JLFP-models

Library prosa.analysis.facts.busy_interval.hep_at_pt

• Processor Executes HEP jobs at Preemption Point
• Processor Executes HEP Jobs after Preemption Point

Library prosa.analysis.facts.busy_interval.pi

• Priority Inversion in a Busy Interval
  • Lower Priority In Busy Intervals
• Priority Inversion due to Non-Preemptive Sections

Library prosa.analysis.facts.busy_interval.pi_bound

• Bounded Priority Inversion Due to Non-Preemptive Sections

Library prosa.analysis.facts.busy_interval.pi_cond

Library prosa.analysis.facts.busy_interval.quiet_time

Library prosa.analysis.facts.busy_interval.service_inversion

• Service Inversion Lemmas

Library prosa.analysis.facts.delay_propagation

• Propagation of Delays in Arrival Curves
  • Arrival Sequence Validity Properties
  • Correctness of the Propagated Arrival Curve

Library prosa.analysis.facts.edf_definitions

• Equivalence of EDF Definitions

Library prosa.analysis.facts.hyperperiod

Library prosa.analysis.facts.interference

• Auxiliary Lemmas about Interference

Library prosa.analysis.facts.jitter

• Propagation of Release Jitter in Arrival Curves
  • Restated General Properties
  • Jitter Propagation Properties
  • Transferred Response-Time Bound

Library prosa.analysis.facts.job_index

Library prosa.analysis.facts.model.arrival_curves

• Facts About Arrival Curves

Library prosa.analysis.facts.model.dbf

• Facts about the Demand Bound Function (DBF)

Library prosa.analysis.facts.model.ideal.priority_inversion

• Lemmas about Priority Inversion for ideal uni-processors

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

• Automation

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

• Service Received by Sets of Jobs in Uniprocessor Schedules
• Service Received by Sets of Jobs in Uniprocessor Ideal-Progress 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.restricted_supply.schedule

• Automation

Library prosa.analysis.facts.model.scheduled

• Correctness of the Scheduled Job(s)
  • The Set of Jobs Scheduled at a Given Time
  • The Job Scheduled on an Ideal Progress Processor
  • The Job Scheduled on a Uniprocessor
  • Case Analysis: a Scheduled Job Exists or no Job is Scheduled

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

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

• • Basic properties of the ELF policy
  • Sequentiality under ELF

Library prosa.analysis.facts.priority.fifo

Library prosa.analysis.facts.priority.fifo_ahep_bound

• Higher-or-Equal-Priority Interference Bound under FIFO

Library prosa.analysis.facts.priority.gel

Library prosa.analysis.facts.priority.inversion

• Lemmas about Priority Inversion
  • Occurrence of Priority Inversion
  • Occurrence of Priority Inversion on Uniprocessors
  • Cumulative Priority Inversion

Library prosa.analysis.facts.priority.jlfp_with_fp

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

• Bound on Higher-or-Equal Priority Workload under EDF Scheduling is Valid

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

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

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
• Task Declaration Notation