TC:Small: Formal Reasoning about Concurrent Programs for Multicore and Multiprocessor Machines

关于并发程序的形式化推理通常是在高层完成的，具有很强的假设，例如内置的线程原语(例如锁)和简化的内存模型(例如顺序一致性)。现有的形式化技术(包括Hoare逻辑和类型系统)一直忽略了一些重要问题，如松弛的内存模型、硬件中断、同步原语的实现以及对软件事务内存和私有化的支持。这严重限制了它们的适用性。本研究的重点是扩展和改造现有的形式化技术，使其能够支持运行在现代多核和多处理器机器上的现实低级别并发程序。PI正在开发一种新的操作方法，用于推理在宽松内存模型下运行的程序；设计新的程序逻辑，用于证明弱内存操作和强内存操作(包括内存围栏和比较并交换指令)；并展示如何将他的方法扩展到现实线程实现和具有宽松内存模型的机器。如果成功，这项研究将有助于提高并发软件组件的可靠性，这些组件构成了世界上许多关键系统的支柱。它还将促进全社区的努力，为安全和可扩展的多核计算寻找新的编程模型。

Formal reasoning about concurrent programs is usually done at ahigh-level with strong assumptions such as built-in thread primitives(e.g., locks) and simplified memory models (e.g., sequentialconsistency). Existing formal techniques (including Hoare logic andtype system) have consistently ignored important issues such asrelaxed memory models, hardware interrupts, implementation ofsynchronization primitives, and support for software transactionalmemory and privatization. This severely limits their applicability.This research focuses on extending and adapting existing formaltechniques so that they can also support realistic low-levelconcurrent programs running on modern multicore and multiprocessormachines. The PI is developing a new operational approach forreasoning about programs running under relaxed memory models;designing new program logics for certifying both weak and strongmemory operations (including the memory-fence and compare-and-swapinstructions); and showing how to scale his approach to real-worldthread implementation and to machines with relaxed memory models. Ifsuccessful, this research will help improve the reliability ofconcurrent software components, which form the backbone of manycritical systems in the world. It will also facilitate thecommunity-wide effort for finding new programming models for safe andscalable multicore computing.