Algorithms for shared-memory systems

共享内存系统的算法

• 批准号: RGPIN-2018-05935
• 负责人: Ruppert, Eric
• 金额: $ 2.04万
• 依托单位: York University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750076
• 关键词: Algorithms; 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.

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