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.TIME.2020.13
URN: urn:nbn:de:0030-drops-129819
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12981/
Go to the corresponding LIPIcs Volume Portal

Guyomarc'h, Jean ; Guerret, François ; El Mejjati, Bilal ; Ohayon, Emmanuel ; Vincke, Bastien ; Mérigot, Alain

Non-Simultaneity as a Design Constraint

pdf-format:
LIPIcs-TIME-2020-13.pdf (0.6 MB)

Abstract

Whether one or multiple hardware execution units are activated (i.e. CPU cores), invalid resource sharing, notably due to simultaneous accesses, proves to be problematic as it can yield to unexpected runtime behaviors with negative implications such as security or safety issues. The growing interest for off-the-shelf multi-core architectures in sensitive applications motivates the need for safe resources sharing. If critical sections are a well-known solution from imperative and non-temporized programming models, they fail to provide safety guarantees. By leveraging the time-triggered programming model, this paper aims at enforcing that identified critical windows of computations can never be simultaneously executed. We achieve this result by determining, before an application is compiled, the exact dates during which a task accesses a shared resource, which enables the off-line validation of non-simultaneity constraints.

BibTeX - Entry

@InProceedings{guyomarch_et_al:LIPIcs:2020:12981,
  author =	{Jean Guyomarc'h and Fran{\c{c}}ois Guerret and Bilal El Mejjati and Emmanuel Ohayon and Bastien Vincke and Alain M{\'e}rigot},
  title =	{{Non-Simultaneity as a Design Constraint}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{13:1--13:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Emilio Mu{\~n}oz-Velasco and Ana Ozaki and Martin Theobald},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12981},
  URN =		{urn:nbn:de:0030-drops-129819},
  doi =		{10.4230/LIPIcs.TIME.2020.13},
  annote =	{Keywords: Temporal reasoning, Temporal constraints, Specification and verification of systems}
}

Keywords: Temporal reasoning, Temporal constraints, Specification and verification of systems
Collection: 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)
Issue Date: 2020
Date of publication: 15.09.2020
Supplementary Material: The implementation of algorithms is available at https://github.com/krono-safe/mcti-detect/

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