License: Creative Commons Attribution 3.0 Germany license (CC BY 3.0 DE)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.5.1.7
URN: urn:nbn:de:0030-drops-107358
Go back to Dagstuhl Artifacts Series

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

Modeling Cache Coherence to Expose Interference (Artifact)

DARTS-5-1-7.pdf (0.3 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, we propose 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 (Artifact)}},
  pages =	{7:1--7:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{1},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-107358},
  doi =		{10.4230/DARTS.5.1.7},
  annote =	{Keywords: Real-time systems, multi-core processor, cache coherence, formal methods}

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

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