License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECRTS.2019.18
URN: urn:nbn:de:0030-drops-107553
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10755/
Sensfelder, Nathanaël ;
Brunel, Julien ;
Pagetti, Claire
Modeling Cache Coherence to Expose Interference
Abstract
To facilitate programming, most multi-core processors feature automated mechanisms maintaining coherence between each core's cache. These mechanisms introduce interference, that is, delays caused by concurrent access to a shared resource. This type of interference is hard to predict, leading to the mechanisms being shunned by real-time system designers, at the cost of potential benefits in both running time and system complexity.
We believe that formal methods can provide the means to ensure that the effects of this interference are properly exposed and mitigated. Consequently, this paper proposes a nascent framework relying on timed automata to model and analyze the interference caused by cache coherence.
BibTeX - Entry
@InProceedings{sensfelder_et_al:LIPIcs:2019:10755,
author = {Nathana{\"e}l Sensfelder and Julien Brunel and Claire Pagetti},
title = {{Modeling Cache Coherence to Expose Interference}},
booktitle = {31st Euromicro Conference on Real-Time Systems (ECRTS 2019)},
pages = {18:1--18:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-110-8},
ISSN = {1868-8969},
year = {2019},
volume = {133},
editor = {Sophie Quinton},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10755},
URN = {urn:nbn:de:0030-drops-107553},
doi = {10.4230/LIPIcs.ECRTS.2019.18},
annote = {Keywords: Real-time systems, multi-core processor, cache coherence, formal methods}
}
