SI2-SSE: LC/DC: Lockless Containers and Data Concurrency

多核编程要求我们改变设计和使用基本算法和数据结构的方式。这项研究代表了一种前瞻性和务实的方法，它将导致发现多处理器应用程序开发中有效数据和资源管理的关键原则。在这个项目的过程中，PI将为设计、验证和有效使用无锁和无等待的数据结构和算法创建新的方法和工具。所建议的方法将允许构建和使用轻量级多处理器算法，通过只支持用户应用程序所需的最小操作集和保证，从而实现最小开销。在这项工作中提出的想法将允许首创的技术，将在性能和软件重用方面带来巨大的提升；因此，商业和科学应用程序的开发人员的生产力将会提高。该研究将为基于工具的非阻塞算法规范和验证铺平道路，这将有助于多处理器程序的可靠性。这项工作将创建新的多处理器数据结构，提供无等待和无锁的进程。如果并发对象保证某个线程有进展，那么它就是无锁的。无等待算法保证所有线程都取得进展，从而消除了性能瓶颈和整个类的安全隐患，如饥饿、死锁和顺序违反。与顺序数据结构不同，并发容器必须在多个线程执行其操作时保持正确性。实现这种正确性会对操作的复杂性和性能产生负面影响。因此，并发容器的用户经常被迫牺牲功能或安全保证来实现期望的性能。在这里，PI将介绍替代功能模型的使用，这些模型将在程序中需要较少功能的部分提供高性能，而在程序中需要它的其他部分提供更多功能。本研究的成果包括：一系列经过正式验证的多处理器数据结构设计，包括队列、向量、环缓冲区、集合和哈希映射；无等待数据库；多资源锁管理器；一组统一的并发api，以协助数据结构的最终用户；以及一种规范这些容器的关键进度和正确性的技术。在这个项目下开发的所有软件都将在BSD许可证下发布，并将提供给广泛的研究和开发社区。

Multicore programming demands a change in the way we design and use fundamental algorithms and data structures. This research represents a forward-looking and pragmatic approach that will lead to the discovery of the key principles for effective data and resource management for multiprocessor application development. In the course of this project the PI will create new methodologies and tools for the design, verification, and effective use of lock-free and wait-free data structures and algorithms. The proposed methodology will allow for the construction and use of lightweight multiprocessor algorithms with minimal overhead by supporting only the minimal set of operations and guarantees required by the user's application. The ideas advanced in this work will allow first-of-a-kind technology that will deliver immense boost in performance and software reuse; thus productivity will increase for developers of commercial and scientific applications. This research will pave the way for tool-based specification and verification of nonblocking algorithms, which will help reliability of multiprocessor programs. This work will create novel multiprocessor data structures that provide wait-free and lock-free progress. A concurrent object is lock-free if it guarantees that some thread makes progress. A wait-free algorithm guarantees that all threads make progress, thus eliminating performance bottlenecks and entire classes of safety hazards such as starvation, deadlock, and order violations. Unlike a sequential data structure, a concurrent container must maintain correctness when multiple threads are performing its operations. Achieving this correctness adversely affects the complexity and performance of the operations. As a result, users of concurrent containers are often forced to sacrifice functionality or safety guarantees to achieve desired performance. Here, the PI will introduce the use of alternative function models that will deliver high performance in parts of the program that require less functionality and more functionality in other fragments of the program that need it. The deliverables of this research include: a collection of formally verified multiprocessor data structure designs including queues, vectors, ring buffers, sets, and hash maps; a wait-free database; a multiple resource lock manager; a set of unified concurrent APIs to assist the end users of the data structures; and a technique for specification of the key progress and correctness properties of these containers. All software developed under this project will be released under BSD License and will be made available to the broad research and development community.