@inproceedings{dinsdale-young2013views,
author = {Dinsdale-Young, Thomas and Birkedal, Lars and Gardner, Philippa and Parkinson, Matthew J. and Yang, Hongseok},
title = {Views: Compositional Reasoning for Concurrent Programs},
booktitle = {Proceedings of POPL},
year = {2013},
month = {January},
abstract = {Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating conjunction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables.
In this paper, we present the “Concurrent Views Framework”, a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Concurrent Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics},
url = {http://approjects.co.za/?big=en-us/research/publication/views-compositional-reasoning-for-concurrent-programs/},
edition = {Proceedings of POPL},
}