-
Constant RMR Recoverable Mutex under System-wide Crashes
Authors:
Prasad Jayanti,
Siddhartha Jayanti,
Anup Joshi
Abstract:
We design two Recoverable Mutual Exclusion (RME) locks for the system-wide crash model. Our first algorithm requires only $O(1)$ space per process, and achieves $O(1)$ worst-case RMR complexity in the CC model. Our second algorithm enhances the first algorithm to achieve (the same) $O(1)$ space per process and $O(1)$ worst-case RMR complexity in both the CC and DSM models. Furthermore, both algori…
▽ More
We design two Recoverable Mutual Exclusion (RME) locks for the system-wide crash model. Our first algorithm requires only $O(1)$ space per process, and achieves $O(1)$ worst-case RMR complexity in the CC model. Our second algorithm enhances the first algorithm to achieve (the same) $O(1)$ space per process and $O(1)$ worst-case RMR complexity in both the CC and DSM models. Furthermore, both algorithms allow dynamically created threads of arbitrary names to join the protocol and access the locks. To our knowledge, these are the only RME locks to achieve worst-case $O(1)$ RMR complexity assuming nothing more than standard hardware support. In light of Chan and Woelfel's $Ω(\log n / \log\log n)$ worst-case RMR lower bound for RME in the individual crash model, our results show a separation between the system-wide crash and individual crash models in worst-case RMR complexity in both the CC and DSM models.
△ Less
Submitted 1 February, 2023;
originally announced February 2023.
-
A Universal Technique for Machine-Certified Proofs of Linearizable Algorithms
Authors:
Prasad Jayanti,
Siddhartha Jayanti,
Ugur Y. Yavuz,
Lizzie Hernandez
Abstract:
Linearizability has been the long standing gold standard for consistency in concurrent data structures. However, proofs of linearizability can be long and intricate, hard to produce, and extremely time consuming even to verify. In this work, we address this issue by introducing simple $universal$, $sound$, and $complete$ proof methods for producing machine-verifiable proofs of linearizability and…
▽ More
Linearizability has been the long standing gold standard for consistency in concurrent data structures. However, proofs of linearizability can be long and intricate, hard to produce, and extremely time consuming even to verify. In this work, we address this issue by introducing simple $universal$, $sound$, and $complete$ proof methods for producing machine-verifiable proofs of linearizability and its close cousin, strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti's single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the Temporal Logic of Actions Proof System).
△ Less
Submitted 13 February, 2023; v1 submitted 1 February, 2023;
originally announced February 2023.
-
Durable Algorithms for Writable LL/SC and CAS with Dynamic Joining
Authors:
Prasad Jayanti,
Siddhartha Jayanti,
Sucharita Jayanti
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). All 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…
▽ More
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). All 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 complexities, meaning the space use scales in the number of processes $n$ that actually use the objects, as opposed to previous protocols which are designed for a maximum number of processes $N$. 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^2)$. 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, we are the first to present durable CAS algorithms that allow for dynamic joining, and our algorithms are the first to exhibit adaptive space complexities. To our knowledge, we are the first to implement any type of durable LLSC objects.
△ Less
Submitted 31 January, 2023;
originally announced February 2023.
-
Recoverable Mutual Exclusion with Abortability
Authors:
Prasad Jayanti,
Anup Joshi
Abstract:
Recent advances in non-volatile main memory (NVRAM) technology have spurred research on designing algorithms that are resilient to process crashes. This paper is a fuller version of our conference paper \cite{jayanti:rmeabort}, which presents the first Recoverable Mutual Exclusion (RME) algorithm that supports abortability. Our algorithm uses only the read, write, and CAS operations, which are com…
▽ More
Recent advances in non-volatile main memory (NVRAM) technology have spurred research on designing algorithms that are resilient to process crashes. This paper is a fuller version of our conference paper \cite{jayanti:rmeabort}, which presents the first Recoverable Mutual Exclusion (RME) algorithm that supports abortability. Our algorithm uses only the read, write, and CAS operations, which are commonly supported by multiprocessors. It satisfies FCFS and other standard properties.
Our algorithm is also adaptive. On DSM and Relaxed-CC multiprocessors, a process incurs $O(\min(k, \log n))$ RMRs in a passage and $O(f+ \min(k, \log n))$ RMRs in an attempt, where $n$ is the number of processes that the algorithm is designed for, $k$ is the point contention of the passage or the attempt, and $f$ is the number of times that $p$ crashes during the attempt. On a Strict CC multiprocessor, the passage and attempt complexities are $O(n)$ and $O(f+n)$.
Attiya et al. proved that, with any mutual exclusion algorithm, a process incurs at least $Ω(\log n)$ RMRs in a passage, if the algorithm uses only the read, write, and CAS operations \cite{Attiya:lbound}. This lower bound implies that the worst-case RMR complexity of our algorithm is optimal for the DSM and Relaxed CC multiprocessors.
△ Less
Submitted 5 December, 2020;
originally announced December 2020.
-
A Recoverable Mutex Algorithm with Sub-logarithmic RMR on Both CC and DSM
Authors:
Prasad Jayanti,
Siddhartha Jayanti,
Anup Joshi
Abstract:
In light of recent advances in non-volatile main memory technology, Golab and Ramaraju reformulated the traditional mutex problem into the novel {\em Recoverable Mutual Exclusion} (RME) problem. In the best known solution for RME, due to Golab and Hendler from PODC 2017, a process incurs at most $O(\frac{\log n}{\log \log n})$ remote memory references (RMRs) per passage, where a passage is an inte…
▽ More
In light of recent advances in non-volatile main memory technology, Golab and Ramaraju reformulated the traditional mutex problem into the novel {\em Recoverable Mutual Exclusion} (RME) problem. In the best known solution for RME, due to Golab and Hendler from PODC 2017, a process incurs at most $O(\frac{\log n}{\log \log n})$ remote memory references (RMRs) per passage, where a passage is an interval from when a process enters the Try section to when it subsequently returns to Remainder. Their algorithm, however, guarantees this bound only for cache-coherent (CC) multiprocessors, leaving open the question of whether a similar bound is possible for distributed shared memory (DSM) multiprocessors.
We answer this question affirmatively by designing an algorithm that satisfies the same complexity bound as Golab and Hendler's for both CC and DSM multiprocessors. Our algorithm has some additional advantages over Golab and Hendler's: (i) its Exit section is wait-free, (ii) it uses only the Fetch-and-Store instruction, and (iii) on a CC machine our algorithm needs each process to have a cache of only $O(1)$ words, while their algorithm needs $O(n)$ words.
△ Less
Submitted 29 May, 2019; v1 submitted 3 April, 2019;
originally announced April 2019.
-
Constant Amortized RMR Complexity Deterministic Abortable Mutual Exclusion Algorithm for CC and DSM Models
Authors:
Prasad Jayanti,
Siddhartha Jayanti
Abstract:
The abortable mutual exclusion problem was introduced by Scott and Scherer to meet a need that arises in database and real time systems, where processes sometimes have to abandon their attempt to acquire a mutual exclusion lock to initiate recovery from a potential deadlock or to avoid overshooting a deadline. Algorithms of O(1) RMR complexity have been known for the standard mutual exclusion prob…
▽ More
The abortable mutual exclusion problem was introduced by Scott and Scherer to meet a need that arises in database and real time systems, where processes sometimes have to abandon their attempt to acquire a mutual exclusion lock to initiate recovery from a potential deadlock or to avoid overshooting a deadline. Algorithms of O(1) RMR complexity have been known for the standard mutual exclusion problem for both the Cache-Coherent (CC) and Distributed Shared Memory (DSM) models of multiprocessors, but whether O(1) RMR complexity is also achievable for abortable mutual exclusion has remained open for the 18 years that this problem has been investigated.
Jayanti gives a Theta(log n) worst case RMR complexity solution for both models, where n is the maximum number of processes that execute the algorithm concurrently. Giakouppis and Woelfel's algorithm, presented at PODC last year, is an O(1) amortized complexity algorithm, but it works only for the CC model, uses randomization, does not satisfy Starvation Freedom, and the O(1) amortized bound holds only in expectation and is proven for the a weak (oblivious) adversary model.
We design an algorithm that is free of these limitations: our algorithm is deterministic, supports fast aborts (a process completes an abort in O(1) steps), has a small space complexity of O(n), requires hardware support for only the Fetch&Store instruction, satisfies a novely defined First Come First Served for abortable locks, and most importantly, has O(1) amortized RMR complexity for both the CC and DSM models. Our algorithm is short and practical with fewer than a dozen lines of code, and is accompanied by a rigorous proof of mutual exclusion through invariants and of starvation-freedom and complexity analysis through distance and potential functions. Thus, modulo amortization, our result answers affirmatively the long standing open question described above.
△ Less
Submitted 12 September, 2018;
originally announced September 2018.
