Panini: A Concurrent Programming Model for Solving Pervasive & Oblivious Interference

Modular reasoning about concurrent programs is complicated by the pervasiveness of interferences that do not give out any information about the behaviors of potentially interfering concurrent tasks, at the interference points. Reasoning about a concurrent program would be easier if a programmer, modularly and statically: (1) knows precisely the program points at which the interference may happen, and (2) has some insights into the behaviors of other potentially concurrent tasks at these points. In this work, we present a core concurrent calculus with these properties and their proofs. Using our calculus a programmer can design and implement concurrent modules of their software using capsules and modularly reason about properties of these concurrent modules using static types referred to in their code, and then automatically have these properties hold in the larger concurrent system formed by composing these capsules. We also illustrate how this concurrent calculus can be used in conjunction with standard Hoare style reasoning to modularly verify concurrent programs with interference