Publications Memory & Shared-Resource Management
Verification of OS-level Cache Management
14th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT 2018), July 2018, Barcelona, Spain
Abstract
Recently, the complexity of safety-critical cyberphysical 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, i.e., without verifying the entire OS.
Cite this paper
@inproceedings{cl_verif_ospert18,
title = {{Verification of OS-level Cache Management}},
author = {Mancuso, Renato and Chaki, Sagar},
booktitle = {14th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT 2018)},
year = 2018,
month = jul,
address = {Barcelona, Spain},
url = {https://cs-people.bu.edu/rmancuso/files/papers/cl_verif_OSPERT18.pdf}
}
TY - CONF AU - Mancuso, Renato AU - Chaki, Sagar TI - Verification of OS-level Cache Management T2 - 14th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT 2018) PY - 2018 DA - 2018/07// CY - Barcelona, Spain AB - Recently, the complexity of safety-critical cyberphysical 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, i.e., without verifying the entire OS. ER -
%0 Conference Paper %A Mancuso, Renato %A Chaki, Sagar %T Verification of OS-level Cache Management %B 14th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT 2018) %D 2018 %C Barcelona, Spain %X Recently, the complexity of safety-critical cyberphysical 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, i.e., without verifying the entire OS.
[
{
"id": "cl_verif_ospert18",
"type": "paper-conference",
"title": "Verification of OS-level Cache Management",
"author": [
{
"family": "Mancuso",
"given": "Renato"
},
{
"family": "Chaki",
"given": "Sagar"
}
],
"container-title": "14th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT 2018)",
"issued": {
"date-parts": [
[
2018,
7
]
]
},
"publisher-place": "Barcelona, Spain",
"abstract": "Recently, the complexity of safety-critical cyberphysical 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, i.e., without verifying the entire OS."
}
]
R. Mancuso and S. Chaki, “Verification of OS-level Cache Management,” in 14th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT 2018), Jul. 2018.
Mancuso, R., & Chaki, S. (2018). Verification of OS-level Cache Management. In 14th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT 2018).