2 Search Results for "Bédin, Denis"

Document
DOI: 10.4230/LIPIcs.DISC.2021.11
Wait-Free CAS-Based Algorithms: The Burden of the Past

Authors: Denis Bédin, François Lépine, Achour Mostéfaoui, Damien Perez, and Matthieu Perrin

Published in: LIPIcs, Volume 209, 35th International Symposium on Distributed Computing (DISC 2021)

Abstract
Herlihy proved that CAS is universal in the classical computing system model composed of an a priori known number of processes. This means that CAS can implement, together with reads and writes, any object with a sequential specification. For this, he proposed the first universal construction capable of emulating any data structure. It has recently been proved that CAS is still universal in the infinite arrival computing model, a model where any number of processes can be created on the fly (e.g. multi-threaded systems). In this paper, we prove that CAS does not allow to implement wait-free and linearizable visible objects in the infinite model with a space complexity bounded by the number of active processes (i.e. ones that have operations in progress on this object). This paper also shows that this lower bound is tight, in the sense that this dependency can be made as low as desired (e.g. logarithmic) by proposing a wait-free and linearizable universal construction, using the compare-and-swap operation, whose space complexity in the number of ever issued operations is defined by a parameter that can be linked to any unbounded function.
Cite as

Denis Bédin, François Lépine, Achour Mostéfaoui, Damien Perez, and Matthieu Perrin. Wait-Free CAS-Based Algorithms: The Burden of the Past. In 35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bedin_et_al:LIPIcs.DISC.2021.11,
  author =	{B\'{e}din, Denis and L\'{e}pine, Fran\c{c}ois and Most\'{e}faoui, Achour and Perez, Damien and Perrin, Matthieu},
  title =	{{Wait-Free CAS-Based Algorithms: The Burden of the Past}},
  booktitle =	{35th International Symposium on Distributed Computing (DISC 2021)},
  pages =	{11:1--11:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-210-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{209},
  editor =	{Gilbert, Seth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021.11},
  URN =		{urn:nbn:de:0030-drops-148131},
  doi =		{10.4230/LIPIcs.DISC.2021.11},
  annote =	{Keywords: Compare-And-Swap, Concurrent Object, Infinite arrival model, Linearizability, Memory complexity, Multi-Threaded Systems, Shared-Memory, Universality, Wait-freedom}
}
Document
DOI: 10.4230/OASIcs.PPES.2011.59
Towards Formally Verified Optimizing Compilation in Flight Control Software

Authors: Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris

Published in: OASIcs, Volume 18, Bringing Theory to Practice: Predictability and Performance in Embedded Systems (2011)

Abstract
This work presents a preliminary evaluation of the use of the CompCert formally specified and verified optimizing compiler for the development of level A critical flight control software. First, the motivation for choosing CompCert is presented, as well as the requirements and constraints for safety-critical avionics software. The main point is to allow optimized code generation by relying on the formal proof of correctness instead of the current un-optimized generation required to produce assembly code structurally similar to the algorithmic language (and even the initial models) source code. The evaluation of its performance (measured using WCET) is presented and the results are compared to those obtained with the currently used compiler. Finally, the paper discusses verification and certification issues that are raised when one seeks to use CompCert for the development of such critical software.
Cite as

Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Towards Formally Verified Optimizing Compilation in Flight Control Software. In Bringing Theory to Practice: Predictability and Performance in Embedded Systems. Open Access Series in Informatics (OASIcs), Volume 18, pp. 59-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{franca_et_al:OASIcs.PPES.2011.59,
  author =	{Fran\c{c}a, Ricardo Bedin and Favre-Felix, Denis and Leroy, Xavier and Pantel, Marc and Souyris, Jean},
  title =	{{Towards Formally Verified Optimizing Compilation in Flight Control Software}},
  booktitle =	{Bringing Theory to Practice: Predictability and Performance in Embedded Systems},
  pages =	{59--68},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-28-6},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{18},
  editor =	{Lucas, Philipp and Wilhelm, Reinhard},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.PPES.2011.59},
  URN =		{urn:nbn:de:0030-drops-30824},
  doi =		{10.4230/OASIcs.PPES.2011.59},
  annote =	{Keywords: Compiler verification, avionics software, WCET, code optimization}
}
  • Refine by Author
  • 1 Bédin, Denis
  • 1 Favre-Felix, Denis
  • 1 França, Ricardo Bedin
  • 1 Leroy, Xavier
  • 1 Lépine, François
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Dependable and fault-tolerant systems and networks
  • 1 Computer systems organization → Multicore architectures
  • 1 Software and its engineering → Process synchronization
  • 1 Theory of computation → Distributed computing models

  • Refine by Keyword
  • 1 Compare-And-Swap
  • 1 Compiler verification
  • 1 Concurrent Object
  • 1 Infinite arrival model
  • 1 Linearizability
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2011
  • 1 2021

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 Imprint Privacy Contact