3 Search Results for "Jayanti, Siddhartha"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.30
Verifying Lock-Free Search Structure Templates

Authors: Nisarg Patel, Dennis Shasha, and Thomas Wies

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
We present and verify template algorithms for lock-free concurrent search structures that cover a broad range of existing implementations based on lists and skiplists. Our linearizability proofs are fully mechanized in the concurrent separation logic Iris. The proofs are modular and cover the broader design space of the underlying algorithms by parameterizing the verification over aspects such as the low-level representation of nodes and the style of data structure maintenance. As a further technical contribution, we present a mechanization of a recently proposed method for reasoning about future-dependent linearization points using hindsight arguments. The mechanization builds on Iris' support for prophecy reasoning and user-defined ghost resources. We demonstrate that the method can help to reduce the proof effort compared to direct prophecy-based proofs.
Cite as

Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-Free Search Structure Templates. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 30:1-30:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{patel_et_al:LIPIcs.ECOOP.2024.30,
  author =	{Patel, Nisarg and Shasha, Dennis and Wies, Thomas},
  title =	{{Verifying Lock-Free Search Structure Templates}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{30:1--30:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.30},
  URN =		{urn:nbn:de:0030-drops-208797},
  doi =		{10.4230/LIPIcs.ECOOP.2024.30},
  annote =	{Keywords: skiplists, lock-free, separation logic, linearizability, future-dependent linearization points, hindsight reasoning}
}
Document
DOI: 10.4230/LIPIcs.DISC.2023.25
Durable Algorithms for Writable LL/SC and CAS with Dynamic Joining

Authors: Prasad Jayanti, Siddhartha Jayanti, and Sucharita Jayanti

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)

Abstract
We present durable implementations for two well known universal primitives - CAS (compare-and-swap), and its ABA-free counter-part LLSC (load-linked, store-conditional). Our implementations satisfy method-based recoverable linearizability (MRL) and method-based detectability (M-detectability) - novel correctness conditions that require only a simple usage pattern to guarantee resilience to individual process crashes (and system-wide crashes), including in implementations with nesting. Additionally, our implementations are: writable, meaning they support a Write() operation; have constant time complexity per operation; allow for dynamic joining, meaning newly created processes (a.k.a. threads) of arbitrary names can join a protocol and access our implementations; and have adaptive space complexity, meaning the space use scales in the number of processes n that actually use the objects, as opposed to previous protocols whose space complexity depends on N, the maximum number of processes that the protocol is designed for. Our durable Writable-CAS implementation, DuraCAS, requires O(m + n) space to support m objects that get accessed by n processes, improving on the state-of-the-art O(m + N²). By definition, LLSC objects must store "contexts" in addition to object values. Our Writable-LLSC implementation, DuraLL, requires O(m + n + C) space, where C is the number of "contexts" stored across all the objects. While LLSC has an advantage over CAS due to being ABA-free, the object definition seems to require additional space usage. To address this trade-off, we define an External Context (EC) variant of LLSC. Our EC Writable-LLSC implementation is ABA-free and has a space complexity of just O(m + n). To our knowledge, our algorithms are the first durable CAS algorithms that allow for dynamic joining, and are the first to exhibit adaptive space complexity. To our knowledge, we are the first to implement any type of durable LLSC objects.
Cite as

Prasad Jayanti, Siddhartha Jayanti, and Sucharita Jayanti. Durable Algorithms for Writable LL/SC and CAS with Dynamic Joining. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jayanti_et_al:LIPIcs.DISC.2023.25,
  author =	{Jayanti, Prasad and Jayanti, Siddhartha and Jayanti, Sucharita},
  title =	{{Durable Algorithms for Writable LL/SC and CAS with Dynamic Joining}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.25},
  URN =		{urn:nbn:de:0030-drops-191510},
  doi =		{10.4230/LIPIcs.DISC.2023.25},
  annote =	{Keywords: durable, recoverable, detectable, persistent memory, dynamic joining, LL/SC, CAS}
}
Document
DOI: 10.4230/LIPIcs.DISC.2021.25
Fast Arrays: Atomic Arrays with Constant Time Initialization

Authors: Siddhartha Jayanti and Julian Shun

Published in: LIPIcs, Volume 209, 35th International Symposium on Distributed Computing (DISC 2021)

Abstract
Some algorithms require a large array, but only operate on a small fraction of its indices. Examples include adjacency matrices for sparse graphs, hash tables, and van Emde Boas trees. For such algorithms, array initialization can be the most time-consuming operation. Fast arrays were invented to avoid this costly initialization. A fast array is a software implementation of an array, such that the entire array can be initialized in just constant time. While algorithms for sequential fast arrays have been known for a long time, to the best of our knowledge, there are no previous algorithms for concurrent fast arrays. We present the first such algorithms in this paper. Our first algorithm is linearizable and wait-free, uses only linear space, and supports all operations - initialize, read, and write - in constant time. Our second algorithm enhances the first to additionally support all the read-modify-write operations available in hardware (such as compare-and-swap) in constant time.
Cite as

Siddhartha Jayanti and Julian Shun. Fast Arrays: Atomic Arrays with Constant Time Initialization. In 35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{jayanti_et_al:LIPIcs.DISC.2021.25,
  author =	{Jayanti, Siddhartha and Shun, Julian},
  title =	{{Fast Arrays: Atomic Arrays with Constant Time Initialization}},
  booktitle =	{35th International Symposium on Distributed Computing (DISC 2021)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-210-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{209},
  editor =	{Gilbert, Seth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021.25},
  URN =		{urn:nbn:de:0030-drops-148278},
  doi =		{10.4230/LIPIcs.DISC.2021.25},
  annote =	{Keywords: fast array, linearizable, wait-free, asynchronous, multiprocessor, constant time, space efficient, data structure}
}
  • Refine by Author
  • 2 Jayanti, Siddhartha
  • 1 Jayanti, Prasad
  • 1 Jayanti, Sucharita
  • 1 Patel, Nisarg
  • 1 Shasha, Dennis
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Concurrent algorithms
  • 2 Theory of computation → Data structures design and analysis
  • 1 Computer systems organization → Dependable and fault-tolerant systems and networks
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Distributed algorithms
  • Show More...

  • Refine by Keyword
  • 1 CAS
  • 1 LL/SC
  • 1 asynchronous
  • 1 constant time
  • 1 data structure
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2021
  • 1 2023
  • 1 2024

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