Search Results

Documents authored by Sensfelder, Nathanaël

Document
DOI: 10.4230/LIPIcs.ECRTS.2020.13
On How to Identify Cache Coherence: Case of the NXP QorIQ T4240

Authors: Nathanaël Sensfelder, Julien Brunel, and Claire Pagetti

Published in: LIPIcs, Volume 165, 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)

Abstract
Architectures used in safety critical systems have to pass certain certification standards, which require sufficient proof that they will behave as expected. Multi-core processors make this challenging by featuring complex interactions between the tasks they run. A lot of these interactions are made without explicit instructions from the program designers. Furthermore, they can have strong negative impacts on performance (and potentially affect correctness). One important such source of interactions is cache coherence, which speeds up operations in most cases, but can also lead to unexpected variations in execution time if not fully understood. Architecture documentations often lack details on the implementation of cache coherence. We thus propose a strategy to ascertain that the platform does indeed implement the cache coherence protocol its user believes it to. We also apply this strategy to the NXP QorIQ T4240, resulting in the identification of a protocol (MESIF) other than the one this architecture’s documentation led us to believe it was using (MESI).
Cite as

Nathanaël Sensfelder, Julien Brunel, and Claire Pagetti. On How to Identify Cache Coherence: Case of the NXP QorIQ T4240. In 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 165, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{sensfelder_et_al:LIPIcs.ECRTS.2020.13,
  author =	{Sensfelder, Nathana\"{e}l and Brunel, Julien and Pagetti, Claire},
  title =	{{On How to Identify Cache Coherence: Case of the NXP QorIQ T4240}},
  booktitle =	{32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-152-8},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{165},
  editor =	{V\"{o}lp, Marcus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2020.13},
  URN =		{urn:nbn:de:0030-drops-123764},
  doi =		{10.4230/LIPIcs.ECRTS.2020.13},
  annote =	{Keywords: Real-time systems, multi-core processor, cache coherence}
}
Document
Artifact
DOI: 10.4230/DARTS.5.1.7
Modeling Cache Coherence to Expose Interference (Artifact)

Authors: Nathanaël Sensfelder, Julien Brunel, and Claire Pagetti

Published in: DARTS, Volume 5, Issue 1, Special Issue of the 31st Euromicro Conference on Real-Time Systems (ECRTS 2019)

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, we propose a nascent framework relying on timed automata to model and analyze the interference caused by cache coherence.
Cite as

Nathanaël Sensfelder, Julien Brunel, and Claire Pagetti. Modeling Cache Coherence to Expose Interference (Artifact). In Special Issue of the 31st Euromicro Conference on Real-Time Systems (ECRTS 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 1, pp. 7:1-7:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{sensfelder_et_al:DARTS.5.1.7,
  author =	{Sensfelder, Nathana\"{e}l and Brunel, Julien and Pagetti, Claire},
  title =	{{Modeling Cache Coherence to Expose Interference}},
  pages =	{7:1--7:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{1},
  editor =	{Sensfelder, Nathana\"{e}l and Brunel, Julien and Pagetti, Claire},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.1.7},
  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}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2019.18
Modeling Cache Coherence to Expose Interference

Authors: Nathanaël Sensfelder, Julien Brunel, and Claire Pagetti

Published in: LIPIcs, Volume 133, 31st Euromicro Conference on Real-Time Systems (ECRTS 2019)

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.
Cite as

Nathanaël Sensfelder, Julien Brunel, and Claire Pagetti. Modeling Cache Coherence to Expose Interference. In 31st Euromicro Conference on Real-Time Systems (ECRTS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 133, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sensfelder_et_al:LIPIcs.ECRTS.2019.18,
  author =	{Sensfelder, Nathana\"{e}l and Brunel, Julien and Pagetti, Claire},
  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 =	{Quinton, Sophie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2019.18},
  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}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact