Search Results

Documents authored by Rieg, Lionel

Document
DOI: 10.4230/LIPIcs.ECRTS.2025.19
Revisiting Timing Anomalies in Predictable In-Order Pipelines

Authors: Lilia Rouizi, Mihail Asavoae, Benjamin Binder, Lionel Rieg, and Florian Brandner

Published in: LIPIcs, Volume 335, 37th Euromicro Conference on Real-Time Systems (ECRTS 2025)

Abstract
The quality of timing guarantees ensured through worst-case-execution time analysis and schedulability tests - required to be both sound and precise - is directly influenced by the predictability properties of the execution platform. A platform is considered predictable when safe and precise bounds can be computed through analysis tools. Counter-intuitive and Amplification Timing Anomalies (TAs) are detrimental to predictability and thus may make it much harder/impossible to compute such bounds. In order to address this issue, research has followed two orthogonal approaches, (i) designing predictable execution platforms and (ii) characterizing counter-intuitive TAs through formal definitions. However, predictable designs rarely apply any formal definitions of timing anomalies. This paper aims at investigating precisely this relationship. We first show how a previously proposed definition of counter-intuitive TAs can be applied to the predictable in-order processor SIC. We then extend this approach in order to provide the first formal definition of both counter-intuitive and amplification effects. The proposed definitions are then evaluated on a regular in-order processor as well as the predictable SIC core using a systematic approach that allows to assess their applicability and relevance. Finally, we prove, for the first time, the absence of some, but not all, TA effects in SIC.
Cite as

Lilia Rouizi, Mihail Asavoae, Benjamin Binder, Lionel Rieg, and Florian Brandner. Revisiting Timing Anomalies in Predictable In-Order Pipelines. In 37th Euromicro Conference on Real-Time Systems (ECRTS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 335, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rouizi_et_al:LIPIcs.ECRTS.2025.19,
  author =	{Rouizi, Lilia and Asavoae, Mihail and Binder, Benjamin and Rieg, Lionel and Brandner, Florian},
  title =	{{Revisiting Timing Anomalies in Predictable In-Order Pipelines}},
  booktitle =	{37th Euromicro Conference on Real-Time Systems (ECRTS 2025)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-377-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{335},
  editor =	{Mancuso, Renato},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2025.19},
  URN =		{urn:nbn:de:0030-drops-235974},
  doi =		{10.4230/LIPIcs.ECRTS.2025.19},
  annote =	{Keywords: Timing Anomalies, Causality, Timing Predictability, Timing Analysis}
}
Document
DOI: 10.4230/LITES.10.1.2
Towards a Coq-verified Chain of Esterel Semantics

Authors: Lionel Rieg and Gérard Berry

Published in: LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1

Abstract
This article focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel’s circuit semantics used by compilers to generate software code and hardware designs. The article also comes with formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics, except for the loop construct of Esterel.
Cite as

Lionel Rieg and Gérard Berry. Towards a Coq-verified Chain of Esterel Semantics. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 2:1-2:54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{rieg_et_al:LITES.10.1.2,
  author =	{Rieg, Lionel and Berry, G\'{e}rard},
  title =	{{Towards a Coq-verified Chain of Esterel Semantics}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{2:1--2:54},
  ISSN =	{2199-2002},
  year =	{2025},
  volume =	{10},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.2},
  URN =		{urn:nbn:de:0030-drops-230144},
  doi =		{10.4230/LITES.10.1.2},
  annote =	{Keywords: Esterel programming language, formal verification, Coq proof assistant}
}
Document
DOI: 10.4230/LITES.8.2.2
Swarms of Mobile Robots: Towards Versatility with Safety

Authors: Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.
Cite as

Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{courtieu_et_al:LITES.8.2.2,
  author =	{Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
  title =	{{Swarms of Mobile Robots: Towards Versatility with Safety}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:36},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.2},
  URN =		{urn:nbn:de:0030-drops-192942},
  doi =		{10.4230/LITES.8.2.2},
  annote =	{Keywords: distributed algorithm, mobile autonomous robots, formal proof}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.597
Extracting Herbrand trees in classical realizability using forcing

Authors: Lionel Rieg

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
Krivine presented in [Krivine, 2011] a methodology to combine Cohen's forcing with the theory of classical realizability and showed that the forcing condition can be seen as a reference that is not subject to backtracks. The underlying classical program transformation was then analyzed by Miquel [Miquel, 2011] in a fully typed setting in classical higher-order arithmetic (PA-omega^+). As a case study of this methodology, we present a method to extract a Herbrand tree from a classical realizer of inconsistency, following the ideas underlying the completeness theorem and the proof of Herbrand's theorem. Unlike the traditional proof based on König's lemma (using a fixed enumeration of atomic formulas), our method is based on the introduction of a particular Cohen real. It is formalized as a proof in PA-omega^+, making explicit the construction of generic sets in this framework in the particular case where the set of forcing conditions is arithmetical. We then analyze the algorithmic content of this proof.
Cite as

Lionel Rieg. Extracting Herbrand trees in classical realizability using forcing. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 597-614, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{rieg:LIPIcs.CSL.2013.597,
  author =	{Rieg, Lionel},
  title =	{{Extracting Herbrand trees in classical realizability using forcing}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{597--614},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.597},
  URN =		{urn:nbn:de:0030-drops-42212},
  doi =		{10.4230/LIPIcs.CSL.2013.597},
  annote =	{Keywords: classical realizability, forcing, Curry-Howard correspondence, Herbrand trees}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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