4 Search Results for "Dominguez, C�sar"

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.30
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack

Authors: Jesús Domínguez and Aleksandar Nanevski

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points (LP). However, LPs often hinder abstraction, and for some algorithms such as the timestamped stack, it is unclear how to even identify their LPs. In this paper, we show how to develop declarative proofs of linearizability by foregoing LPs and instead employing axiomatization of so-called visibility relations. While visibility relations have been considered before for the timestamped stack, our study is the first to show how to derive the axiomatization systematically and intuitively from the sequential specification of the stack. In addition to the visibility relation, a novel separability relation emerges to generalize real-time precedence of procedure invocation. The visibility and separability relations have natural definitions for the timestamped stack, and enable a novel proof that reduces the algorithm to a simplified form where the timestamps are generated atomically.
Cite as

Jesús Domínguez and Aleksandar Nanevski. Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dominguez_et_al:LIPIcs.CONCUR.2023.30,
  author =	{Dom{\'\i}nguez, Jes\'{u}s and Nanevski, Aleksandar},
  title =	{{Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.30},
  URN =		{urn:nbn:de:0030-drops-190245},
  doi =		{10.4230/LIPIcs.CONCUR.2023.30},
  annote =	{Keywords: Linearizability, Visibility Relations, Timestamped Stack}
}
Document
DOI: 10.4230/LIPIcs.SEA.2023.7
Simple Runs-Bounded FM-Index Designs Are Fast

Authors: Diego Díaz-Domínguez, Saska Dönges, Simon J. Puglisi, and Leena Salmela

Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)

Abstract
Given a string X of length n on alphabet σ, the FM-index data structure allows counting all occurrences of a pattern P of length m in O(m) time via an algorithm called backward search. An important difficulty when searching with an FM-index is to support queries on L, the Burrows-Wheeler transform of X, while L is in compressed form. This problem has been the subject of intense research for 25 years now. Run-length encoding of L is an effective way to reduce index size, in particular when the data being indexed is highly-repetitive, which is the case in many types of modern data, including those arising from versioned document collections and in pangenomics. This paper takes a back-to-basics look at supporting backward search in FM-indexes, exploring and engineering two simple designs. The first divides the BWT string into blocks containing b symbols each and then run-length compresses each block separately, possibly introducing new runs (compared to applying run-length encoding once, to the whole string). Each block stores counts of each symbol that occurs before the block. This method supports the operation rank_c(L, i) (i.e., count the number of times c occurs in the prefix L[1..i]) by first determining the block i/b in which i falls and scanning the block to the appropriate position counting occurrences of c along the way. This partial answer to rank_c(L, i) is then added to the stored count of c symbols before the block to determine the final answer. Our second design has a similar structure, but instead divides the run-length-encoded version of L into blocks containing an equal number of runs. The trick then is to determine the block in which a query falls, which is achieved via a predecessor query over the block starting positions. We show via extensive experiments on a wide range of repetitive text collections that these FM-indexes are not only easy to implement, but also fast and space efficient in practice.
Cite as

Diego Díaz-Domínguez, Saska Dönges, Simon J. Puglisi, and Leena Salmela. Simple Runs-Bounded FM-Index Designs Are Fast. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{diazdominguez_et_al:LIPIcs.SEA.2023.7,
  author =	{D{\'\i}az-Dom{\'\i}nguez, Diego and D\"{o}nges, Saska and Puglisi, Simon J. and Salmela, Leena},
  title =	{{Simple Runs-Bounded FM-Index Designs Are Fast}},
  booktitle =	{21st International Symposium on Experimental Algorithms (SEA 2023)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-279-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{265},
  editor =	{Georgiadis, Loukas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.7},
  URN =		{urn:nbn:de:0030-drops-183579},
  doi =		{10.4230/LIPIcs.SEA.2023.7},
  annote =	{Keywords: data structures, efficient algorithms}
}
Document
DOI: 10.4230/DagSemProc.05021.11
Diagrammatic logic and exceptions:an introduction

Authors: Dominique Duval and Jean-Claude Reynaud

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)

Abstract
For dealing with computational effects in computer science, it may be helpful to use several logics: typically, a logic with implicit effects for the language, and a more classical logic for the user. Hence, the study of computational effects should take place in a framework where distinct logics can be related. In this paper, such a framework is presented: it is a category, called the category of propagators. Each propagator defines a kind of logic, called a diagrammatic logic, which is endowed with a deduction system and a sound notion of models. Morphisms of propagators provide the required relationships between diagrammatic logics. The category of propagators has been introduced by Duval and Lair in 2002, it is based on the notion of sketches, which is due to Ehresmann in the 1960's. Then, the paper outlines how Duval and Reynaud in 2004 used the category of propagators for dealing with the computational effect of raising and handling exceptions. Another application of diagrammatic logic is presented by Dominguez et al. in the same conference
Cite as

Dominique Duval and Jean-Claude Reynaud. Diagrammatic logic and exceptions:an introduction. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{duval_et_al:DagSemProc.05021.11,
  author =	{Duval, Dominique and Reynaud, Jean-Claude},
  title =	{{Diagrammatic logic and exceptions:an introduction}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.11},
  URN =		{urn:nbn:de:0030-drops-2931},
  doi =		{10.4230/DagSemProc.05021.11},
  annote =	{Keywords: Specifications, Semantics, Exceptions, Sketches, Diagrammatic Logic, Extensive Categories, Monads.}
}
Document
DOI: 10.4230/DagSemProc.05021.22
Towards Diagrammatic Specifications of Symbolic Computation Systems

Authors: César Dominguez, Dominique Duval, Laureano Lamban, and Julio Rubio Garcia

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)

Abstract
The aim of this work is to present an ongoing project to formalize, in the framework of diagrammatic logic (due to Dominique Duval and Christian Lair) some data structures appearing in Sergeraert's symbolic computation systems Kenzo and EAT. More precisely, we intend to translate into the diagrammatic setting a previous work based on standard algebraic specification techniques. In particular, we give hints on the reason why an important construction (called imp construction) in the specification of the systems can be understood as a freely generating functor between suitable categories of diagrammatic realizations. Even if very partial, these positive results seem to indicate that this new kind of specification is promising in the field of symbolic computation.
Cite as

César Dominguez, Dominique Duval, Laureano Lamban, and Julio Rubio Garcia. Towards Diagrammatic Specifications of Symbolic Computation Systems. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{dominguez_et_al:DagSemProc.05021.22,
  author =	{Dominguez, C\'{e}sar and Duval, Dominique and Lamban, Laureano and Rubio Garcia, Julio},
  title =	{{Towards Diagrammatic Specifications of Symbolic Computation Systems}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--23},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.22},
  URN =		{urn:nbn:de:0030-drops-2927},
  doi =		{10.4230/DagSemProc.05021.22},
  annote =	{Keywords: Specification, symbolic computation, sketches, diagrammatic logic}
}
  • Refine by Author
  • 2 Duval, Dominique
  • 1 Dominguez, César
  • 1 Domínguez, Jesús
  • 1 Díaz-Domínguez, Diego
  • 1 Dönges, Saska
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Design and analysis of algorithms
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 Diagrammatic Logic
  • 1 Exceptions
  • 1 Extensive Categories
  • 1 Linearizability
  • 1 Monads.
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2006
  • 2 2023

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