Empirical evidence for MPSoCs in critical systems: The case of NXP’s T2080 cache coherence

The adoption of complex MPSoCs in critical real-time embedded systems mandates a detailed analysis their architecture to facilitate certification. This analysis is hindered by the lack of a thorough understanding of the MPSoC system due to the unobvious and/or insufficiently documented behavior of some key hardware features. Confidence on those features can only be regained by building specific tests to both, assess whether their behavior matches specifications and unveil their behavior when it is not fully known a priori. In this work, we introduce a systematic approach that constructs this thorough understanding of the MPSoC architecture-- and assess against its specification in processor documentation -- with a focus on the cache coherence protocol in the avionics-relevant NXP T2080 architecture as our use-case. Our approach covers all transitions in the MESI cache coherence protocol, with emphasis on the coherence between DMA and processing cores. We build evidence of their behavior based on available debug support and performance monitors. Our analysis discloses unexpected behavior for coherence-related notifications as well as some hardware monitors. This work has been partially supported by the Spanish Ministry of Science and Innovation under grant PID2019-107255GB; the European Union’s Horizon 2020 research and innovation programme under grant agreement No. 878752 (MASTECS) and the European Research Council (ERC) grant agreement No. 772773 (SuPerCom); the HiPEAC Network of Excellence; and the Natural Sciences and Engineering Research Council of Canada (NSERC).