Rely-guarantee protocols

Filipe Militão, Jonathan Aldrich, Luís Caires

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationECOOP 2014 - Object-Oriented Programming: 28th European Conference, Proceedings
PublisherSpringer-Verlag
Pages334-359
Number of pages26
Volume8586 LNCS
ISBN (Print)9783662442012
DOIs
Publication statusPublished - 2014
Event28th European Conference on Object-Oriented Programming, ECOOP 2014 - Uppsala, Sweden
Duration: 28 Jul 20141 Aug 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8586 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference28th European Conference on Object-Oriented Programming, ECOOP 2014
CountrySweden
CityUppsala
Period28/07/141/08/14

Fingerprint

Dive into the research topics of 'Rely-guarantee protocols'. Together they form a unique fingerprint.

Cite this