6 Search Results for "Brunel, Julien"

Document
Artifact
DOI: 10.4230/DARTS.8.2.9
Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact)

Authors: Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
This artifact contains a version of MultiCrusty, a Rust library designed for writing and checking communication protocols following the Affine Multiparty Session Types theory introduced in our ECOOP'22 paper. MultiCrusty can work, and should be used, with Scribble [Yoshida et al., 2014] and kMC [{Julien} {Lange} and {Nobuko} {Yoshida}, 2019]: with the former tool, users can write correct global protocols and project them onto local Rust types defined within MultiCrusty, this approach is qualified as top-down; while the latter tool allows to check local Rust types written by users, this approach is qualified as bottom-up. Our artifact contains those three tools, their respective source files, as well as the different examples and benchmarks introduced in our paper, all together within a Docker image.
Cite as

Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{lagaillardie_et_al:DARTS.8.2.9,
  author =	{Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
  title =	{{Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact)}},
  pages =	{9:1--9:16},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.9},
  URN =		{urn:nbn:de:0030-drops-162075},
  doi =		{10.4230/DARTS.8.2.9},
  annote =	{Keywords: Rust language, affine multiparty session types, failures, cancellation}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.18
Multiparty Session Programming with Global Protocol Combinators (Artifact)

Authors: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
In the paper "Multiparty Session Programming with Global Protocol Combinators", we introduce a library, ocaml-mpst for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. This artifact is the source code of ocaml-mpst, with all the examples and benchmarks discussed in the paper.
Cite as

Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming with Global Protocol Combinators (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 18:1-18:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{imai_et_al:DARTS.6.2.18,
  author =	{Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
  title =	{{Multiparty Session Programming with Global Protocol Combinators (Artifact)}},
  pages =	{18:1--18:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.6.2.18},
  URN =		{urn:nbn:de:0030-drops-132159},
  doi =		{10.4230/DARTS.6.2.18},
  annote =	{Keywords: Multiparty Session Types, Communication Protocol, Concurrent and Distributed Programming, OCaml}
}
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-dev.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
DOI: 10.4230/LIPIcs.TIME.2019.15
A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic

Authors: Quentin Peyras, Julien Brunel, and David Chemouil

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
First-Order Linear Temporal Logic (FOLTL) is well-suited to specify infinite-state systems. However, FOLTL satisfiability is not even semi-decidable, thus preventing automated verification. To address this, a possible track is to constrain specifications to a decidable fragment of FOLTL, but known fragments are too restricted to be usable in practice. In this paper, we exhibit various fragments of increasing scope that provide a pertinent basis for abstract specification of infinite-state systems. We show that these fragments enjoy the Bounded Domain Property (any satisfiable FOLTL formula has a model with a finite, bounded FO domain), which provides a basis for complete, automated verification by reduction to LTL satisfiability. Finally, we present a simple case study illustrating the applicability and limitations of our results.
Cite as

Quentin Peyras, Julien Brunel, and David Chemouil. A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{peyras_et_al:LIPIcs.TIME.2019.15,
  author =	{Peyras, Quentin and Brunel, Julien and Chemouil, David},
  title =	{{A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.15},
  URN =		{urn:nbn:de:0030-drops-113731},
  doi =		{10.4230/LIPIcs.TIME.2019.15},
  annote =	{Keywords: First-Order Linear Temporal Logic, Bounded Domain Property, Finite Domain Property, Decidability}
}
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-dev.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-dev.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}
}
  • Refine by Author
  • 4 Brunel, Julien
  • 3 Pagetti, Claire
  • 3 Sensfelder, Nathanaël
  • 2 Neykova, Rumyana
  • 2 Yoshida, Nobuko
  • Show More...

  • Refine by Classification
  • 3 Computer systems organization → Multicore architectures
  • 3 Computer systems organization → Real-time systems
  • 1 Software and its engineering → Concurrent programming languages
  • 1 Software and its engineering → Concurrent programming structures
  • 1 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 3 Real-time systems
  • 3 cache coherence
  • 3 multi-core processor
  • 2 formal methods
  • 1 Bounded Domain Property
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 3 2019
  • 2 2020
  • 1 2022

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