Reasoning about actors that share state
Abstract
Concurrent programming is notoriously difficult. That challenge has prompted researchers to investigate approaches to organizing and understanding concurrent behavior. The recent dataspace model of actors is one such example of an organization methodology. It recognizes the benefit of isolation between components but also the need for sharing. My dissertation tackles the other aspect---understanding concurrency---by exploring the potential of reasoning about dataspace programs using types. The first challenge is integrating dataspace programming to a typed setting. Doing so allows for checking that each actor agrees on the types of communicated values. In initial work, I designed a type system that incorporates an approximation of the dataspace communication mechanism to ensure this structural agreement. The rest of the dissertation concerns the question of reasoning about the communication behavior of program components. By utilizing a structured notation for programming such actors, I show that it is possible to automatically check behavioral properties of programs.--Author's abstract