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

关于并发程序的形式化推理通常是在高层次上进行的，带有强假设，如内置的线程原语（例如，锁）和简化的存储器模型（例如，sequentialconsistency）。现有的形式化技术（包括Hoare逻辑和类型系统）一直忽视了一些重要的问题，如宽松的内存模型、硬件中断、同步原语的实现以及对软件事务内存和私有化的支持。这严重限制了它们的适用性，本研究的重点是扩展和调整现有的formaltechniques，使它们也可以支持现实的低层次并发程序运行在现代多核和多处理器机器上。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.