Search

We present Locksynth, a tool that automatically derives synchronization needed for destructive updates to concurrent data structures that involve a constant number of shared heap memory write operations. Locksynth serves as the implementation of our prior work on deriving abstract synchronization code. Designing concurrent data structures involves inferring correct synchronization code starting with a prior understanding of the sequential data structure's operations. Further, an understanding of shared memory model and the synchronization primitives is also required. The reasoning involved transforming a sequential data structure into its concurrent version can be performed using Answer Set Programming and we mechanized our approach in previous work. The reasoning involves deduction and abduction that can be succinctly modeled in ASP. We assume that the abstract sequential code of the data structure's operations is provided, alongside axioms that describe concurrent behavior. This information is used to automatically derive concurrent code for that data structure, such as dictionary operations for linked lists and binary search trees that involve a constant number of destructive update operations. We also are able to infer the correct set of locks (but not code synthesis) for external height-balanced binary search trees that involve left/right tree rotations. Locksynth performs the analyses required to infer correct sets of locks and as a final step, also derives the C++ synchronization code for the synthesized data structures. We also provide a performance analysis of the C++ code synthesized by Locksynth with the hand-crafted versions available from the Synchrobench microbenchmark suite. To the best of our knowledge, our tool is the first to employ ASP as a backend reasoner to perform concurrent data structure synthesis.

Mutual exclusion is one of the most commonly used techniques to handle contention in concurrent systems. Traditionally, mutual exclusion algorithms have been designed under the assumption that a process does not fail while acquiring/releasing a lock or while executing its critical section. However, failures do occur in real life, potentially leaving the lock in an inconsistent state. This gives rise to the problem of recoverable mutual exclusion (RME) that involves designing a mutual exclusion (ME) algorithm that can tolerate failures, while maintaining safety and liveness properties. In this work, we present a framework that transforms any algorithm that solves the RME problem into an algorithm that can also simultaneously adapt to (1) the number of processes competing for the lock, as well as (2) the number of failures that have occurred in the recent past, while maintaining the correctness and performance properties of the underlying RME algorithm. Additionally, the algorithm constructed as a result of this transformation adds certain desirable properties like fairness (a variation of FCFS) and bounded recovery. Assume that the worst-case RMR complexity of a critical section request in the underlying RME algorithm is $R(n)$. Then, our framework yields an RME algorithm for which the worst-case RMR complexity of a critical section request is given by $\mathcal{O}(\min \{\ddot{c}, \sqrt{F+1}, R(n)\})$, where $\ddot{c}$ denotes the point contention of the request and $F$ denotes the number of failures in the recent past of the request. We further extend our framework by presenting a novel memory reclamation algorithm to bound the worst-case space complexity of the RME algorithm. The memory reclamation techniques maintain the fairness, performance and correctness properties of our transformation and is general enough to be employed to bound the space of other RME algorithms., Comment: arXiv admin note: substantial text overlap with arXiv:2006.07086

We tackle the problem of automatically designing concurrent data structure operations given a sequential data structure specification and knowledge about concurrent behavior. Designing concurrent code is a non-trivial task even in simplest of cases. Humans often design concurrent data structure operations by transforming sequential versions into their respective concurrent versions. This requires an understanding of the data structure, its sequential behavior, thread interactions during concurrent execution and shared memory synchronization primitives. We mechanize this design process using automated commonsense reasoning. We assume that the data structure description is provided as axioms alongside the sequential code of its algebraic operations. This information is used to automatically derive concurrent code for that data structure, such as dictionary operations for linked lists and binary search trees. Knowledge in our case is expressed using Answer Set Programming (ASP), and we employ deduction and abduction -- just as humans do -- in the reasoning involved. ASP allows for succinct modeling of first order theories of pointer data structures, run-time thread interactions and shared memory synchronization. Our reasoner can systematically make the same judgments as a human reasoner, while constructing provably safe concurrent code. We present several reasoning challenges involved in transforming the sequential data structure into its equivalent concurrent version. All the reasoning tasks are encoded in ASP and our reasoner can make sound judgments to transform sequential code into concurrent code. To the best of our knowledge, our work is the first one to use commonsense reasoning to automatically transform sequential programs into concurrent code. We also have developed a tool that we describe that relies on state-of-the-art ASP solvers and performs the reasoning tasks involved to generate concurrent code., Comment: In Proceedings ICLP 2021, arXiv:2109.07914. arXiv admin note: substantial text overlap with arXiv:2011.04045

Mutual exclusion (ME) is a commonly used technique to handle conflicts in concurrent systems. With recent advancements in non-volatile memory technology, there is an increased focus on the problem of recoverable mutual exclusion (RME), a special case of ME where processes can fail and recover. However, in order to ensure that the problem of RME is also of practical interest, and not just a theoretical one, memory reclamation poses as a major obstacle in several RME algorithms. Often RME algorithms need to allocate memory dynamically, which increases the memory footprint of the algorithm over time. These algorithms are typically not equipped with suitable garbage collection due to concurrency and failures. In this work, we present the first "general" recoverable algorithm for memory reclamation in the context of recoverable mutual exclusion. Our algorithm can be plugged into any RME algorithm very easily and preserves all correctness property and most desirable properties of the algorithm. The space overhead of our algorithm is $\mathcal{O}(n^2 * sizeof(node)\ )$, where $n$ is the total number of processes in the system. In terms of remote memory references (RMRs), our algorithm is RMR-optimal, i.e, it has a constant RMR overhead per passage. Our RMR and space complexities are applicable to both $CC$ and $DSM$ memory models., Comment: arXiv admin note: text overlap with arXiv:2006.07086

In this paper we tackle the problem of automatically designing concurrent data structure operations given a sequential data structure specification and knowledge about concurrent behavior. Designing concurrent code is a non-trivial task even in simplest of cases. Humans often design concurrent data structure operations by transforming sequential versions into their respective concurrent versions. This requires an understanding of the data structure, its sequential behavior, thread interactions during concurrent execution and shared memory synchronization primitives. We mechanize this design process using automated commonsense reasoning. We assume that the data structure description is provided as axioms alongside the sequential code of its algebraic operations. This information is used to automatically derive concurrent code for that data structure, such as dictionary operations for linked lists and binary search trees. Knowledge in our case is expressed using Answer Set Programming (ASP), and we employ deduction, induction and abduction---just as humans do---in the reasoning involved. ASP allows for succinct modeling of first order theories of pointer data structures, run-time thread interactions and shared memory synchronization. Our reasoner can systematically make the same judgments as a human reasoner while constructing provably safe concurrent code. We present several reasoning challenges involved in transforming the sequential data structure into its equivalent concurrent version. All the reasoning tasks are encoded in ASP and our reasoner can make sound judgments to transform sequential code into concurrent code. To the best of our knowledge, our work is the first one to use commonsense reasoning to automatically transform sequential programs into concurrent code.

We develop an inductive proof-technique to generate imperative programs for pointer data structures from behavioural specifications expressed in the Answer Set Programming (ASP) formalism. ASP is a non-monotonic logic based formalism that employs negation-as-failure which helps emulate the human thought process, allowing domain experts to model desired system behaviour succinctly. We argue in this paper that ASP's reliance on negation-as-failure makes it a better formalism than those based on first-order logic for writing formal specifications. We assume the a domain expert provides the representation of inductively defined data structures along with a specification of its operations. Our procedures combined with our novel proof-technique reason over the specifications and automatically generate an imperative program. Our proof-technique leverages the idea of partial deduction to simplify logical specifications. By algebraically simplifying logical specifications we arrive at a residual specification which can be interpreted as an appropriate imperative program. This work is in the realm of constructing programs that are correct according to a given specification.

Mutual exclusion (ME) is one of the most commonly used techniques to handle conflicts in concurrent systems. Traditionally, mutual exclusion algorithms have been designed under the assumption that a process does not fail while acquiring/releasing a lock or while executing its critical section. However, failures do occur in real life, potentially leaving the lock in an inconsistent state. This gives rise to the problem of \emph{recoverable mutual exclusion (RME)} that involves designing a mutual exclusion algorithm that can tolerate failures, while maintaining safety and liveness properties. One of the important measures of performance of any ME algorithm, including an RME algorithm, is the number of \emph{remote memory references (RMRs)} made by a process (for acquiring and releasing a lock as well as recovering the lock structure after a failure). The best known RME algorithm solves the problem for $n$ processes in sub-logarithmic number of RMRs, given by $\mathcal{O}(\frac{\log n}{\log \log n})$, irrespective of the number of failures in the system. In this work, we present a new algorithm for solving the RME problem whose RMR complexity gradually \emph{adapts} to the number of failures that have occurred in the system "recently". In the absence of failures, our algorithm generates only $\mathcal{O}(1)$ RMRs. Furthermore, its RMR complexity is given by $\mathcal{O}(\min\{ \sqrt{F}, \frac{\log n}{\log \log n} \})$ where $F$ is the total number of failures in the "recent" past. In addition to read and write instructions, our algorithm uses compare-and-swap (\CAS{}) and fetch-and-store (\FAS{}) hardware instructions, both of which are commonly available in most modern processors.

The group mutual exclusion (GME) problem is a generalization of the classical mutual exclusion problem in which every critical section is associated with a type or session. Critical sections belonging to the same session can execute concurrently, whereas critical sections belonging to different sessions must be executed serially. The well-known read-write mutual exclusion problem is a special case of the group mutual exclusion problem. In this work, we present a novel GME algorithm for an asynchronous shared-memory system that, in addition to satisfying lockout freedom, bounded exit and concurrent entering properties, has O(1) step-complexity when the system contains no conflicting requests as well as O(1) space-complexity per GME object when the system contains sufficient number of GME objects. To the best of our knowledge, no existing GME algorithm has O(1) step-complexity for concurrent entering. Moreover, most existing GME algorithms have {\Omega}(n) space complexity per GME object, where n denotes the number of processes in the system. We also show that our GME algorithm can be easily modified to use bounded space variables.

In this work, we consider the problem of placing replicas in a data center or storage area network, represented as a digraph, so as to lexico-minimize a previously proposed reliability measure which minimizes the impact of all failure events in the model in decreasing order of severity. Prior work focuses on the special case in which the digraph is an arborescence. In this work, we consider the broader class of multitrees: digraphs in which the subgraph induced by vertices reachable from a fixed node forms a tree. We parameterize multitrees by their number of "roots" (nodes with in-degree zero), and rule out membership in the class of fixed-parameter tractable problems (FPT) by showing that finding optimal replica placements in multitrees with 3 roots is NP-hard. On the positive side, we show that the problem of finding optimal replica placements in the class of \emph{untangled} multitrees is FPT, as parameterized by the replication factor $\rho$ and the number of roots $k$. Our approach combines dynamic programming (DP) with a novel tree decomposition to find an optimal placement of $\rho$ replicas on the leaves of a multitree with $n$ nodes and $k$ roots in $O(n^2\rho^{2k+3})$ time., Comment: 18 pages, 7 figures accepted for publication in COCOA 2017

In data centers, data replication is the primary method used to ensure availability of customer data. To avoid correlated failure, cloud storage infrastructure providers model hierarchical failure domains using a tree, and avoid placing a large number of data replicas within the same failure domain (i.e. on the same branch of the tree). Typical best practices ensure that replicas are distributed across failure domains, but relatively little is known concerning optimization algorithms for distributing data replicas. Using a hierarchical model, we answer how to distribute replicas across failure domains optimally. We formulate a novel optimization problem for replica placement in data centers. As part of our problem, we formalize and explain a new criterion for optimizing a replica placement. Our overall goal is to choose placements in which correlated failures disable as few replicas as possible. We provide two optimization algorithms for dependency models represented by trees. We first present an $O(n + \rho \log \rho)$ time dynamic programming algorithm for placing $\rho$ replicas of a single file on the leaves (representing servers) of a tree with $n$ vertices. We next consider the problem of placing replicas of $m$ blocks of data, where each block may have different replication factors. For this problem, we give an exact algorithm which runs in polynomial time when the skew, the difference in the number of replicas between the largest and smallest blocks of data, is constant., Comment: 64 pages, 9 figures. Preprint submission to Theoretical Computer Science

An important first step when deploying a wireless ad hoc network is neighbor discovery in which every node attempts to determine the set of nodes it can communicate with in one wireless hop. In the recent years, cognitive radio (CR) technology has gained attention as an attractive approach to alleviate spectrum congestion. A cognitive radio transceiver can operate over a wide range of frequencies, possibly scanning multiple frequency bands. A cognitive radio node can opportunistically utilize unused wireless spectrum without interference from other wireless devices in its vicinity. Due to spatial variations in frequency usage and hardware variations in radio transceivers, different nodes in the network may perceive different subsets of frequencies available to them for communication. This heterogeneity in the available channel sets across the network increases the complexity of solving the neighbor discovery problem in a cognitive radio network. In this work, we design and analyze several randomized algorithms for neighbor discovery in such a (heterogeneous) network under a variety of assumptions (e.g. maximum node degree known or unknown) for both synchronous and asynchronous systems under minimal knowledge. We also show that our randomized algorithms are naturally suited to tolerate unreliable channels and adversarial attacks., Comment: 54 pages, 5 figures, 1 table, 6 algorithms, accepted in Journal of Parallel and Distributed Computing

A new model of causal failure is presented and used to solve a novel replica placement problem in data centers. The model describes dependencies among system components as a directed graph. A replica placement is defined as a subset of vertices in such a graph. A criterion for optimizing replica placements is formalized and explained. In this work, the optimization goal is to avoid choosing placements in which a single failure event is likely to wipe out multiple replicas. Using this criterion, a fast algorithm is given for the scenario in which the dependency model is a tree. The main contribution of the paper is an $O(n + \rho \log \rho)$ dynamic programming algorithm for placing $\rho$ replicas on a tree with $n$ vertices. This algorithm exhibits the interesting property that only two subproblems need to be recursively considered at each stage. An $O(n^2 \rho)$ greedy algorithm is also briefly reported., Comment: 22 pages, 7 figures, 4 algorithm listings