2 Search Results for "de Carvalho, Daniel"

Document
DOI: 10.4230/LIPIcs.ECRTS.2020.9
Demystifying the Real-Time Linux Scheduling Latency

Authors: Daniel Bristot de Oliveira, Daniel Casini, Rômulo Silva de Oliveira, and Tommaso Cucinotta

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

Abstract
Linux has become a viable operating system for many real-time workloads. However, the black-box approach adopted by cyclictest, the tool used to evaluate the main real-time metric of the kernel, the scheduling latency, along with the absence of a theoretically-sound description of the in-kernel behavior, sheds some doubts about Linux meriting the real-time adjective. Aiming at clarifying the PREEMPT_RT Linux scheduling latency, this paper leverages the Thread Synchronization Model of Linux to derive a set of properties and rules defining the Linux kernel behavior from a scheduling perspective. These rules are then leveraged to derive a sound bound to the scheduling latency, considering all the sources of delays occurring in all possible sequences of synchronization events in the kernel. This paper also presents a tracing method, efficient in time and memory overheads, to observe the kernel events needed to define the variables used in the analysis. This results in an easy-to-use tool for deriving reliable scheduling latency bounds that can be used in practice. Finally, an experimental analysis compares the cyclictest and the proposed tool, showing that the proposed method can find sound bounds faster with acceptable overheads.
Cite as

Daniel Bristot de Oliveira, Daniel Casini, Rômulo Silva de Oliveira, and Tommaso Cucinotta. Demystifying the Real-Time Linux Scheduling Latency. In 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 165, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{deoliveira_et_al:LIPIcs.ECRTS.2020.9,
  author =	{de Oliveira, Daniel Bristot and Casini, Daniel and de Oliveira, R\^{o}mulo Silva and Cucinotta, Tommaso},
  title =	{{Demystifying the Real-Time Linux Scheduling Latency}},
  booktitle =	{32nd Euromicro Conference on Real-Time Systems (ECRTS 2020)},
  pages =	{9:1--9:23},
  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.9},
  URN =		{urn:nbn:de:0030-drops-123721},
  doi =		{10.4230/LIPIcs.ECRTS.2020.9},
  annote =	{Keywords: Real-time operating systems, Linux kernel, PREEMPT\underlineRT, Scheduling latency}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.41
The Relational Model Is Injective for Multiplicative Exponential Linear Logic

Authors: Daniel de Carvalho

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
We prove a completeness result for Multiplicative Exponential Linear Logic (MELL): we show that the relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized by cut-elimination.
Cite as

Daniel de Carvalho. The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{decarvalho:LIPIcs.CSL.2016.41,
  author =	{de Carvalho, Daniel},
  title =	{{The Relational Model Is Injective for Multiplicative Exponential Linear Logic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{41:1--41:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.41},
  URN =		{urn:nbn:de:0030-drops-65815},
  doi =		{10.4230/LIPIcs.CSL.2016.41},
  annote =	{Keywords: Linear Logic, Denotational semantics, Proof-nets}
}
  • Refine by Author
  • 1 Casini, Daniel
  • 1 Cucinotta, Tommaso
  • 1 de Carvalho, Daniel
  • 1 de Oliveira, Daniel Bristot
  • 1 de Oliveira, Rômulo Silva

  • Refine by Classification
  • 1 Computer systems organization → Real-time operating systems

  • Refine by Keyword
  • 1 Denotational semantics
  • 1 Linear Logic
  • 1 Linux kernel
  • 1 PREEMPT_RT
  • 1 Proof-nets
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2016
  • 1 2020

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