- Sporadic Task Model
- Sporadic Task Model with Release Jitter
- Sporadic Task Model with Parallel Jobs
- Sporadic Task Model with Arbitrary Processor Affinities (APA)
- Utility Library

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