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

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

With the growth of the web, cloud computing, sensor networks and multicore programming, concurrency has become critical to software applications in the real world. Because the Actor model of concurrent computation provides scalable concurrency, commercial software is often written using the Actor model. Many concurrency related errors such as unprocessable messages, deadlocks, and livelocks result from a mismatch of component actors in a system. The research develops choreography types as a method to understand concurrency structures and detect concurrency related bugs. The intuition behind the research is that combining symbolic execution with information from concrete traces obtained during unit testing can provide a way to infer and approximate choreography types. The research would make concurrent and distributed programming safer--increasing trust in applications such as cloud computing on which a large part of the US economy is dependent today. Much as data types help programmers think about the interfaces of components in a sequential program, the research would provide ways in which programmers can think about the structure of parallel programs in terms of choreographing actors with evolving type structure. The educational impact of the research is to facilitate teaching scalable parallel programming, creating tools that expose and facilitate the understanding of the structure of concurrent programs.