Scalable Computation of Inter-Core Bounds Through Exact Abstractions
Mohammed Foughali, Marius Mikučionis, Maryline Zhang · 2024
A real-time systems (RTS) typically consists of a set of real-time tasks that execute on a multicore platform following a scheduling policy. In an RTS, computing inter-core bounds, i.e., bounds separating events occurring on different cores, is crucial. While efficient techniques to over-approximate such bounds exist, little has been proposed to compute their exact values. Given an RTS with a set of cores$c$and a set of tasks$T$, under partitioned fixed-priority scheduling with limited preemption, a recent work by Foughali, Hladik and Zuepke (FHZ) models tasks with affinity$c$(i.e., allocated to core$c\in C$) as a Uppaaltimed automata (TA) network$N_{C}$. Through compositional model checking, FHZ achieved a substantial gain in scalability for bounds local to a core. However, computing inter-core bounds for some events of interest$E$, produced by a subset of tasks$T_{E}\subseteq T$with different affinities$C_{E}\subseteq C$, requires model checking$N_{E}=\Vert _{c\in C_{E}}N_{c}$, i.e., the parallel composition of all TA networks$N_{c}$for each$c\in C_{E}$, which often produces an intractable state space. In this paper, we present a new scalable approach based on exact abstractions to compute exact inter-core bounds in a schedulable RTS, under the assumption that tasks in$T_{E}$have distinct affinities. We develop a new Uppaalquery, and a novel algorithm that computes, for each TA network$N_{c}$in$N_{1\mathrm{i}}$, an abstraction$\mathcal{A}(N_{c})$preserving the exact intervals within which events occur on$c$. Then, we model check$\mathcal{A}(N_{E})=\Vert _{c\in C_{E}}\mathcal{A}(N_{c})$(instead of$N_{E}$), therefore drastically reducing the state space. We demonstrate the scalability of our approach as we efficiently compute inter-core bounds for the WATERS 2017 industrial challenge, where FHZ fails to scale.