Computer Science Department
School of Computer Science, Carnegie Mellon University


Rely-Guarantee Protocols for Safe Interference over Shared Memory

Filipe David Oliveira Militão

December 2015

Ph.D. Thesis


Keywords: Programming languages, interference control, linearity, typestates, rely-guarantee protocols, concurrency, shared mutable state

Mutable state can be useful in certain algorithms, to structure programs, or for efficiency purposes. However, when shared mutable state is used in non-local or nonobvious ways, the interactions that can occur via aliases to that shared memory can be a source of program errors. Undisciplined uses of shared state may unsafely interfere with local reasoning as other aliases may interleave their changes to the shared state in unexpected ways. We propose a novel technique, rely-guarantee protocols, that structures the interactions between aliases and ensures that only safe interference is possible.

We present a linear type system outfitted with our novel sharing mechanism that enables controlled interference over shared mutable resources. Each alias is assigned separate, local roles encoded in a protocol abstraction that constrains how an alias can legally use that shared state. By following the spirit of rely-guarantee reasoning, our rely-guarantee protocols ensure that only safe interference can occur but still allow many interesting uses of shared state, such as going beyond invariant and monotonic usages.

This thesis describes the three core mechanisms that enable our type-based technique to work: 1) we show how a protocol models an alias's perspective on how the shared state evolves and constrains that alias’s interactions with the shared state; 2) we show how protocols can be used while enforcing the agreed interference contract; and finally, 3) we show how to check that all local protocols to some shared state can be safely composed to ensure globally safe interference over that shared memory. The interference caused by shared state is rooted at how the uses of different aliases to that state may be interleaved (perhaps even in non-deterministic ways) at run-time. Therefore, our technique is mostly agnostic as to whether this interference was the result of alias interleaving caused by sequential or concurrent semantics. We show implementations of our technique in both settings, and highlight their differences. Because sharing is "first-class" (and not tied to a module), we show a polymorphic procedure that enables abstract compositions of protocols. Thus, protocols can be specialized or extended without requiring specific knowledge of the interference produce by other protocols to that state. We show that protocol composition can ensure safety even when considering abstracted protocols. We show that this core composition mechanism is sound, decidable (without the need for manual intervention), and provide an algorithm implementation.

236 pages

Thesis Committee:
Jonathan Aldrich (Chair)
Frank Pfenning
Karl Crary
Neelakantan Krishnaswami (University of Birmingham)
Luís Caires (Chair, Univeridade Nova de Lisboa, Portugal)
António Ravara (Univeridade Nova de Lisboa, Portugal)
Vasco Vasconcelos (Universidade de Lisboa, Portugal)

Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by