Identifying Timing Interferences on Multicore Processors

Organisation:	IRT Saint Exupéry, Toulouse and INRIA Grenoble / CONVECS team (FRANCE)
Method:	LNT MCL
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Hardware Design.
Period:	2020
Size:	n/a
Description:	Multi-core platforms are suitable for the implementation of critical real-time systems as they provide the computational power required by embedded applications while maintaining an acceptable energy consumption. However, the correctness of hard real-time systems implemented on multi-core platforms is difficult to establish, since it depends both on the correctness of the computations and on the compliance with various temporal constraints (sampling time, worst-case response times, data aging, etc.). Given that hardware resources are shared between cores, estimating the Worst-Case Execution Times (WCET) of tasks deployed on multiple cores is challenging, since the execution of a task on a core may impact the timing behavior of the tasks executing in parallel on other cores. Therefore, a reasonable WCET estimation requires to identify the sources of such interferences and take their effects into account. This work proposes a method to automate the detection of temporal interferences (i.e., situations where the execution time of a task changes due to the presence of other tasks running on other cores) using formal methods and verification. The first step is to build two behavioural models of the software application and execution platform in the LNT language: an isolated model (with only one core enabled, and thus interference-free) and a non-isolated model (with all cores enabled, and thus containing interferences). The interferences manifest as differences between the execution traces generated from these two behavioral models. Two solutions are proposed to detect these differences: PATCHECK defines interferences as specific trace patterns, describes them in the MCL language, and uses the model checker of CADP to detect their presence on traces generated from the non-isolated model; SYNCHECK compares the traces obtained from the isolated and non-isolated models by computing a specific synchronous product using the EXP.OPEN tool of CADP and checking an MCL formula denoting the presence of interferences in this product. This method was applied to a part of Infineon's AURIX TC275 microcontroller, a System-on-Chip (SoC) containing three in-order execution cores equipped with private local memories for program and data. Each core has two memory interfaces: a Program Memory Interface (PMI) and a Data Memory Interface (DMI). The SoC's components (cores, memories, IPs) are interconnected via the Shared Resource Interconnection Crossbar Interconnect (XBar SRI) and the System Peripheral Bus (SPB). The interference detection method was successfully applied on several synthetic applications and also on an Integrated Air System Control (IASC) running on AURIX TC275.
Conclusions:	The detection of interferences in real-time applications running on multicore systems can be (partly) automated using behavioral modeling and verification using LNT, MCL, and CADP. The application of the proposed method to a part of the AURIX TC275 platform has shown that the analysis is both safe and able to prevent reporting spurious interferences.
Publications:	[Nguyen-Jenn-Serwe-et-al-20] Viet Anh Nguyen, Eric Jenn, Wendelin Serwe, Frédéric Lang, and Radu Mateescu. Using Model Checking to Identify Timing Interferences on Multicore Processors. Proceedings of the 10th European Congress on Embedded Real Time Software and Systems (ERTS'2020), Toulouse, France, January 29-31, 2020. Available on-line at: https://hal.inria.fr/hal-02462085/en or from the CADP Web site in PDF or PostScript
Contact:	Eric Jenn IRT Saint Exupéry B 612 3 rue Tarfaya, CS 34436 F-31405 Toulouse FRANCE Email: [email protected]
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page