Publications

BibTex format

@inproceedings{Dinsdale-Young:2013:10.1145/2429069.2429104,
author = {Dinsdale-Young, T and Birkedal, L and Gardner, P and Parkinson, M and Yang, H},
doi = {10.1145/2429069.2429104},
pages = {287--300},
publisher = {ACM},
title = {Views: compositional reasoning for concurrent programs},
url = {http://dx.doi.org/10.1145/2429069.2429104},
year = {2013}
}

Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Dinsdale-Young,T
AU  - Birkedal,L
AU  - Gardner,P
AU  - Parkinson,M
AU  - Yang,H
DO  - 10.1145/2429069.2429104
EP  - 300
PB  - ACM
PY  - 2013///
SP  - 287
TI  - Views: compositional reasoning for concurrent programs
UR  - http://dx.doi.org/10.1145/2429069.2429104
UR  - http://hdl.handle.net/10044/1/33224
ER  -

Download

ProfessorPhilippaGardner

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)