Grant: Discovery Grants Program - Individual

In modern multicore computers, many processes can run concurrently. In order to exploit the processing power of these computers, processes must be able to communicate with one another efficiently in order to coordinate their work, so that they can cooperatively solve problems. The processes communicate by accessing a shared memory. The system hardware provides low-level operations to access this memory, but it is more convenient for programmers if the information in memory is organized into high-level data structures that can be accessed by more complex operations. The main thread of my research is on the efficient implementation of the high-level data structures from the low-level primitive operations provided in hardware. In particular, I am interested in lock-free data structures, which allow many processes to access the same data concurrently, but this requires careful coordination between processes to ensure that updates by one process do not interfere with updates or reads of the same data by other processes.My students and I will design novel shared data structures and prove them correct. In addition to building handcrafted, efficient implementations of individual data structures, we will also look for general techniques that permit classes of data structures to be implemented. These data structures will be evaluated empirically, but also theoretically by proving upper bounds on the amount of time needed to perform sets of operations. The proofs of correctness for these data structures are often quite intricate, because one must consider all possible ways that the low-level steps of different processes can be interleaved when they perform high-level operations, and this causes an exponential blow up in the number of different possible ways that the code used to access the data structure can be executed by a collection of processes. Thus, writing these proofs is a time-consuming and error-prone process. We will also look for ways to use machine-checkable proofs to automate parts of this process. Besides improving our confidence in the correctness of a data structure, this approach will make it easier for designers of such data structures to modify and optimize them without having to reprove their correctness from scratch.This work on practical implementations of shared data structures will be complemented by more theoretical work on the foundations of distributed computing. For example, my students and I will work on proving complexity lower bounds, which show that every possible algorithm that solves a particular problem must use at least a certain amount of time or space. These bounds are useful for understanding the fundamental limits of shared-memory computing, and for determining when we should stop looking for better algorithms.