Checking Concurrent Typestate with Access Permissions in Plural: A Retrospective

Abstract

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 pro-tocol. 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.