Views: Compositional Reasoning for Concurrent Programs
The authors present a framework for reasoning compositionally about concurrent programs. At its core is the notion of a view: an abstraction of the state that takes account of the possible interference due to other threads. Threads' views are composable, and an update to the state by one thread must preserve the views of other threads. They prove soundness for their framework, and demonstrate its utility by studying examples. In particular, they show that several variants of concurrent separation logic, type systems, and concurrent abstract predicates can all be seen as instantiations of their framework. Soundness for particular instantiations simply follows from the soundness of their framework.