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

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

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.