- Basic Definitions
- Arrival Models
- Uniprocessor Scheduling Model
- Global Scheduling Model
- Partitioned Scheduling Model
- APA Scheduling Model
- Schedulability Analysis
- Sustainability
- Implementation
- Utility Library

`rt.model.time:`

Definition of time.`rt.model.priority:`

Definitions and lemmas about priorities.`rt.model.suspension:`

Definition of the suspension model.`rt.model.policy_tdma:`

Definitions related to TDMA policies.

`rt.model.arrival.basic.arrival_sequence:`

Definitions and lemmas about arrival sequences.`rt.model.arrival.basic.job:`

Definition of a valid sporadic job.`rt.model.arrival.basic.task:`

Definition of a valid sporadic task.`rt.model.arrival.basic.task_arrival:`

Definition of the sporadic task model and related lemmas.`rt.model.arrival.basic.arrival_bounds:`

Definition of the bound on the arrival of sporadic jobs with jitter.

`rt.model.arrival.jitter.arrival_sequence:`

Additional definitions about arrival sequences with jitter.`rt.model.arrival.jitter.job:`

Definition of a valid sporadic job with jitter.`rt.model.arrival.jitter.arrival_bounds:`

Definition of the bound on the arrival of sporadic jobs with jitter.`rt.model.arrival.jitter.task_arrival:`

Definition of the sporadic task model for tasks with jitter.

`rt.model.schedule.uni.schedule:`

Definition and lemmas about uniprocessor schedules.`rt.model.schedule.uni.service:`

Definitions and lemmas related to service.`rt.model.schedule.uni.schedulability:`

Definition of deadline miss.`rt.model.schedule.uni.response_time:`

Definitions and lemmas about response-time bounds.`rt.model.schedule.uni.workload:`

Definitions and lemmas about workload.`rt.model.schedule.uni.end_time:`

Definition of completion time.`rt.model.schedule.uni.sustainability:`

Definition of weak and strong sustainability.`rt.model.schedule.uni.schedule_of_task:`

Definitions and lemmas about schedules of sporadic tasks.`rt.model.schedule.uni.transformation.construction:`

Prefix-based construction of a uniprocessor scheduled using a provided algorithm.

`rt.model.schedule.uni.basic.busy_interval:`

Definitions and lemmas about busy intervals.`rt.model.schedule.uni.basic.platform:`

Definition of the platform constraints.`rt.model.schedule.uni.basic.platform_tdma:`

Definitions related to TDMA policies.

`rt.model.schedule.uni.jitter.schedule:`

Extra definitions for schedules with jitter.`rt.model.schedule.uni.jitter.valid_schedule:`

Definition of a valid schedule with jitter.`rt.model.schedule.uni.jitter.platform:`

Platform constraints for schedules with jitter.`rt.model.schedule.uni.jitter.busy_interval:`

Definitions and lemmas related to busy interval in schedules with jitter.

`rt.model.schedule.uni.susp.schedule:`

Extra definitions for schedules of self-suspending tasks.`rt.model.schedule.uni.susp.valid_schedule:`

Notion of valid schedule with suspensions.`rt.model.schedule.uni.susp.suspension_intervals:`

Definition of a suspension interval.`rt.model.schedule.uni.susp.last_execution:`

Definition of the instant after the last execution of a job.`rt.model.schedule.uni.susp.platform:`

Platform constraints for self-suspending tasks.`rt.model.schedule.uni.susp.build_suspension_table:`

Generation of suspension tables using some predicate.

`rt.model.schedule.global.response_time:`

Definitions and lemmas about response-time bounds.`rt.model.schedule.global.schedulability:`

Definitions and lemmas about deadline misses.`rt.model.schedule.global.workload:`

Definitions and lemmas about workload.`rt.model.schedule.global.transformation.construction:`

Prefix-based construction of a global schedule using a provided algorithm.

`rt.model.schedule.global.basic.schedule:`

Definitions and lemmas about schedules.`rt.model.schedule.global.basic.platform:`

Definitions and lemmas about the processor platform.`rt.model.schedule.global.basic.constrained_deadlines:`

Lemmas about the processor platform under constrained deadlines.`rt.model.schedule.global.basic.interference:`

Definitions and lemmas about interference.`rt.model.schedule.global.basic.interference_edf:`

Lemmas about interference in EDF-scheduled systems.

`rt.model.schedule.global.jitter.job:`

Extra definitions about jobs with jitter.`rt.model.schedule.global.jitter.schedule:`

Definitions and lemmas about schedules with jitter.`rt.model.schedule.global.jitter.platform:`

Definitions and lemmas about the processor platform.`rt.model.schedule.global.jitter.interference_edf:`

Lemmas about interference in EDF-scheduled systems.`rt.model.schedule.global.jitter.interference:`

Definitions and lemmas about interference.`rt.model.schedule.global.jitter.constrained_deadlines:`

Lemmas about the processor platform under constrained deadlines.

`rt.model.schedule.partitioned.schedule:`

Definition of partitioned scheduling.`rt.model.schedule.partitioned.schedulability:`

Definitions relating the schedulability of global and partitioned scheduling.

`rt.model.schedule.apa.affinity:`

Definition of a processor affinity.`rt.model.schedule.apa.interference_edf:`

Lemmas about interference in EDF-scheduled systems.`rt.model.schedule.apa.interference:`

Definitions and lemmas about interference.`rt.model.schedule.apa.constrained_deadlines:`

Lemmas about the processor platform under constrained deadlines.`rt.model.schedule.apa.platform:`

Definitions and lemmas about the processor platform.

`rt.analysis.uni.basic.workload_bound_fp:`

Workload bound for sporadic tasks under constrained deadlines.`rt.analysis.uni.basic.fp_rta_theory:`

Proof that any fixed point of the FP RTA gives a response-time bound.`rt.analysis.uni.basic.fp_rta_comp:`

Definition and proofs of correctness and termination of the RTA for sporadic tasks.

`rt.analysis.uni.basic.tdma_rta_theory:`

Proof that any fixed point of the TDMA RTA gives a response-time bound.`rt.analysis.uni.basic.tdma_wcrt_analysis:`

Definition and proofs of correctness and termination of the RTA for TDMA tasks.

`rt.analysis.uni.jitter.workload_bound_fp:`

Workload bound for FP scheduling with constrained deadlines.`rt.analysis.uni.jitter.fp_rta_theory:`

Proof that any fixed point of the FP RTA gives a response-time bound.`rt.analysis.uni.jitter.fp_rta_comp:`

Definition and proofs of correctness and termination of the FP RTA.

`rt.analysis.uni.susp.dynamic.oblivious.reduction:`

Construction of a worse schedule without suspensions by inflating job costs (suspension-oblivious approach).`rt.analysis.uni.susp.dynamic.oblivious.fp_rta:`

Instantiation of the FP RTA for self-suspending tasks based on the suspension-oblivious approach.

`rt.analysis.uni.susp.dynamic.jitter.jitter_schedule:`

Construction of the worse schedule with jitter and no suspensions (jitter-based approach).`rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties:`

Basic properties of the generated schedule with jitter.`rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_service:`

Service-related properties of the generated schedule with jitter.`rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation:`

Construction of a task set with jitter and no suspension times.`rt.analysis.uni.susp.dynamic.jitter.taskset_membership:`

Proof that the generated task set “contains” the generated schedule.`rt.analysis.uni.susp.dynamic.jitter.rta_by_reduction:`

Comparing response-time bounds between the original schedule (with suspensions) and the generated schedule (with jitter and no suspensions).`rt.analysis.uni.susp.dynamic.jitter.taskset_rta:`

Using the reduction to derive a response-time analysis for the task set with suspensions.

`rt.analysis.global.basic.workload_bound:`

Definition and proof of correctness of the workload bound.`rt.analysis.global.basic.interference_bound_fp:`

Definition of the interference bound for FP scheduling.`rt.analysis.global.basic.interference_bound_edf:`

Definition and proof of correctness of the EDF-specific interference bound.`rt.analysis.global.basic.interference_bound:`

Definition of the generic interference bound.`rt.analysis.global.basic.bertogna_fp_theory:`

Proof that any fixed point in the FP RTA is a safe response-time bound.`rt.analysis.global.basic.bertogna_fp_comp:`

Definition and proofs of correctness and termination of the FP RTA.`rt.analysis.global.basic.bertogna_edf_theory:`

Proof that any fixed point in the EDF RTA is a safe response-time bound.`rt.analysis.global.basic.bertogna_edf_comp:`

Definition and proofs of correctness and termination of the EDF RTA.

`rt.analysis.global.jitter.workload_bound:`

Definition and proof of correctness of the jitter-aware workload bound.`rt.analysis.global.jitter.interference_bound_fp:`

Definition of the jitter-aware interference bound for FP scheduling.`rt.analysis.global.jitter.interference_bound_edf:`

Definition and proof of correctness of the jitter-aware EDF-specific interference bound.`rt.analysis.global.jitter.interference_bound:`

Definition of the generic jitter-aware interference bound.`rt.analysis.global.jitter.bertogna_fp_theory:`

Proof that any fixed point in the jitter-aware FP RTA is a safe response-time bound.`rt.analysis.global.jitter.bertogna_fp_comp:`

Definition and proofs of correctness and termination of the jitter-aware FP RTA.`rt.analysis.global.jitter.bertogna_edf_theory:`

Proof that any fixed point in the jitter-aware EDF RTA is a safe response-time bound.`rt.analysis.global.jitter.bertogna_edf_comp:`

Definition and proofs of correctness and termination of the jitter-aware EDF RTA.

`rt.analysis.global.parallel.workload_bound:`

Definition and proof of correctness of the workload bound for parallel jobs.`rt.analysis.global.parallel.interference_bound:`

Definition of the generic interference bound for parallel jobs.`rt.analysis.global.parallel.interference_bound_fp:`

Definition of the interference bound for FP scheduling for parallel jobs.`rt.analysis.global.parallel.interference_bound_edf:`

Definition and proof of correctness of the EDF-specific interference bound for parallel jobs.`rt.analysis.global.parallel.bertogna_fp_theory:`

Proof that any fixed point in the FP RTA for parallel jobs is a safe response-time bound.`rt.analysis.global.parallel.bertogna_fp_comp:`

Definition and proofs of correctness and termination of the FP RTA for parallel jobs`rt.analysis.global.parallel.bertogna_edf_theory:`

Proof that any fixed point in the EDF RTA for parallel jobs is a safe response-time bound.`rt.analysis.global.parallel.bertogna_edf_comp:`

Definition and proofs of correctness and termination of the EDF RTA for parallel jobs.

`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_theory:`

Proof that any fixed point in the EDF RTA is a safe response-time bound.`rt.analysis.apa.bertogna_edf_comp:`

Definition and proofs of correctness and termination of the EDF RTA.

`rt.analysis.uni.susp.sustainability.allcosts.reduction:`

Construction of a schedule with worse costs and variable suspension times.`rt.analysis.uni.susp.sustainability.allcosts.reduction_properties:`

Properties of the generated schedule with worse costs and variable suspension times.`rt.analysis.uni.susp.sustainability.allcosts.main_claim:`

Main claim of weak-sustainability w.r.t. job costs and variable suspension times.`rt.analysis.uni.susp.sustainability.singlecost.reduction:`

Construction of a schedule with worse costs for a single job.`rt.analysis.uni.susp.sustainability.singlecost.reduction_properties:`

Properties of the generated schedule with worse costs for a single job.

`rt.implementation.arrival_sequence:`

Implementation of a periodic arrival sequence.`rt.implementation.task:`

Implementation of a real-time task.`rt.implementation.job:`

Implementation of a job.

`rt.implementation.uni.basic.schedule:`

Implementation of a work-conserving scheduler.`rt.implementation.uni.basic.fp_rta_example:`

Example of applying the FP RTA to a concrete task set.`rt.implementation.uni.basic.tdma_rta_example:`

Example of applying the FP RTA to a concrete task set.`rt.implementation.uni.basic.schedule_tdma:`

Implementation of a TDMA scheduler.`rt.implementation.uni.basic.extraction_tdma:`

Extraction of the TDMA analysis.

`rt.implementation.uni.jitter.job:`

Implementation of a job with jitter.`rt.implementation.uni.jitter.task:`

Implementation of a real-time task with jitter.`rt.implementation.uni.jitter.schedule:`

Implementation of a work-conserving scheduler with jitter.`rt.implementation.uni.jitter.arrival_sequence:`

Implementation of a periodic arrival sequence.`rt.implementation.uni.jitter.fp_rta_example:`

Example of applying the FP RTA on a concrete task set.

`rt.implementation.uni.susp.dynamic.job:`

Implementation of a job with suspensions.`rt.implementation.uni.susp.dynamic.task:`

Implementation of a real-time task with suspensions.`rt.implementation.uni.susp.dynamic.arrival_sequence:`

Implementation of a periodic arrival sequence.`rt.implementation.uni.susp.schedule:`

Implementation of a work-conserving schedule with suspensions.`rt.implementation.uni.susp.dynamic.oblivious.fp_rta_example:`

Example of applying the FP RTA on concrete self-suspending tasks.

`rt.implementation.global.basic.schedule:`

Implementation of a work-conserving scheduler.`rt.implementation.global.basic.bertogna_edf_example:`

Example of applying the EDF RTA to a task set with 3 tasks.`rt.implementation.global.basic.bertogna_fp_example:`

Example of applying the FP RTA to a task set with 3 tasks.

`rt.implementation.global.jitter.arrival_sequence:`

Implementation of a periodic arrival sequence for jobs with jitter.`rt.implementation.global.jitter.job:`

Implementation of a job with jitter.`rt.implementation.global.jitter.task:`

Implementation of a real-time task with jitter.`rt.implementation.global.jitter.schedule:`

Implementation of a jitter-aware scheduler.`rt.implementation.global.jitter.bertogna_edf_example:`

Example of applying the jitter-aware EDF RTA to a task set with 3 tasks.`rt.implementation.global.jitter.bertogna_fp_example:`

Example of applying the jitter-aware FP RTA to a task set with 3 tasks.

`rt.implementation.global.parallel.bertogna_edf_example:`

Example of applying the EDF RTA for parallel jobs to a task set with 3 tasks.`rt.implementation.global.parallel.bertogna_fp_example:`

Example of applying the FP RTA for parallel jobs to a task set with 3 tasks.

`rt.implementation.apa.arrival_sequence:`

Implementation of a periodic arrival sequence.`rt.implementation.apa.job:`

Implementation of a job.`rt.implementation.apa.schedule:`

Implementation of a work-conserving APA scheduler.`rt.implementation.apa.task:`

Implementation of a real-time task with processor affinities.`rt.implementation.apa.bertogna_edf_example:`

`rt.implementation.apa.bertogna_fp_example:`

`rt.util.notation:`

Customized notations for increasing readability.`rt.util.tactics:`

Set of tactics used in our development.`rt.util.div_mod:`

Definitions and lemmas related to floor/ceil and 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.step_function:`

Lemmas about step functions (e.g. service).`rt.util.minmax:`

Definitions and lemmas about min/max.`rt.util.find_seq:`

Definition of a find operation that can fail.`rt.util.pick:`

Definition of pick operator for lists.`rt.util.counting:`

Additional lemmas about counting.`rt.util.all:`

Compilation of all utility libraries.