SHF: Small: Collaborative Research: Static and Dynamic Analysis for Cooperative Concurrency

SHF：小型：协作研究：协作并发的静态和动态分析

基本信息

批准号：
1116883
负责人：
Cormac Flanagan
金额：
$ 35.95万
依托单位：
University of California-Santa Cruz
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2011
资助国家：
美国
起止时间：
2011-07-01 至 2015-06-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1116883&HistoricalAwards=false
关键词：
SHF Small Collaborative Research Static

项目摘要

The widespread adoption of multicore processors requires multithreadedsoftware to exploit these hardware resources. Unfortunately, theconstruction and validation of reliable concurrent software currentlyrequires extraordinary effort, due to unanticipated interactionsbetween concurrent threads. Thus, developing better programmingtechniques and tools for concurrent programming is essential. Thisresearch develops a cooperative programming methodology formultithreaded software, based on the philosophy that all threadinterference must be explicitly documented via source-level "yield"annotations by the programmer.The project will investigate both static and dynamic checkingtechniques to verify the correctness of yield annotations. Onceverified, these annotations guarantee that code executed betweensuccessive yields is serializable and thus amenable to sequentialreasoning. Moreover, yield-free code is deterministic. Despiteprovided these strong safety guarantees, this methodology does notimpact program performance. The cooperative methodology provides arobust foundation for multithreaded software and can potentiallytransform the principles and practices of multithreaded softwareengineering. This work on cooperability will also provide researchopportunities for graduate and undergraduate students, and it willsupport endeavors to provide access to science education for allstudents.

多核处理器的广泛采用需要多线程软件来利用这些硬件资源。不幸的是，由于并发线程之间存在意外的交互，目前可靠的并发软件的构建和验证需要付出巨大的努力。因此，开发更好的并发编程技术和工具至关重要。这项研究开发了一种用于多线程软件的协作编程方法，其理念是所有线程干扰必须由程序员通过源代码级“yield”注释明确记录。该项目将研究静态和动态检查技术，以验证yield注释的正确性。一旦经过验证，这些注释保证在连续的生成之间执行的代码是可序列化的，因此适合顺序推理。此外，无收益代码是确定性的。尽管提供了这些强有力的安全保证，但这种方法不会影响程序性能。协作方法为多线程软件提供了坚实的基础，并且有可能改变多线程软件工程的原理和实践。这项合作性工作还将为研究生和本科生提供研究机会，并将支持为所有学生提供科学教育机会的努力。