rt.model.basic.time: Definition of time.rt.model.basic.arrival_sequence: Definition and lemmas about arrival sequences.rt.model.basic.schedule: Definitions and lemmas about schedules.rt.model.basic.job: Definition of a valid job.rt.model.basic.task: Definition of a valid task.rt.model.basic.response_time: Definitions and lemmas about response-time bounds.rt.model.basic.schedulability: Definitions and lemmas about deadline misses.rt.model.basic.priority: Definitions and lemmas about priorities.rt.model.basic.task_arrival: Definition of task arrival models.rt.model.basic.platform: Definitions and lemmas about the processor platform.rt.model.basic.constrained_deadlines: Lemmas about the processor platform under constrained deadlines.rt.model.basic.workload: Definitions and lemmas about workload.rt.model.basic.interference: Definitions and lemmas about interference.rt.model.basic.interference_edf: Lemmas about interference in EDF-scheduled systems.rt.analysis.basic.workload_bound: Definition and proof of correctness of the workload bound.rt.analysis.basic.interference_bound: Definition of the generic interference bound.rt.analysis.basic.interference_bound_fp: Definition of the interference bound for FP scheduling.rt.analysis.basic.interference_bound_edf: Definition and proof of correctness of the EDF-specific interference bound.rt.analysis.basic.bertogna_fp_theory: Proof that any fixed point in the FP RTA is a safe response-time bound.rt.analysis.basic.bertogna_fp_comp: Definition and proofs of correctness and termination of the FP RTA.rt.analysis.basic.bertogna_edf_comp: Definition and proofs of correctness and termination of the EDF RTA.rt.analysis.basic.bertogna_edf_theory: Proof that any fixed point in the EDF RTA is a safe response-time bound.rt.implementation.basic.job: Implementation of a job.rt.implementation.basic.task: Implementation of a real-time task.rt.implementation.basic.arrival_sequence: Implementation of a periodic arrival sequence.rt.implementation.basic.schedule: Implementation of a work-conserving scheduler.rt.implementation.basic.bertogna_edf_example: Example of applying the EDF RTA to a task set with 3 tasks.rt.implementation.basic.bertogna_fp_example: Example of applying the FP RTA to a task set with 3 tasks.rt.model.jitter.time: Definition of time.rt.model.jitter.arrival_sequence: Definition and lemmas about arrival sequences.rt.model.jitter.schedule: Definitions and lemmas about schedules with jitter.rt.model.jitter.job: Definition of a valid job with jitter.rt.model.jitter.task: Definition of a valid task with jitter.rt.model.jitter.response_time: Definitions and lemmas about response-time bounds.rt.model.jitter.schedulability: Definitions and lemmas about deadline misses.rt.model.jitter.priority: Definitions and lemmas about priorities.rt.model.jitter.task_arrival: Definition of task arrival models.rt.model.jitter.platform: Definitions and lemmas about the processor platform.rt.model.jitter.constrained_deadlines: Lemmas about the processor platform under constrained deadlines.rt.model.jitter.workload: Definitions and lemmas about workload.rt.model.jitter.interference: Definitions and lemmas about interference.rt.model.jitter.interference_edf: Lemmas about interference in EDF-scheduled systems.rt.analysis.jitter.workload_bound: Definition and proof of correctness of the jitter-aware workload bound.rt.analysis.jitter.interference_bound: Definition of the generic jitter-aware interference bound.rt.analysis.jitter.interference_bound_fp: Definition of the jitter-aware interference bound for FP scheduling.rt.analysis.jitter.interference_bound_edf: Definition and proof of correctness of the jitter-aware EDF-specific interference bound.rt.analysis.jitter.bertogna_fp_theory: Proof that any fixed point in the jitter-aware FP RTA is a safe response-time bound.rt.analysis.jitter.bertogna_fp_comp: Definition and proofs of correctness and termination of the jitter-aware FP RTA.rt.analysis.jitter.bertogna_edf_comp: Definition and proofs of correctness and termination of the jitter-aware EDF RTA.rt.analysis.jitter.bertogna_edf_theory: Proof that any fixed point in the jitter-aware EDF RTA is a safe response-time bound.rt.implementation.jitter.job: Implementation of a job with jitter.rt.implementation.jitter.task: Implementation of a real-time task with jitter.rt.implementation.jitter.arrival_sequence: Implementation of a periodic arrival sequence for jobs with jitter.rt.implementation.jitter.schedule: Implementation of a jitter-aware scheduler.rt.implementation.jitter.bertogna_edf_example: Example of applying the jitter-aware EDF RTA to a task set with 3 tasks.rt.implementation.jitter.bertogna_fp_example: Example of applying the jitter-aware FP RTA to a task set with 3 tasks.rt.analysis.parallel.workload_bound: Definition and proof of correctness of the workload bound for parallel jobs.rt.analysis.parallel.interference_bound: Definition of the generic interference bound for parallel jobs.rt.analysis.parallel.interference_bound_fp: Definition of the interference bound for FP scheduling for parallel jobs.rt.analysis.parallel.interference_bound_edf: Definition and proof of correctness of the EDF-specific interference bound for parallel jobs.rt.analysis.parallel.bertogna_fp_theory: Proof that any fixed point in the FP RTA for parallel jobs is a safe response-time bound.rt.analysis.parallel.bertogna_fp_comp: Definition and proofs of correctness and termination of the FP RTA for parallel jobs.rt.analysis.parallel.bertogna_edf_comp: Definition and proofs of correctness and termination of the EDF RTA for parallel jobs.rt.analysis.parallel.bertogna_edf_theory: Proof that any fixed point in the EDF RTA for parallel jobs is a safe response-time bound.To test this analysis, we reuse the scheduler implementation for sequential jobs (a particular case of parallelism).
rt.implementation.jitter.bertogna_edf_example: Example of applying the EDF RTA for parallel jobs to a task set with 3 tasks.rt.implementation.jitter.bertogna_fp_example: Example of applying the FP RTA for parallel jobs to a task set with 3 tasks.rt.model.apa.time: Definition of time.rt.model.apa.arrival_sequence: Definition and lemmas about arrival sequences.rt.model.apa.schedule: Definitions and lemmas about schedules.rt.model.apa.job: Definition of a valid job.rt.model.apa.task: Definition of a valid task.rt.model.apa.affinity: Definition of a processor affinity.rt.model.apa.response_time: Definitions and lemmas about response-time bounds.rt.model.apa.schedulability: Definitions and lemmas about deadline misses.rt.model.apa.priority: Definitions and lemmas about priorities.rt.model.apa.task_arrival: Definition of task arrival models.rt.model.apa.platform: Definitions and lemmas about the processor platform.rt.model.apa.constrained_deadlines: Lemmas about the processor platform under constrained deadlines.rt.model.apa.workload: Definitions and lemmas about workload.rt.model.apa.interference: Definitions and lemmas about interference.rt.model.apa.interference_edf: Lemmas about interference in EDF-scheduled systems.rt.analysis.apa.workload_bound: Definition and proof of correctness of the workload bound.rt.analysis.apa.interference_bound: Definition of the generic interference bound.rt.analysis.apa.interference_bound_fp: Definition of the interference bound for FP scheduling.rt.analysis.apa.interference_bound_edf: Definition and proof of correctness of the EDF-specific interference bound.rt.analysis.apa.bertogna_fp_theory: Proof that any fixed point in the FP RTA is a safe response-time bound.rt.analysis.apa.bertogna_fp_comp: Definition and proofs of correctness and termination of the FP RTA.rt.analysis.apa.bertogna_edf_comp: Definition and proofs of correctness and termination of the EDF RTA.rt.analysis.apa.bertogna_edf_theory: Proof that any fixed point in the EDF RTA is a safe response-time bound.rt.implementation.apa.job: Implementation of a job.rt.implementation.apa.task: Implementation of a real-time task with processor affinities.rt.implementation.apa.arrival_sequence: Implementation of a periodic arrival sequence.rt.implementation.apa.schedule: Implementation of a work-conserving APA scheduler.rt.implementation.apa.bertogna_edf_example: Example of applying the APA-reduction of the EDF RTA to a task set with 3 tasks.rt.implementation.apa.bertogna_fp_example: Example of applying the APA-reduction of the FP RTA to a task set with 3 tasks.rt.util.notation: Customized notations for increasing readability.rt.util.tactics: Set of tactics used in our development.rt.util.divround: Definition of floor and ceiling of integer division.rt.util.nat: Additional lemmas about natural numbers and arithmetic.rt.util.induction: Lemmas about induction on natural numbers.rt.util.fixedpoint: Lemmas about fixed point iterations.rt.util.ssromega: Adaptation of the Omega tactic for ssreflect.rt.util.bigcat: Lemmas about the big concatenation operator.rt.util.list: Additional lemmas about lists.rt.util.seqset: Definition of a set as a list without duplicates.rt.util.powerset: Definition and lemmas about power sets.rt.util.sorting: Additional lemmas about sorting.rt.util.bigord: Lemmas about big operators involving Ordinal functions.rt.util.ord_quantifier: Lemmas about [exists, …] and [forall, …] from ssreflect.rt.util.sum: Additional lemmas about summation.rt.util.counting: Additional lemmas about counting.rt.util.all: Compilation of all the other utility libraries.