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

TC：小：关于多核和多处理器机器并发程序的形式推理

• 批准号: 0915888
• 负责人: Zhong Shao
• 金额: $ 50万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-09-01 至 2014-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0915888&HistoricalAwards=false
• 关键词: TC; Small; Formal; Reasoning; about

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.

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