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.
