Cooperative decoupled processes

Event-driven programming has become a major paradigm in developing concurrent, distributed systems. Its benefits are often informally captured by the key tenet of “decoupling,” a notion which roughly captures the ability of processes to join and leave (or fail) applications dynamically, and to be developed by independent parties. Programming models for event-driven programming either make it hard to globally reason about control flow, thus hampering sound execution, or sacrifice decoupling to aid in reasoning about control flow. This work fills the gap by introducing a programming model—dubbed cooperative decoupled processes—that achieves both decoupling and global reasoning about control flow. We introduce this programming model through an event calculus, loosely inspired by the Join calculus, that enables reasoning about cooperative decoupled processes through the concepts of pre- and postconditions. A linear type system controls aliasing of events to avoid a break of control flow and thus safe exchange of shared events. Fundamental properties of the type system such as subject reduction, migration safety, and progress are established.