Accession Number:

ADA605817

Title:

Rely-Guarantee Protocols

Descriptive Note:

Technical rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Report Date:

2014-05-01

Pagination or Media Count:

152.0

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.

Subject Categories:

  • Operations Research
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE