SHF: Small: Symbolic Commutativity Analysis for Multicore Concurrency

点击翻译按钮获取中文摘要

Modern software applications need results to be computed quickly as a matter of practicality, system safety or even security. Unfortunately, CPU speeds themselves are no longer increasing as they used to and hardware companies, instead, offer multicore CPUs. This poses a classical, but notoriously difficult problem: how to divide software programs into multiple interoperating tasks, that can execute concurrently, without stepping on each others' feet. It is well-known that data structure "commutativity" is one route to concurrency. Intuitively, two data-structure operations commute, provided that they can be executed in either order. In this way, commutativity characterizes the independence of program fragments. In recent years, researchers have shown that this can enable concurrency in contexts such as transactional memory, optimistic concurrency, runtime systems and parallelizing compilers. However, it remains an open question as to how to safely extract commutativity information from source code.This project is developing techniques to automatically verify and even synthesize commutativity from source code. Further, this commutativity is employed (integrated with so-called linearizability) in a new parallelizing compiler and transactional object system. These new tools enable programmers to focus on writing correct sequential programs, and yet automatically exploit multicore architectures. The impacts of this work include advances in mathematical foundations, algorithms, symbolic program analysis, compilers and runtime systems. The project also involves engagement with students through multiple tiers of education - ranging from pre-college math students to summer school modules - and outreach aimed at broadening participation of underrepresented groups.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.