23 Search Results for "Hugues, J�r�me"

Document
DOI: 10.4230/LIPIcs.IPEC.2023.25
Twin-Width of Graphs with Tree-Structured Decompositions

Authors: Irene Heinrich and Simon Raßmann

Published in: LIPIcs, Volume 285, 18th International Symposium on Parameterized and Exact Computation (IPEC 2023)

Abstract
The twin-width of a graph measures its distance to co-graphs and generalizes classical width concepts such as tree-width or rank-width. Since its introduction in 2020 [Édouard Bonnet et al., 2022; Édouard Bonnet et al., 2020], a mass of new results has appeared relating twin width to group theory, model theory, combinatorial optimization, and structural graph theory. We take a detailed look at the interplay between the twin-width of a graph and the twin-width of its components under tree-structured decompositions: We prove that the twin-width of a graph is at most twice its strong tree-width, contrasting nicely with the result of [Édouard Bonnet and Hugues Déprés, 2023; Édouard Bonnet and Hugues Déprés, 2022], which states that twin-width can be exponential in tree-width. Further, we employ the fundamental concept from structural graph theory of decomposing a graph into highly connected components, in order to obtain optimal linear bounds on the twin-width of a graph given the widths of its biconnected components. For triconnected components we obtain a linear upper bound if we add red edges to the components indicating the splits which led to the components. Extending this approach to quasi-4-connectivity, we obtain a quadratic upper bound. Finally, we investigate how the adhesion of a tree decomposition influences the twin-width of the decomposed graph.
Cite as

Irene Heinrich and Simon Raßmann. Twin-Width of Graphs with Tree-Structured Decompositions. In 18th International Symposium on Parameterized and Exact Computation (IPEC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 285, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{heinrich_et_al:LIPIcs.IPEC.2023.25,
  author =	{Heinrich, Irene and Ra{\ss}mann, Simon},
  title =	{{Twin-Width of Graphs with Tree-Structured Decompositions}},
  booktitle =	{18th International Symposium on Parameterized and Exact Computation (IPEC 2023)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-305-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{285},
  editor =	{Misra, Neeldhara and Wahlstr\"{o}m, Magnus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2023.25},
  URN =		{urn:nbn:de:0030-drops-194449},
  doi =		{10.4230/LIPIcs.IPEC.2023.25},
  annote =	{Keywords: twin-width, quasi-4 connected components, strong tree-width}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.12
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users

Authors: Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
The Coq Community Survey 2022 was an online public survey of users of the Coq proof assistant conducted during February 2022. Broadly, the survey asked about use of Coq features, user interfaces, libraries, plugins, and tools, views on renaming Coq and Coq improvements, and also demographic data such as education and experience with Coq and other proof assistants and programming languages. The survey received 466 submitted responses, making it the largest survey of users of an interactive theorem prover (ITP) so far. We present the design of the survey, a summary of key results, and analysis of answers relevant to ITP technology development and usage. In particular, we analyze user characteristics associated with adoption of tools and libraries and make comparisons to adjacent software communities. Notably, we find that experience has significant impact on Coq user behavior, including on usage of tools, libraries, and integrated development environments.
Cite as

Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann. Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dealmeidaborges_et_al:LIPIcs.ITP.2023.12,
  author =	{de Almeida Borges, Ana and Casanueva Art{\'\i}s, Annal{\'\i} and Falleri, Jean-R\'{e}my and Gallego Arias, Emilio Jes\'{u}s and Martin-Dorel, \'{E}rik and Palmskog, Karl and Serebrenik, Alexander and Zimmermann, Th\'{e}o},
  title =	{{Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.12},
  URN =		{urn:nbn:de:0030-drops-183875},
  doi =		{10.4230/LIPIcs.ITP.2023.12},
  annote =	{Keywords: Coq, Community, Survey, Statistical Analysis}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.10
Approximating Highly Inapproximable Problems on Graphs of Bounded Twin-Width

Authors: Pierre Bergé, Édouard Bonnet, Hugues Déprés, and Rémi Watrigant

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
For any ε > 0, we give a polynomial-time n^ε-approximation algorithm for Max Independent Set in graphs of bounded twin-width given with an O(1)-sequence. This result is derived from the following time-approximation trade-off: We establish an O(1)^{2^q-1}-approximation algorithm running in time exp(O_q(n^{2^{-q}})), for every integer q ⩾ 0. Guided by the same framework, we obtain similar approximation algorithms for Min Coloring and Max Induced Matching. In general graphs, all these problems are known to be highly inapproximable: for any ε > 0, a polynomial-time n^{1-ε}-approximation for any of them would imply that P=NP [Håstad, FOCS '96; Zuckerman, ToC '07; Chalermsook et al., SODA '13]. We generalize the algorithms for Max Independent Set and Max Induced Matching to the independent (induced) packing of any fixed connected graph H. In contrast, we show that such approximation guarantees on graphs of bounded twin-width given with an O(1)-sequence are very unlikely for Min Independent Dominating Set, and somewhat unlikely for Longest Path and Longest Induced Path. Regarding the existence of better approximation algorithms, there is a (very) light evidence that the obtained approximation factor of n^ε for Max Independent Set may be best possible. This is the first in-depth study of the approximability of problems in graphs of bounded twin-width. Prior to this paper, essentially the only such result was a polynomial-time O(1)-approximation algorithm for Min Dominating Set [Bonnet et al., ICALP '21].
Cite as

Pierre Bergé, Édouard Bonnet, Hugues Déprés, and Rémi Watrigant. Approximating Highly Inapproximable Problems on Graphs of Bounded Twin-Width. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 10:1-10:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{berge_et_al:LIPIcs.STACS.2023.10,
  author =	{Berg\'{e}, Pierre and Bonnet, \'{E}douard and D\'{e}pr\'{e}s, Hugues and Watrigant, R\'{e}mi},
  title =	{{Approximating Highly Inapproximable Problems on Graphs of Bounded Twin-Width}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{10:1--10:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.10},
  URN =		{urn:nbn:de:0030-drops-176629},
  doi =		{10.4230/LIPIcs.STACS.2023.10},
  annote =	{Keywords: Approximation algorithms, bounded twin-width}
}
Document
DOI: 10.4230/LIPIcs.CCC.2022.30
Interactive Oracle Proofs of Proximity to Algebraic Geometry Codes

Authors: Sarah Bordage, Mathieu Lhotel, Jade Nardi, and Hugues Randriam

Published in: LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022)

Abstract
In this work, we initiate the study of proximity testing to Algebraic Geometry (AG) codes. An AG code C = C(𝒳, 𝒫, D) over an algebraic curve 𝒳 is a vector space associated to evaluations on 𝒫 ⊆ 𝒳 of functions in the Riemann-Roch space L_𝒳(D). The problem of testing proximity to an error-correcting code C consists in distinguishing between the case where an input word, given as an oracle, belongs to C and the one where it is far from every codeword of C. AG codes are good candidates to construct probabilistic proof systems, but there exists no efficient proximity tests for them. We aim to fill this gap. We construct an Interactive Oracle Proof of Proximity (IOPP) for some families of AG codes by generalizing an IOPP for Reed-Solomon codes, known as the FRI protocol [Eli Ben-Sasson et al., 2018]. We identify suitable requirements for designing efficient IOPP systems for AG codes. Our approach relies on a neat decomposition of the Riemann-Roch space of any invariant divisor under a group action on a curve into several explicit Riemann-Roch spaces on the quotient curve. We provide sufficient conditions on an AG code C that allow to reduce a proximity testing problem for C to a membership problem for a significantly smaller code C'. As concrete instantiations, we study AG codes on Kummer curves and curves in the Hermitian tower. The latter can be defined over polylogarithmic-size alphabet. We specialize the generic AG-IOPP construction to reach linear prover running time and logarithmic verification on Kummer curves, and quasilinear prover time with polylogarithmic verification on the Hermitian tower.
Cite as

Sarah Bordage, Mathieu Lhotel, Jade Nardi, and Hugues Randriam. Interactive Oracle Proofs of Proximity to Algebraic Geometry Codes. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 30:1-30:45, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bordage_et_al:LIPIcs.CCC.2022.30,
  author =	{Bordage, Sarah and Lhotel, Mathieu and Nardi, Jade and Randriam, Hugues},
  title =	{{Interactive Oracle Proofs of Proximity to Algebraic Geometry Codes}},
  booktitle =	{37th Computational Complexity Conference (CCC 2022)},
  pages =	{30:1--30:45},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-241-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{234},
  editor =	{Lovett, Shachar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.30},
  URN =		{urn:nbn:de:0030-drops-165923},
  doi =		{10.4230/LIPIcs.CCC.2022.30},
  annote =	{Keywords: Algebraic geometry codes, Interactive oracle proofs of proximity, Proximity testing}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2022.18
Deciding Twin-Width at Most 4 Is NP-Complete

Authors: Pierre Bergé, Édouard Bonnet, and Hugues Déprés

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We show that determining if an n-vertex graph has twin-width at most 4 is NP-complete, and requires time 2^Ω(n/log n) unless the Exponential-Time Hypothesis fails. Along the way, we give an elementary proof that n-vertex graphs subdivided at least 2 log n times have twin-width at most 4. We also show how to encode trigraphs H (2-edge colored graphs involved in the definition of twin-width) into graphs G, in the sense that every d-sequence (sequence of vertex contractions witnessing that the twin-width is at most d) of G inevitably creates H as an induced subtrigraph, whereas there exists a partial d-sequence that actually goes from G to H. We believe that these facts and their proofs can be of independent interest.
Cite as

Pierre Bergé, Édouard Bonnet, and Hugues Déprés. Deciding Twin-Width at Most 4 Is NP-Complete. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{berge_et_al:LIPIcs.ICALP.2022.18,
  author =	{Berg\'{e}, Pierre and Bonnet, \'{E}douard and D\'{e}pr\'{e}s, Hugues},
  title =	{{Deciding Twin-Width at Most 4 Is NP-Complete}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.18},
  URN =		{urn:nbn:de:0030-drops-163595},
  doi =		{10.4230/LIPIcs.ICALP.2022.18},
  annote =	{Keywords: Twin-width, lower bounds}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.3
Putting Randomized Compiler Testing into Production (Artifact)

Authors: Alastair F. Donaldson, Hugues Evrard, and Paul Thomson

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

Abstract
This artifact accompanies our experience report for our compiler testing technology transfer project: taking the GraphicsFuzz research project on randomized metamorphic testing of graphics shader compilers, and building the necessary tooling around it to provide a highly automated process for improving the Khronos Vulkan Conformance Test Suite (CTS) with test cases that expose fuzzer-found compiler bugs, or that plug gaps in test coverage. The artifact consists of two Dockerfiles and associated files that can be used to build two Docker containers. The containers include our main tool for performing fuzzing: gfauto. The containers allow the user to fuzz SwiftShader, a software Vulkan implementation, finding 4 bugs. The user will also perform some line coverage analysis of SwiftShader using our tools to synthesize a small test that increases line coverage. Ubuntu, gfauto, SwiftShader, and other dependencies inside the Docker containers are fixed at specific versions, and all random seeds are set to specific values. Thus, all examples should reproduce faithfully on any machine.
Cite as

Alastair F. Donaldson, Hugues Evrard, and Paul Thomson. Putting Randomized Compiler Testing into Production (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{donaldson_et_al:DARTS.6.2.3,
  author =	{Donaldson, Alastair F. and Evrard, Hugues and Thomson, Paul},
  title =	{{Putting Randomized Compiler Testing into Production (Artifact)}},
  pages =	{3:1--3:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Donaldson, Alastair F. and Evrard, Hugues and Thomson, Paul},
  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.3},
  URN =		{urn:nbn:de:0030-drops-132005},
  doi =		{10.4230/DARTS.6.2.3},
  annote =	{Keywords: Compilers, metamorphic testing, 3D graphics, experience report}
}
Document
Experience Report
DOI: 10.4230/LIPIcs.ECOOP.2020.22
Putting Randomized Compiler Testing into Production (Experience Report)

Authors: Alastair F. Donaldson, Hugues Evrard, and Paul Thomson

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
We describe our experience over the last 18 months on a compiler testing technology transfer project: taking the GraphicsFuzz research project on randomized metamorphic testing of graphics shader compilers, and building the necessary tooling around it to provide a highly automated process for improving the Khronos Vulkan Conformance Test Suite (CTS) with test cases that expose fuzzer-found compiler bugs, or that plug gaps in test coverage. We present this tooling for test automation - gfauto - in detail, as well as our use of differential coverage and test case reduction as a method for automatically synthesizing tests that fill coverage gaps. We explain the value that GraphicsFuzz has provided in automatically testing the ecosystem of tools for transforming, optimizing and validating Vulkan shaders, and the challenges faced when testing a tool ecosystem rather than a single tool. We discuss practical issues associated with putting automated metamorphic testing into production, related to test case validity, bug de-duplication and floating-point precision, and provide illustrative examples of bugs found during our work.
Cite as

Alastair F. Donaldson, Hugues Evrard, and Paul Thomson. Putting Randomized Compiler Testing into Production (Experience Report). In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 22:1-22:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{donaldson_et_al:LIPIcs.ECOOP.2020.22,
  author =	{Donaldson, Alastair F. and Evrard, Hugues and Thomson, Paul},
  title =	{{Putting Randomized Compiler Testing into Production}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{22:1--22:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.22},
  URN =		{urn:nbn:de:0030-drops-131791},
  doi =		{10.4230/LIPIcs.ECOOP.2020.22},
  annote =	{Keywords: Compilers, metamorphic testing, 3D graphics, experience report}
}
Document
DOI: 10.4230/OASIcs.WCET.2019.6
Validating Static WCET Analysis: A Method and Its Application

Authors: Wei-Tsun Sun, Eric Jenn, and Hugues Cassé

Published in: OASIcs, Volume 72, 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019)

Abstract
WCET analysis is a key activity in the development of safety critical real-time systems. Whether upper bounds on WCETs are obtained using static analysis or measurements, the confidence on the compliance of a system with its temporal requirements directly depends on the confidence on these estimations. Static WCET analysis based on abstract interpretation takes benefits from its formal foundations. However, it also strongly depends on the correctness of the underlying models. We hereby show how we have validated the version of the data flow static analyser of OTAWA applied to the AURIX TC275 target processor.
Cite as

Wei-Tsun Sun, Eric Jenn, and Hugues Cassé. Validating Static WCET Analysis: A Method and Its Application. In 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019). Open Access Series in Informatics (OASIcs), Volume 72, pp. 6:1-6:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sun_et_al:OASIcs.WCET.2019.6,
  author =	{Sun, Wei-Tsun and Jenn, Eric and Cass\'{e}, Hugues},
  title =	{{Validating Static WCET Analysis: A Method and Its Application}},
  booktitle =	{19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019)},
  pages =	{6:1--6:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-118-4},
  ISSN =	{2190-6807},
  year =	{2019},
  volume =	{72},
  editor =	{Altmeyer, Sebastian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2019.6},
  URN =		{urn:nbn:de:0030-drops-107713},
  doi =		{10.4230/OASIcs.WCET.2019.6},
  annote =	{Keywords: validation of WCET tools, ISS, nML}
}
Document
DOI: 10.4230/OASIcs.WCET.2018.3
Reducing Timing Interferences in Real-Time Applications Running on Multicore Architectures

Authors: Thomas Carle and Hugues Cassé

Published in: OASIcs, Volume 63, 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)

Abstract
We introduce a unified wcet analysis and scheduling framework for real-time applications deployed on multicore architectures. Our method does not follow a particular programming model, meaning that any piece of existing code (in particular legacy) can be re-used, and aims at reducing automatically the worst-case number of timing interferences between tasks. Our method is based on the notion of Time Interest Points (tips), which are instructions that can generate and/or suffer from timing interferences. We show how such points can be extracted from the binary code of applications and selected prior to performing the wcet analysis. We then represent real-time tasks as sequences of time intervals separated by tips, and schedule those tasks so that the overall makespan (including the potential timing penalties incurred by interferences) is minimized. This scheduling phase is performed using an Integer Linear Programming (ilp) solver. Preliminary results on state-of-the-art benchmarks show promising results and pave the way for future extensions of the model and optimizations.
Cite as

Thomas Carle and Hugues Cassé. Reducing Timing Interferences in Real-Time Applications Running on Multicore Architectures. In 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018). Open Access Series in Informatics (OASIcs), Volume 63, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{carle_et_al:OASIcs.WCET.2018.3,
  author =	{Carle, Thomas and Cass\'{e}, Hugues},
  title =	{{Reducing Timing Interferences in Real-Time Applications Running on Multicore Architectures}},
  booktitle =	{18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)},
  pages =	{3:1--3:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-073-6},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{63},
  editor =	{Brandner, Florian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2018.3},
  URN =		{urn:nbn:de:0030-drops-97493},
  doi =		{10.4230/OASIcs.WCET.2018.3},
  annote =	{Keywords: Multicore architecture, WCET, Time Interest Points}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.23
GPU Schedulers: How Fair Is Fair Enough?

Authors: Tyler Sorensen, Hugues Evrard, and Alastair F. Donaldson

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Blocking synchronisation idioms, e.g. mutexes and barriers, play an important role in concurrent programming. However, systems with semi-fair schedulers, e.g. graphics processing units (GPUs), are becoming increasingly common. Such schedulers provide varying degrees of fairness, guaranteeing enough to allow some, but not all, blocking idioms. While a number of applications that use blocking idioms do run on today's GPUs, reasoning about liveness properties of such applications is difficult as documentation is scarce and scattered. In this work, we aim to clarify fairness properties of semi-fair schedulers. To do this, we define a general temporal logic formula, based on weak fairness, parameterised by a predicate that enables fairness per-thread at certain points of an execution. We then define fairness properties for three GPU schedulers: HSA, OpenCL, and occupancy-bound execution. We examine existing GPU applications and show that none of the above schedulers are strong enough to provide the fairness properties required by these applications. It hence appears that existing GPU scheduler descriptions do not entirely capture the fairness properties that are provided on current GPUs. Thus, we present two new schedulers that aim to support existing GPU applications. We analyse the behaviour of common blocking idioms under each scheduler and show that one of our new schedulers allows a more natural implementation of a GPU protocol.
Cite as

Tyler Sorensen, Hugues Evrard, and Alastair F. Donaldson. GPU Schedulers: How Fair Is Fair Enough?. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{sorensen_et_al:LIPIcs.CONCUR.2018.23,
  author =	{Sorensen, Tyler and Evrard, Hugues and Donaldson, Alastair F.},
  title =	{{GPU Schedulers: How Fair Is Fair Enough?}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.23},
  URN =		{urn:nbn:de:0030-drops-95619},
  doi =		{10.4230/LIPIcs.CONCUR.2018.23},
  annote =	{Keywords: GPU scheduling, Blocking synchronisation, GPU semantics}
}
Document
DOI: 10.4230/OASIcs.WCET.2017.9
The W-SEPT Project: Towards Semantic-Aware WCET Estimation

Authors: Claire Maiza, Pascal Raymond, Catherine Parent-Vigouroux, Armelle Bonenfant, Fabienne Carrier, Hugues Cassé, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Erwan Jahier, Hanbing Li, Marianne de Michiel, Vincent Mussot, Isabelle Puaut, Christine Rochange, Erven Rohou, Jordy Ruiz, Pascal Sotin, and Wei-Tsun Sun

Published in: OASIcs, Volume 57, 17th International Workshop on Worst-Case Execution Time Analysis (WCET 2017)

Abstract
Critical embedded systems are generally composed of repetitive tasks that must meet hard timing constraints, such as termination deadlines. Providing an upper bound of the worst-case execution time (WCET) of such tasks at design time is necessary to guarantee the correctness of the system. In static WCET analysis, a main source of over-approximation comes from the complexity of the modern hardware platforms: their timing behavior tends to become more unpredictable because of features like caches, pipeline, branch prediction, etc. Another source of over-approximation comes from the software itself: WCET analysis may consider potential worst-cases executions that are actually infeasible, because of the semantics of the program or because they correspond to unrealistic inputs. The W-SEPT project, for "WCET, Semantics, Precision and Traceability", has been carried out to study and exploit the influence of program semantics on the WCET estimation. This paper presents the results of this project : a semantic-aware WCET estimation workflow for high-level designed systems.
Cite as

Claire Maiza, Pascal Raymond, Catherine Parent-Vigouroux, Armelle Bonenfant, Fabienne Carrier, Hugues Cassé, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Erwan Jahier, Hanbing Li, Marianne de Michiel, Vincent Mussot, Isabelle Puaut, Christine Rochange, Erven Rohou, Jordy Ruiz, Pascal Sotin, and Wei-Tsun Sun. The W-SEPT Project: Towards Semantic-Aware WCET Estimation. In 17th International Workshop on Worst-Case Execution Time Analysis (WCET 2017). Open Access Series in Informatics (OASIcs), Volume 57, pp. 9:1-9:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{maiza_et_al:OASIcs.WCET.2017.9,
  author =	{Maiza, Claire and Raymond, Pascal and Parent-Vigouroux, Catherine and Bonenfant, Armelle and Carrier, Fabienne and Cass\'{e}, Hugues and Cuenot, Philippe and Claraz, Denis and Halbwachs, Nicolas and Jahier, Erwan and Li, Hanbing and de Michiel, Marianne and Mussot, Vincent and Puaut, Isabelle and Rochange, Christine and Rohou, Erven and Ruiz, Jordy and Sotin, Pascal and Sun, Wei-Tsun},
  title =	{{The W-SEPT Project: Towards Semantic-Aware WCET Estimation}},
  booktitle =	{17th International Workshop on Worst-Case Execution Time Analysis (WCET 2017)},
  pages =	{9:1--9:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-057-6},
  ISSN =	{2190-6807},
  year =	{2017},
  volume =	{57},
  editor =	{Reineke, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2017.9},
  URN =		{urn:nbn:de:0030-drops-73097},
  doi =		{10.4230/OASIcs.WCET.2017.9},
  annote =	{Keywords: Worst-case execution time analysis, Static analysis, Program analysis}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2016.7
Set-Consensus Collections are Decidable

Authors: Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, and Petr Kuznetsov

Published in: LIPIcs, Volume 70, 20th International Conference on Principles of Distributed Systems (OPODIS 2016)

Abstract
A natural way to measure the power of a distributed-computing model is to characterize the set of tasks that can be solved in it. In general, however, the question of whether a given task can be solved in a given model is undecidable, even if we only consider the wait-free shared-memory model. In this paper, we address this question for restricted classes of models and tasks. We show that the question of whether a collection C of (l, j)-set consensus objects, for various l (the number of processes that can invoke the object) and j (the number of distinct outputs the object returns), can be used by n processes to solve wait-free k-set consensus is decidable. Moreover, we provide a simple O(n^2) decision algorithm, based on a dynamic programming solution to the Knapsack optimization problem. We then present an adaptive wait-free set-consensus algorithm that, for each set of participating processes, achieves the best level of agreement that is possible to achieve using C. Overall, this gives us a complete characterization of a read-write model defined by a collection of set-consensus objects through its set-consensus power.
Cite as

Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, and Petr Kuznetsov. Set-Consensus Collections are Decidable. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{delportegallet_et_al:LIPIcs.OPODIS.2016.7,
  author =	{Delporte-Gallet, Carole and Fauconnier, Hugues and Gafni, Eli and Kuznetsov, Petr},
  title =	{{Set-Consensus Collections are Decidable}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.7},
  URN =		{urn:nbn:de:0030-drops-70761},
  doi =		{10.4230/LIPIcs.OPODIS.2016.7},
  annote =	{Keywords: Decidability, distributed tasks, set consensus, Knapsack problem}
}
Document
DOI: 10.4230/OASIcs.WCET.2016.3
Expressing and Exploiting Conflicts over Paths in WCET Analysis

Authors: Vincent Mussot, Jordy Ruiz, Pascal Sotin, Marianne de Michiel, and Hugues Cassé

Published in: OASIcs, Volume 55, 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016)

Abstract
The presence of infeasible paths in a program is a source of imprecision in the Worst-Case Execution Time (WCET) analysis. Detecting, expressing and exploiting such paths can improve the WCET estimation or, at least, improve the confidence we have in estimation precision. In this article, we propose an extension of the FFX format to express conflicts over paths and we detail two ways of enhancing the WCET analyses with that information. We demonstrate and compare these techniques on the Mälardalen benchmark suite and on C code generated from Esterel.
Cite as

Vincent Mussot, Jordy Ruiz, Pascal Sotin, Marianne de Michiel, and Hugues Cassé. Expressing and Exploiting Conflicts over Paths in WCET Analysis. In 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016). Open Access Series in Informatics (OASIcs), Volume 55, pp. 3:1-3:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{mussot_et_al:OASIcs.WCET.2016.3,
  author =	{Mussot, Vincent and Ruiz, Jordy and Sotin, Pascal and de Michiel, Marianne and Cass\'{e}, Hugues},
  title =	{{Expressing and Exploiting Conflicts over Paths in WCET Analysis}},
  booktitle =	{16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016)},
  pages =	{3:1--3:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-025-5},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{55},
  editor =	{Schoeberl, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2016.3},
  URN =		{urn:nbn:de:0030-drops-68966},
  doi =		{10.4230/OASIcs.WCET.2016.3},
  annote =	{Keywords: WCET analysis, Infeasible paths, Path conflicts, IPET, CFG transformation}
}
Document
DOI: 10.4230/OASIcs.WCET.2016.8
Dynamic Branch Resolution Based on Combined Static Analyses

Authors: Wei-Tsun Sun and Hugues Cassé

Published in: OASIcs, Volume 55, 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016)

Abstract
Static analysis requires the full knowledge of the overall program structure. The structure of a program can be represented by a Control Flow Graph (CFG) where vertices are basic blocks (BB) and edges represent the control flow between the BB. To construct a full CFG, all the BB as well as all of their possible targets addresses must be found. In this paper, we present a method to resolve dynamic branches, that identifies the target addresses of BB created due to the switch-cases and calls on function pointers. We also implemented a slicing method to speed up the overall analysis which makes our approach applicable on large and realistic real-time programs.
Cite as

Wei-Tsun Sun and Hugues Cassé. Dynamic Branch Resolution Based on Combined Static Analyses. In 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016). Open Access Series in Informatics (OASIcs), Volume 55, pp. 8:1-8:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{sun_et_al:OASIcs.WCET.2016.8,
  author =	{Sun, Wei-Tsun and Cass\'{e}, Hugues},
  title =	{{Dynamic Branch Resolution Based on Combined Static Analyses}},
  booktitle =	{16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016)},
  pages =	{8:1--8:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-025-5},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{55},
  editor =	{Schoeberl, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2016.8},
  URN =		{urn:nbn:de:0030-drops-69014},
  doi =		{10.4230/OASIcs.WCET.2016.8},
  annote =	{Keywords: WCET, static analysis, dynamic branch, assembly, machine language}
}
Document
DOI: 10.4230/OASIcs.WCET.2015.1
A Framework to Quantify the Overestimations of Static WCET Analysis

Authors: Hugues Cassé, Haluk Ozaktas, and Christine Rochange

Published in: OASIcs, Volume 47, 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)

Abstract
To reduce complexity while computing an upper bound on the worst-case execution time, static WCET analysis performs over-approximations. This feeds the general feeling that static WCET estimations can be far above the real WCET. This feeling is strengthened when these estimations are compared to measured execution times: generally, it is very unlikely to capture the worstcase from observations, then the difference between the highest watermark and the proven WCET upper bound might be considerable. In this paper, we introduce a framework to quantify the possible overestimation on WCET upper bounds obtained by static analysis. The objective is to derive a lower bound on the WCET to complement the upper bound.
Cite as

Hugues Cassé, Haluk Ozaktas, and Christine Rochange. A Framework to Quantify the Overestimations of Static WCET Analysis. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{casse_et_al:OASIcs.WCET.2015.1,
  author =	{Cass\'{e}, Hugues and Ozaktas, Haluk and Rochange, Christine},
  title =	{{A Framework to Quantify the Overestimations of Static WCET Analysis}},
  booktitle =	{15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
  pages =	{1--10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-95-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{47},
  editor =	{Cazorla, Francisco J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.1},
  URN =		{urn:nbn:de:0030-drops-52517},
  doi =		{10.4230/OASIcs.WCET.2015.1},
  annote =	{Keywords: Static WCET analysis, uncertainty, overestimation, cache analysis}
}
  • Refine by Author
  • 12 Cassé, Hugues
  • 3 Ballabriga, Clément
  • 3 Donaldson, Alastair F.
  • 3 Evrard, Hugues
  • 3 Rochange, Christine
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → Compilers
  • 2 Software and its engineering → Software testing and debugging
  • 2 Theory of computation → Fixed parameter tractability
  • 2 Theory of computation → Graph algorithms analysis
  • 1 Computer systems organization → Real-time systems
  • Show More...

  • Refine by Keyword
  • 4 WCET
  • 3 WCET analysis
  • 2 3D graphics
  • 2 AADL
  • 2 Compilers
  • Show More...

  • Refine by Type
  • 23 document

  • Refine by Publication Year
  • 3 2008
  • 3 2023
  • 2 2015
  • 2 2016
  • 2 2017
  • Show More...

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