3 Search Results for "van Glabbeek, Rob J."

Document
DOI: 10.4230/LIPIcs.CONCUR.2019.34
A Sound Foundation for the Topological Approach to Task Solvability

Authors: Jérémy Ledent and Samuel Mimram

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
The area of fault-tolerant distributed computability is concerned with the solvability of decision tasks in various computational models where the processes might crash. A very successful approach to prove impossibility results in this context is that of combinatorial topology, started by Herlihy and Shavit’s paper in 1999. They proved that, for wait-free protocols where the processes communicate through read/write registers, a task is solvable if and only if there exists some map between simplicial complexes satisfying some properties. This approach was then extended to many different contexts, where the processes have access to various synchronization and communication primitives. Usually, in those cases, the existence of a simplicial map from the protocol complex to the output complex is taken as the definition of what it means to solve a task. In particular, no proof is provided of the fact that this abstract topological definition agrees with a more concrete operational definition of task solvability. In this paper, we bridge this gap by proving a version of Herlihy and Shavit’s theorem that applies to any kind of object. First, we start with a very general way of specifying concurrent objects, and we define what it means to implement an object B in a computational model where the processes are allowed to communicate through shared objects A_1, ..., A_k. Then, we derive the notion of a decision task as a special case of concurrent object. Finally, we prove an analogue of Herlihy and Shavit’s theorem in this context. In particular, our version of the theorem subsumes all the uses of the combinatorial topology approach that we are aware of.
Cite as

Jérémy Ledent and Samuel Mimram. A Sound Foundation for the Topological Approach to Task Solvability. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ledent_et_al:LIPIcs.CONCUR.2019.34,
  author =	{Ledent, J\'{e}r\'{e}my and Mimram, Samuel},
  title =	{{A Sound Foundation for the Topological Approach to Task Solvability}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{34:1--34:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.34},
  URN =		{urn:nbn:de:0030-drops-109365},
  doi =		{10.4230/LIPIcs.CONCUR.2019.34},
  annote =	{Keywords: Fault-tolerant protocols, Asynchronous computability, Combinatorial topology, Protocol complex, Distributed task}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2018.3
Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk)

Authors: Rob van Glabbeek

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

Abstract
A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's, Peterson's and Lamport's bakery are meant to be speed independent. In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however. This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras.
Cite as

Rob van Glabbeek. Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{vanglabbeek:LIPIcs.CONCUR.2018.3,
  author =	{van Glabbeek, Rob},
  title =	{{Is Speed-Independent Mutual Exclusion Implementable?}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{3:1--3:1},
  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.3},
  URN =		{urn:nbn:de:0030-drops-95415},
  doi =		{10.4230/LIPIcs.CONCUR.2018.3},
  annote =	{Keywords: Mutual exclusion, speed independence, concurrent reading and writing, liveness, justness}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.25
Precongruence Formats with Lookahead through Modal Decomposition

Authors: Wan Fokkink and Rob J. van Glabbeek

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.
Cite as

Wan Fokkink and Rob J. van Glabbeek. Precongruence Formats with Lookahead through Modal Decomposition. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fokkink_et_al:LIPIcs.CSL.2017.25,
  author =	{Fokkink, Wan and van Glabbeek, Rob J.},
  title =	{{Precongruence Formats with Lookahead through Modal Decomposition}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.25},
  URN =		{urn:nbn:de:0030-drops-76776},
  doi =		{10.4230/LIPIcs.CSL.2017.25},
  annote =	{Keywords: Structural Operational Semantics, Compositionality, Congruence, Modal Logic, Modal Decomposition, Lookahead}
}
  • Refine by Author
  • 1 Fokkink, Wan
  • 1 Ledent, Jérémy
  • 1 Mimram, Samuel
  • 1 van Glabbeek, Rob
  • 1 van Glabbeek, Rob J.

  • Refine by Classification
  • 2 Theory of computation → Concurrency

  • Refine by Keyword
  • 1 Asynchronous computability
  • 1 Combinatorial topology
  • 1 Compositionality
  • 1 Congruence
  • 1 Distributed task
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2017
  • 1 2018
  • 1 2019

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