SHF: Small: Programming, and Reasoning about, Actors that Share State

Many software applications consist of many components that must compute in parallel and independently of each other and yet must coordinate their activities to achieve the overarching goal. Developers refer to this scenario as concurrent programming, and they consider the creation of concurrent software as one of the most difficult problems around. The investigator and his team are studying a novel solution to this problem. Their approach is to think of concurrent software systems as a collection of conversing actors. Like in real conversations, these actors exchange words and refer back to the context of ideas that a conversation has established so far. The investigator's key insight is to create a special purpose notation for programming these two aspects of conversations explicitly. Preliminary investigations show that this notation greatly facilitates programming concurrent systems and thinking about their coordination efforts. The project will directly impact the evolution of future programming languages and indirectly affect the lives of working programmers. Technically, the project injects two entirely new ideas into the so-called actor model of computation. The first is an explicitly managed space of shared assertions. Using this space, actors can establish a common state, modify it in a controlled manner, and get informed when changes happen. When an actor crashes, its portion of the shared state is automatically withdrawn, making it possible to easily cope with failures and thus making the system resilient. The second idea is a language for programming actor interactions, including message sending and state sharing. While this new language restricts how actors interact and what they interact about, it will enable language designers to provide type systems and model checkers that statically enforce adherence to protocols and verify that the concurrent software system will achieve its specified goals. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.