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

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

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.