SHF: Small: Design and Inference of Choreography Types to Reduce Concurrency Programming Errors

SHF：小型：编排类型的设计和推理以减少并发编程错误

• 批准号: 1617401
• 负责人: Gul Agha
• 金额: $ 50万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-06-01 至 2020-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1617401&HistoricalAwards=false
• 关键词: SHF; Small; Design; Inference; Choreography

With the growth of the web, cloud computing, sensor networks andmulticore programming, concurrency has become critical to softwareapplications in the real world. Because the Actor model of concurrentcomputation provides scalable concurrency, commercial software isoften written using the Actor model. Many concurrency related errorssuch as unprocessable messages, deadlocks, and livelocks result from amismatch of component actors in a system. The research developschoreography types as a method to understand concurrency structuresand detect concurrency related bugs. The intuition behind theresearch is that combining symbolic execution with information fromconcrete traces obtained during unit testing can provide a way toinfer and approximate choreography types. The research would make concurrent and distributed programmingsafer--increasing trust in applications such as cloud computing onwhich a large part of the US economy is dependent today. Much as datatypes help programmers think about the interfaces of components in asequential program, the research would provide ways in whichprogrammers can think about the structure of parallel programs interms of choreographing actors with evolving type structure. Theeducational impact of the research is to facilitate teaching scalableparallel programming, creating tools that expose and facilitate theunderstanding of the structure of concurrent programs.

随着网络、云计算、传感器网络和多核编程的发展，并发性已经成为真实的世界中软件应用的关键。 由于并发计算的Actor模型提供了可伸缩的并发性，商业软件通常使用Actor模型编写。 许多与并发相关的错误，如不可处理的消息、死锁和活锁，都是由于系统中组件参与者的不匹配造成的。 研究开发了一种理解并发结构和检测并发相关错误的方法。 研究背后的直觉是，将符号执行与单元测试期间获得的具体跟踪信息相结合，可以提供一种推断和近似编排类型的方法。这项研究将使并发和分布式编程更安全-增加对云计算等应用程序的信任，而今天美国经济的很大一部分依赖于云计算。 就像数据库帮助程序员考虑顺序程序中组件的接口一样，这项研究将提供程序员可以考虑并行程序结构的方法，即用不断发展的类型结构编排演员。 该研究的教育影响是促进可扩展并行编程的教学，创建暴露和促进并发程序结构理解的工具。