Verification of OS-level cache management
Files
Accepted manuscript
Supplemental materials (from published version)
Date
2018-07-01
DOI
Authors
Mancuso, Renato
Chaki, Sagar
Version
Accepted manuscript
OA Version
Citation
Renato Mancuso, Sagar Chaki. 2018. "Verification of OS-level Cache Management." Proceedings of Operating Systems Platforms for Embedded Real-Time Applications. Operating Systems Platforms for Embedded Real-Time Applications (OSPERT)
Abstract
Recently, the complexity of safety-critical cyber-physical systems has spiked due to an increasing demand for performance, impacting both software and hardware layers. The timing behavior of complex systems, however, is harder to analyze. Real-time hardware resource management aims at mitigating this problem, but the proposed solutions often involve OS-level modifications. In this sense, software verification is key to build trust and allow such techniques to be broadly adopted. This paper specifically focuses on CPU cache management, demonstrating that OS-level hardware management logic can be verified at the source code level in a modular way, ie, without verifying the entire OS.