Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exact schedulability test for sporadic mixed-criticality real-time systems using antichains and oracles

Simon Picard, Antonio Paolillo, Gilles Geeraerts, Joël Goossens

TL;DR

This work addresses the problem of exact schedulability assessment in uniprocessor mixed-criticality real-time systems with sporadic task sets by means of a finite automaton that has to be explored in order to check for schedulability, and provides a generic algorithm to mitigate the state explosion problem.

Abstract

This work addresses the problem of exact schedulability assessment in uniprocessor mixed-criticality real-time systems with sporadic task sets. We model the problem by means of a finite automaton that has to be explored in order to check for schedulability. To mitigate the state explosion problem, we provide a generic algorithm which is parameterised by several techniques called oracles and simulation relations. These techniques leverage results from the scheduling literature as "plug-ins" that make the algorithm more efficient in practice. Our approach achieves up to a 99.998% reduction in the search space required for exact schedulability testing, making it practical for a range of task sets, up to 8 tasks or maximum periods of 350. This method enables to challenge the pessimism of an existing schedulability test and to derive a new dynamic-priority scheduler, demonstrating its good performance. This is the full version of an RTNS 2024 paper.

Exact schedulability test for sporadic mixed-criticality real-time systems using antichains and oracles

TL;DR

This work addresses the problem of exact schedulability assessment in uniprocessor mixed-criticality real-time systems with sporadic task sets by means of a finite automaton that has to be explored in order to check for schedulability, and provides a generic algorithm to mitigate the state explosion problem.

Abstract

This work addresses the problem of exact schedulability assessment in uniprocessor mixed-criticality real-time systems with sporadic task sets. We model the problem by means of a finite automaton that has to be explored in order to check for schedulability. To mitigate the state explosion problem, we provide a generic algorithm which is parameterised by several techniques called oracles and simulation relations. These techniques leverage results from the scheduling literature as "plug-ins" that make the algorithm more efficient in practice. Our approach achieves up to a 99.998% reduction in the search space required for exact schedulability testing, making it practical for a range of task sets, up to 8 tasks or maximum periods of 350. This method enables to challenge the pessimism of an existing schedulability test and to derive a new dynamic-priority scheduler, demonstrating its good performance. This is the full version of an RTNS 2024 paper.

Paper Structure

This paper contains 17 sections, 11 theorems, 6 equations, 5 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem definition
  3. Automaton based semantic
  4. An efficient algorithm for safety with simulation relation and oracles
  5. A simulation relation and oracles for dual-criticality scheduling
  6. Idle tasks simulation relation
  7. Safe state oracles
  8. Unsafe state oracles
  9. Evaluation
  10. Random task set parameter generation
  11. Antichain impact on state space exploration
  12. Oracle impact
  13. Scheduling analysis
  14. Related Work
  15. Conclusion
  16. ...and 2 more sections

Key Result

Proposition 1

Let $A = \langle V, E, v_0, F \rangle$ be a finite automaton. For all pairs of states $v$ and $v'$ s.t. $v\preccurlyeq v'$, the following holds: (1) if $v$ is unsafe, then $v'$ is unsafe too; (2) if $v'$ is safe, then $v$ is safe too.

Figures (5)

  • Figure 1: $A(\tau^{a}, \mathsf{sch}_{\text{EDF-VD}})$ developed automaton with intermediary transitions. Intermediary states have a dashed outline, and greyed out states are simulated.
  • Figure 2: Example of a fully developed automaton, without intermediary transitions. Greyed out states are simulated.
  • Figure 3: Execution times in seconds before halt for BFS and ACBFS. Dashed line is $x=y$, dotted line is the linear regression on the samples (after $\mathsf{log}_{10}$).
  • Figure 4: \ref{['fig:acbfs-scalability']} ACBFS' median execution times over 40 explorations before halt, with varying number of task and maximum period and a 15 minutes timeout. \ref{['fig:scheduling']} Schedulability ratio over average utilisation per test. Exploration with ACBFS and $\mathsf{HI}$ over demand for exact tests.
  • Figure 5: Oracles' impact on the number of states visited and the execution time.

Theorems & Definitions (52)

  • Definition 1
  • Definition 2: System states
  • Definition 3: Time to deadline
  • Definition 4: Active tasks
  • Definition 5: Eligible task
  • Definition 6: Implicitly completed task
  • Definition 7: Deadline-miss state
  • Definition 8: Scheduler
  • Definition 9: EDF-VD scheduler
  • Definition 10: Release transition
  • ...and 42 more