Algorithms for shared-memory systems

在现代多核计算机中，许多进程可以并发运行。为了利用这些计算机的处理能力，进程必须能够有效地相互通信，以便协调它们的工作，以便它们能够协作解决问题。这些进程通过访问共享内存进行通信。系统硬件提供了访问该内存的低级操作，但如果将内存中的信息组织成可以通过更复杂的操作访问的高级数据结构，对程序员来说会更方便。本文研究的主线是从硬件提供的低级原语操作中高效地实现高级数据结构。特别是，我对无锁数据结构感兴趣，它允许多个进程同时访问相同的数据，但这需要进程之间的仔细协调，以确保一个进程的更新不会干扰其他进程对相同数据的更新或读取。*我的学生和我将设计新颖的共享数据结构，并证明它们是正确的。除了构建手工制作的、高效的单个数据结构实现之外，我们还将寻找允许实现数据结构类的通用技术。这些数据结构将通过经验评估，但也将通过证明执行一组操作所需时间的上限来进行理论评估。这些数据结构的正确性证明通常相当复杂，因为必须考虑所有可能的方法，即不同进程的低级步骤在执行高级操作时可以交错，这会导致用于访问数据结构的代码可以由一组进程执行的不同可能方式的数量呈指数级增长。因此，编写这些证明是一个耗时且容易出错的过程。我们还将寻找使用机器可检查校样的方法，使这一过程的某些部分自动化。除了提高我们对数据结构正确性的信心外，这种方法还将使这种数据结构的设计者更容易修改和优化它们，而不必从头开始重新证明它们的正确性。*这项关于共享数据结构的实际实现的工作将得到更多关于分布式计算基础的理论工作的补充。例如，我的学生和我将致力于证明复杂性下界，这表明每一个解决特定问题的可能算法都必须至少使用一定的时间或空间。这些界限有助于理解共享内存计算的基本限制，并有助于确定我们何时应该停止寻找更好的算法。

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.