TY - GEN
T1 - Rely-guarantee protocols
AU - Militão, Filipe
AU - Aldrich, Jonathan
AU - Caires, Luís
PY - 2014
Y1 - 2014
N2 - The use of shared mutable state, commonly seen in object-oriented systems, is often problematic due to the potential conflicting interactions between aliases to the same state. We present a substructural type system outfitted with a novel lightweight interference control mechanism, rely-guarantee protocols, that enables controlled aliasing of shared resources. By assigning each alias separate roles, encoded in a novel protocol abstraction in the spirit of rely-guarantee reasoning, our type system ensures that challenging uses of shared state will never interfere in an unsafe fashion. In particular, rely-guarantee protocols ensure that each alias will never observe an unexpected value, or type, when inspecting shared memory regardless of how the changes to that shared state (originating from potentially unknown program contexts) are interleaved at run-time.
AB - The use of shared mutable state, commonly seen in object-oriented systems, is often problematic due to the potential conflicting interactions between aliases to the same state. We present a substructural type system outfitted with a novel lightweight interference control mechanism, rely-guarantee protocols, that enables controlled aliasing of shared resources. By assigning each alias separate roles, encoded in a novel protocol abstraction in the spirit of rely-guarantee reasoning, our type system ensures that challenging uses of shared state will never interfere in an unsafe fashion. In particular, rely-guarantee protocols ensure that each alias will never observe an unexpected value, or type, when inspecting shared memory regardless of how the changes to that shared state (originating from potentially unknown program contexts) are interleaved at run-time.
UR - http://www.scopus.com/inward/record.url?scp=84905408019&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-44202-9_14
DO - 10.1007/978-3-662-44202-9_14
M3 - Conference contribution
AN - SCOPUS:84905408019
SN - 9783662442012
VL - 8586 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 334
EP - 359
BT - ECOOP 2014 - Object-Oriented Programming: 28th European Conference, Proceedings
PB - Springer Verlag
T2 - 28th European Conference on Object-Oriented Programming, ECOOP 2014
Y2 - 28 July 2014 through 1 August 2014
ER -