Verification of OS-level cache management
MetadataShow full item record
Citation (published version)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)
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.