file.pdf (153.48 kB)
0/0

Checking Concurrent Typestate with Access Permissions in Plural: A Retrospective

Download (153.48 kB)
journal contribution
posted on 01.07.2014 by Kevin Bierhoff, Nels E. Beckman, Jonathan Aldrich

Objects often define usage protocols that clients must follow in order for these objects to work properly. In the presence of aliasing, however, it is difficult to check whether all the aliases of an object properly coordinate to enforce the protocol. Plural is a type-based system that can soundly enforce challenging protocols even in concurrent programs. In this paper, we discuss how Plural supports natural idioms for reasoning about programs, leveraging access permissions that express the programmer’s design intent within the code. We trace the predecessors of the design intent idioms used in Plural, discuss how we have found different forms of design intent to be complimentary, and outline remaining challenges and directions for future work in the area.

History

Publisher Statement

© ACM, 2014. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published at http://doi.acm.org/10.1145/2601097.2601105

Date

01/07/2014

Exports

Exports