Library rt.implementation.arrival_sequence

Library rt.implementation.global.parallel.bertogna_edf_example

Library rt.implementation.global.parallel.bertogna_fp_example

Library rt.implementation.global.basic.schedule

Library rt.implementation.global.basic.bertogna_edf_example

Library rt.implementation.global.basic.bertogna_fp_example

Library rt.implementation.global.jitter.schedule

Library rt.implementation.global.jitter.arrival_sequence

Library rt.implementation.global.jitter.bertogna_edf_example

Library rt.implementation.global.jitter.job

Library rt.implementation.global.jitter.bertogna_fp_example

Library rt.implementation.global.jitter.task

Library rt.implementation.job

Library rt.implementation.apa.schedule

Library rt.implementation.apa.arrival_sequence

Library rt.implementation.apa.bertogna_edf_example

Library rt.implementation.apa.job

Library rt.implementation.apa.bertogna_fp_example

Library rt.implementation.apa.task

Library rt.implementation.uni.susp.schedule

Library rt.implementation.uni.susp.dynamic.oblivious.fp_rta_example

Library rt.implementation.uni.susp.dynamic.arrival_sequence

Library rt.implementation.uni.susp.dynamic.job

Library rt.implementation.uni.susp.dynamic.task

Library rt.implementation.uni.basic.schedule_tdma

Library rt.implementation.uni.basic.schedule

Library rt.implementation.uni.basic.tdma_rta_example

Library rt.implementation.uni.basic.extraction_tdma

Library rt.implementation.uni.basic.fp_rta_example

Library rt.implementation.uni.jitter.schedule

Library rt.implementation.uni.jitter.arrival_sequence

Library rt.implementation.uni.jitter.job

Library rt.implementation.uni.jitter.fp_rta_example

Library rt.implementation.uni.jitter.task

Library rt.implementation.task

Library rt.model.priority

Library rt.model.suspension

Library rt.model.schedule.partitioned.schedule

Library rt.model.schedule.partitioned.schedulability

Library rt.model.schedule.global.schedulability

Library rt.model.schedule.global.workload

Library rt.model.schedule.global.transformation.construction

Library rt.model.schedule.global.response_time

Library rt.model.schedule.global.basic.schedule

Library rt.model.schedule.global.basic.constrained_deadlines

Library rt.model.schedule.global.basic.interference_edf

Library rt.model.schedule.global.basic.platform

Library rt.model.schedule.global.basic.interference

Library rt.model.schedule.global.jitter.schedule

Library rt.model.schedule.global.jitter.constrained_deadlines

Library rt.model.schedule.global.jitter.interference_edf

Library rt.model.schedule.global.jitter.job

Library rt.model.schedule.global.jitter.platform

Library rt.model.schedule.global.jitter.interference

Library rt.model.schedule.apa.constrained_deadlines

Library rt.model.schedule.apa.interference_edf

Library rt.model.schedule.apa.affinity

Library rt.model.schedule.apa.platform

Library rt.model.schedule.apa.interference

Library rt.model.schedule.uni.schedule

Library rt.model.schedule.uni.schedulability

Library rt.model.schedule.uni.susp.schedule

Library rt.model.schedule.uni.susp.suspension_intervals

Library rt.model.schedule.uni.susp.last_execution

Library rt.model.schedule.uni.susp.platform

Library rt.model.schedule.uni.susp.valid_schedule

Library rt.model.schedule.uni.susp.build_suspension_table

Library rt.model.schedule.uni.end_time

Library rt.model.schedule.uni.nonpreemptive.schedule

Library rt.model.schedule.uni.nonpreemptive.platform

Library rt.model.schedule.uni.workload

Library rt.model.schedule.uni.service

Library rt.model.schedule.uni.limited.rbf

Library rt.model.schedule.uni.limited.schedule

Library rt.model.schedule.uni.limited.busy_interval

• Busy Interval for JLFP-models

Library rt.model.schedule.uni.limited.platform.nonpreemptive

• Platform for fully nonpreemptive model

Library rt.model.schedule.uni.limited.platform.definitions

• Platform with limited preemptions

Library rt.model.schedule.uni.limited.platform.limited

• Platform for models with limited preemptions

Library rt.model.schedule.uni.limited.platform.priority_inversion_is_bounded

• Priority inversion is bounded

Library rt.model.schedule.uni.limited.platform.preemptive

• Platform for fully premptive model

Library rt.model.schedule.uni.limited.platform.util

• Non-decreasing sequence

Library rt.model.schedule.uni.limited.edf.response_time_bound

• Abstract RTA for EDF-schedulers
  • Filling Out Hypothesis Of Abstract RTA Theorem
  • Final Theorem

Library rt.model.schedule.uni.limited.edf.nonpr_reg.concrete_models.response_time_bound

• RTA for concrete models
• RTA for fully preemptive EDF model
• RTA for fully nonpreemptive EDF model
• RTA for EDF with fixed premption points
• RTA for EDF with floating nonpreemptive regions

Library rt.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound

• RTA for EDF-schedulers with bounded nonpreemprive segments
  • Priority inversion is bounded
  • Response-Time Bound

Library rt.model.schedule.uni.limited.jlfp_instantiation

• JLFP instantiation of Interference and Interfering Workload
  • Interference and Interfering Workload
  • Equivalences

Library rt.model.schedule.uni.limited.fixed_priority.response_time_bound

• Abstract RTA for FP-schedulers
  • Filling Out Hypotheses Of Abstract RTA Theorem
  • Final Theorem

Library rt.model.schedule.uni.limited.fixed_priority.nonpr_reg.concrete_models.response_time_bound

• RTA for concrete models
• RTA for fully preemptive FP model
• RTA for fully nonpreemptive FP model
• RTA for FP-schedulers with fixed premption points
• RTA for FP-schedulers with floating nonpreemptive regions

Library rt.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound

• RTA for FP-schedulers with bounded nonpreemptive segments
  • Priority inversion is bounded
  • Response-Time Bound

Library rt.model.schedule.uni.limited.abstract_RTA.definitions

• Definitions for Abstract Response-Time Analysis

Library rt.model.schedule.uni.limited.abstract_RTA.abstract_rta

• Abstract Response-Time Analysis

Library rt.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space

• Reduction of the serach space for Abstract RTA

Library rt.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta

• Abstract Response-Time Analysis with sequential jobs

Library rt.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service

• Lock-in service of a job

Library rt.model.schedule.uni.transformation.construction

Library rt.model.schedule.uni.response_time

Library rt.model.schedule.uni.basic.platform

Library rt.model.schedule.uni.basic.platform_tdma

Library rt.model.schedule.uni.jitter.schedule

Library rt.model.schedule.uni.jitter.busy_interval

Library rt.model.schedule.uni.jitter.platform

Library rt.model.schedule.uni.jitter.valid_schedule

Library rt.model.schedule.uni.schedule_of_task

Library rt.model.schedule.uni.sustainability

Library rt.model.time

Library rt.model.policy_tdma

Library rt.model.arrival.curves.bounds

Library rt.model.arrival.basic.arrival_sequence

Library rt.model.arrival.basic.arrival_bounds

Library rt.model.arrival.basic.task_arrival

Library rt.model.arrival.basic.job

Library rt.model.arrival.basic.task

Library rt.model.arrival.jitter.arrival_sequence

Library rt.model.arrival.jitter.arrival_bounds

Library rt.model.arrival.jitter.task_arrival

Library rt.model.arrival.jitter.job

Library rt.util.powerset

Library rt.util.find_seq

Library rt.util.bigord

Library rt.util.counting

Library rt.util.fixedpoint

Library rt.util.notation

Library rt.util.minmax

Library rt.util.induction

Library rt.util.seqset

Library rt.util.list

Library rt.util.tactics

• Very basic automation
• Equality types
• Basic simplification tactics
  • Delineating cases in proofs
  • Exploiting a hypothesis
• New tactics for ssreflect

Library rt.util.bigcat

Library rt.util.step_function

Library rt.util.all

Library rt.util.div_mod

Library rt.util.search_arg

Library rt.util.ord_quantifier

Library rt.util.epsilon

Library rt.util.ssromega

Library rt.util.pick

Library rt.util.sum

Library rt.util.sorting

• Sorting

Library rt.util.rewrite_facilities

• Rewriting

Library rt.util.nat

Library rt.analysis.global.parallel.interference_bound

Library rt.analysis.global.parallel.bertogna_fp_comp

Library rt.analysis.global.parallel.bertogna_edf_comp

Library rt.analysis.global.parallel.bertogna_edf_theory

Library rt.analysis.global.parallel.interference_bound_edf

Library rt.analysis.global.parallel.bertogna_fp_theory

Library rt.analysis.global.parallel.workload_bound

Library rt.analysis.global.parallel.interference_bound_fp

Library rt.analysis.global.basic.interference_bound

Library rt.analysis.global.basic.bertogna_fp_comp

Library rt.analysis.global.basic.bertogna_edf_comp

Library rt.analysis.global.basic.bertogna_edf_theory

Library rt.analysis.global.basic.interference_bound_edf

Library rt.analysis.global.basic.bertogna_fp_theory

Library rt.analysis.global.basic.workload_bound

Library rt.analysis.global.basic.interference_bound_fp

Library rt.analysis.global.jitter.interference_bound

Library rt.analysis.global.jitter.bertogna_fp_comp

Library rt.analysis.global.jitter.bertogna_edf_comp

Library rt.analysis.global.jitter.bertogna_edf_theory

Library rt.analysis.global.jitter.interference_bound_edf

Library rt.analysis.global.jitter.bertogna_fp_theory

Library rt.analysis.global.jitter.workload_bound

Library rt.analysis.global.jitter.interference_bound_fp

Library rt.analysis.apa.interference_bound

Library rt.analysis.apa.bertogna_fp_comp

Library rt.analysis.apa.bertogna_edf_comp

Library rt.analysis.apa.bertogna_edf_theory

Library rt.analysis.apa.interference_bound_edf

Library rt.analysis.apa.bertogna_fp_theory

Library rt.analysis.apa.workload_bound

Library rt.analysis.apa.interference_bound_fp

Library rt.analysis.uni.arrival_curves.workload_bound

Library rt.analysis.uni.susp.sustainability.singlecost.reduction_properties

Library rt.analysis.uni.susp.sustainability.singlecost.reduction

Library rt.analysis.uni.susp.sustainability.allcosts.main_claim

Library rt.analysis.uni.susp.sustainability.allcosts.reduction_properties

Library rt.analysis.uni.susp.sustainability.allcosts.reduction

Library rt.analysis.uni.susp.dynamic.oblivious.reduction

Library rt.analysis.uni.susp.dynamic.oblivious.fp_rta

Library rt.analysis.uni.susp.dynamic.jitter.rta_by_reduction

• • • • Main Claim

Library rt.analysis.uni.susp.dynamic.jitter.taskset_rta

Library rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation

Library rt.analysis.uni.susp.dynamic.jitter.taskset_membership

Library rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_service

• • 6-(A) Less High-Priority Service Before the Arrival of Job j in sched_jitter
    • • Main Claim of Section (A)
  • 6-(B) More High-Priority Service After the Arrival of Job j in sched_jitter
    • • Main Claim of Section (B)
  • 6-(C) Conclusion: Comparing Response Times of Job j
    • • Main Claim of Section (C)

Library rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties

Library rt.analysis.uni.susp.dynamic.jitter.jitter_schedule

Library rt.analysis.uni.basic.tdma_rta_theory

Library rt.analysis.uni.basic.fp_rta_comp

Library rt.analysis.uni.basic.workload_bound_fp

Library rt.analysis.uni.basic.tdma_wcrt_analysis

Library rt.analysis.uni.basic.fp_rta_theory

Library rt.analysis.uni.jitter.fp_rta_comp

Library rt.analysis.uni.jitter.workload_bound_fp

Library rt.analysis.uni.jitter.fp_rta_theory

Library rt.restructuring.model.preemption.preemption_model

• Platform with limited preemptions

Library rt.restructuring.model.schedule.work_conserving

Library rt.restructuring.model.schedule.edf

Library rt.restructuring.model.schedule.tdma.tdma_facts

Library rt.restructuring.model.schedule.tdma.tdma

Library rt.restructuring.model.schedule.sequential

Library rt.restructuring.model.schedule.priority_based.priorities

Library rt.restructuring.model.schedule.priority_based.preemptive

Library rt.restructuring.model.processor.multiprocessor

Library rt.restructuring.model.processor.ideal

Library rt.restructuring.model.processor.varspeed

Library rt.restructuring.model.processor.platform_properties

Library rt.restructuring.model.processor.spin

Library rt.restructuring.model.job

Library rt.restructuring.model.readiness.basic

Library rt.restructuring.model.readiness.jitter

Library rt.restructuring.model.task

Library rt.restructuring.model.aggregate.service_of_jobs

• Service Received by Sets of Jobs

Library rt.restructuring.model.aggregate.workload

• Workload of Sets of Jobs

Library rt.restructuring.model.aggregate.task_arrivals

Library rt.restructuring.model.arrival.arrival_curves

Library rt.restructuring.model.arrival.sporadic

Library rt.restructuring.behavior.schedule

Library rt.restructuring.behavior.arrival_sequence

Library rt.restructuring.behavior.all

Library rt.restructuring.behavior.ready

Library rt.restructuring.behavior.service

Library rt.restructuring.behavior.job

Library rt.restructuring.behavior.time

Library rt.restructuring.analysis.transform.prefix

Library rt.restructuring.analysis.transform.edf_trans

Library rt.restructuring.analysis.transform.swap

Library rt.restructuring.analysis.transform.facts.edf_opt

Library rt.restructuring.analysis.transform.facts.swaps

Library rt.restructuring.analysis.transform.facts.replace_at

Library rt.restructuring.analysis.schedulability

Library rt.restructuring.analysis.edf.optimality

Library rt.restructuring.analysis.workload

• Lemmas about Workload of Sets of Jobs

Library rt.restructuring.analysis.task_schedule

• Schedule of task

Library rt.restructuring.analysis.abstract.core.definitions

• Definitions for Abstract Response-Time Analysis

Library rt.restructuring.analysis.abstract.core.abstract_rta

• Abstract Response-Time Analysis

Library rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold

• Run-to-Completion Threshold of a job

Library rt.restructuring.analysis.abstract.core.reduction_of_search_space

• Reduction of the serach space for Abstract RTA

Library rt.restructuring.analysis.abstract.core.abstract_seq_rta

• Abstract Response-Time Analysis with sequential jobs

Library rt.restructuring.analysis.abstract.core.run_to_completion_threshold

• Run-to-completion threshold

Library rt.restructuring.analysis.basic_facts.deadlines

Library rt.restructuring.analysis.basic_facts.ideal_schedule

Library rt.restructuring.analysis.basic_facts.service_of_jobs

• Lemmas about Service Received by Sets of Jobs

Library rt.restructuring.analysis.basic_facts.completion

• necessarily receive service, we can conclude that scheduled jobs have
• remaining positive cost.

Library rt.restructuring.analysis.basic_facts.all

Library rt.restructuring.analysis.basic_facts.service

Library rt.restructuring.analysis.basic_facts.arrivals

Library rt.restructuring.analysis.basic_facts.task_arrivals

Library rt.restructuring.analysis.basic_facts.sequential

Library rt.restructuring.analysis.arrival.rbf

• Request Bound Functions (RBF)

Library rt.restructuring.analysis.arrival.workload_bound

• Task Workload Bounded by Arrival Curves