The nation’s computing infrastructure utilizes multicore processors and multiprocessor hardware across the entire spectrum of systems from small mobile devices to huge data centers. These systems offer increased performance and scaling over single-processor systems, but at a significant cost: writing correct concurrent software is notoriously challenging. Programmers must take extreme care to orchestrate synchronization between concurrently running threads to avoid unintended interference while simultaneously eliminating synchronization whenever possible to avoid performance bottlenecks. To address this challenge, this project develops the Synchronicity tool to automatically synthesize high-performance concurrent software from simple specifications of the desired behavior. This research has the potential to reduce the costs of developing computing infrastructure, by eliminating the costly process of manually writing, testing, and reasoning about concurrent code, and it may reduce the hardware resources and energy required to meet computing needs.
Synchronicity starts with an initial programmer-provided description of a software component suitable execution on a single thread. It then uses counterexample-guided inductive synthesis to search for thread-safe concurrent components conforming to that specification. Synchronicity verifies thread safety using an extended form of Lipton’s theory of reduction. Multiple thread-safe concurrent solutions may be found, and Synchronicity automatically ranks according to their performance on a programmer-supplied workload. The project is committed to increasing access to science education for all students, including women, under-represented groups, and first-generation college students. The investigators include students from these groups in this research, at both the undergraduate and graduate level.
This material is based upon work supported by the National Science Foundation under Grants No. 1812951 and 1813133.
Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.