When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECRTS.2019.18
URN: urn:nbn:de:0030-drops-107553
Go to the corresponding LIPIcs Volume Portal

Sensfelder, Nathanaƫl ; Brunel, Julien ; Pagetti, Claire

Modeling Cache Coherence to Expose Interference

LIPIcs-ECRTS-2019-18.pdf (1 MB)


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

  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 =		{},
  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}

Keywords: Real-time systems, multi-core processor, cache coherence, formal methods
Seminar: 31st Euromicro Conference on Real-Time Systems (ECRTS 2019)
Issue Date: 2019
Date of publication: 08.07.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI