Search Results

Documents authored by Morrison, Adam

Document
DOI: 10.4230/LIPIcs.OPODIS.2020.15
Recoverable, Abortable, and Adaptive Mutual Exclusion with Sublogarithmic RMR Complexity

Authors: Daniel Katzan and Adam Morrison

Published in: LIPIcs, Volume 184, 24th International Conference on Principles of Distributed Systems (OPODIS 2020)

Abstract
We present the first recoverable mutual exclusion (RME) algorithm that is simultaneously abortable, adaptive to point contention, and with sublogarithmic RMR complexity. Our algorithm has O(min(K,log_W N)) RMR passage complexity and O(F + min(K,log_W N)) RMR super-passage complexity, where K is the number of concurrent processes (point contention), W is the size (in bits) of registers, and F is the number of crashes in a super-passage. Under the standard assumption that W = Θ(log N), these bounds translate to worst-case O((log N)/(log log N)) passage complexity and O(F + (log N)/(log log N)) super-passage complexity. Our key building blocks are: - A D-process abortable RME algorithm, for D ≤ W, with O(1) passage complexity and O(1+F) super-passage complexity. We obtain this algorithm by using the Fetch-And-Add (FAA) primitive, unlike prior work on RME that uses Fetch-And-Store (FAS/SWAP). - A generic transformation that transforms any abortable RME algorithm with passage complexity of B < W, into an abortable RME lock with passage complexity of O(min(K,B)).
Cite as

Daniel Katzan and Adam Morrison. Recoverable, Abortable, and Adaptive Mutual Exclusion with Sublogarithmic RMR Complexity. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 184, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{katzan_et_al:LIPIcs.OPODIS.2020.15,
  author =	{Katzan, Daniel and Morrison, Adam},
  title =	{{Recoverable, Abortable, and Adaptive Mutual Exclusion with Sublogarithmic RMR Complexity}},
  booktitle =	{24th International Conference on Principles of Distributed Systems (OPODIS 2020)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-176-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{184},
  editor =	{Bramas, Quentin and Oshman, Rotem and Romano, Paolo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2020.15},
  URN =		{urn:nbn:de:0030-drops-135004},
  doi =		{10.4230/LIPIcs.OPODIS.2020.15},
  annote =	{Keywords: Mutual exclusion, recovery, non-volatile memory}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.23
Order out of Chaos: Proving Linearizability Using Local Views

Authors: Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning about the view of the memory obtained by the threads, because as they execute, threads observe different fragments of memory from different points in time. Until today, every linearizability proof has tackled this challenge from scratch. We present a unifying proof argument for the correctness of unsynchronized traversals, and apply it to prove the linearizability of several highly concurrent search data structures, including an optimistic self-balancing binary search tree, the Lazy List and a lock-free skip list. Our framework harnesses sequential reasoning about the view of a thread, considering the thread as if it traverses the data structure without interference from other operations. Our key contribution is showing that properties of reachability along search paths can be deduced for concurrent traversals from such interference-free traversals, when certain intuitive conditions are met. Basing the correctness of traversals on such local view arguments greatly simplifies linearizability proofs. At the heart of our result lies a notion of order on the memory, corresponding to the order in which locations in memory are read by the threads, which guarantees a certain notion of consistency between the view of the thread and the actual memory. To apply our framework, the user proves that the data structure satisfies two conditions: (1) acyclicity of the order on memory, even when it is considered across intermediate memory states, and (2) preservation of search paths to locations modified by interfering writes. Establishing the conditions, as well as the full linearizability proof utilizing our proof argument, reduces to simple concurrent reasoning. The result is a clear and comprehensible correctness proof, and elucidates common patterns underlying several existing data structures.
Cite as

Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham. Order out of Chaos: Proving Linearizability Using Local Views. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{feldman_et_al:LIPIcs.DISC.2018.23,
  author =	{Feldman, Yotam M. Y. and Enea, Constantin and Morrison, Adam and Rinetzky, Noam and Shoham, Sharon},
  title =	{{Order out of Chaos: Proving Linearizability Using Local Views}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.23},
  URN =		{urn:nbn:de:0030-drops-98124},
  doi =		{10.4230/LIPIcs.DISC.2018.23},
  annote =	{Keywords: concurrency and synchronization, concurrent data structures, lineariazability, optimistic concurrency control, verification and formal methods}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2015.15
A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms

Authors: Orr Tamir, Adam Morrison, and Noam Rinetzky

Published in: LIPIcs, Volume 46, 19th International Conference on Principles of Distributed Systems (OPODIS 2015)

Abstract
Existing concurrent priority queues do not allow to update the priority of an element after its insertion. As a result, algorithms that need this functionality, such as Dijkstra's single source shortest path algorithm, resort to cumbersome and inefficient workarounds. We report on a heap-based concurrent priority queue which allows to change the priority of an element after its insertion. We show that the enriched interface allows to express Dijkstra's algorithm in a more natural way, and that its implementation, using our concurrent priority queue, outperform existing algorithms.
Cite as

Orr Tamir, Adam Morrison, and Noam Rinetzky. A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 46, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{tamir_et_al:LIPIcs.OPODIS.2015.15,
  author =	{Tamir, Orr and Morrison, Adam and Rinetzky, Noam},
  title =	{{A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms}},
  booktitle =	{19th International Conference on Principles of Distributed Systems (OPODIS 2015)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-98-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{46},
  editor =	{Anceaume, Emmanuelle and Cachin, Christian and Potop-Butucaru, Maria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2015.15},
  URN =		{urn:nbn:de:0030-drops-66068},
  doi =		{10.4230/LIPIcs.OPODIS.2015.15},
  annote =	{Keywords: priority queues, concurrent data structures, Dijkstra's single-source shortest path algorithm}
}
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 About DROPS Imprint Privacy Contact