Computer Science Thesis Oral

Tuesday, December 15, 2015 - 9:30am


Traffic 21 Classroom 6501 Gates & Hillman Centers



For More Information, Contact:

Mutable state can be useful in certain algorithms, to structure programs, or for efficiency purposes. However, the interactions that can occur via aliased mutable state can be a source of program errors. Undisciplined uses of shared state may unsafely interfere with local reasoning as other aliases can interleave their changes to the shared state in unexpected ways. We propose a new technique, rely-guarantee protocols, that structures these interactions to ensure that only safe interference is possible. We present a linear type system outfitted with our novel sharing mechanism to enable controlled interference over shared resources. Each alias is assigned separate, local roles encoded in a protocol abstraction that constrains how an alias can use the shared resources. We describe the main mechanisms of our technique: 1) how a protocol models an alias’s perspective on the evolution of the shared resources; 2) how protocols can be used while enforcing the agreed interference contract; and finally, 3) 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 indifferent 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. 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, and provide an algorithm implementation. Thesis Committee: Jonathan Aldrich (Co-Chair) Luis Caires (Co-Chair, New University of Lisbon)Frank Pfenning Karl Crary Neelakantan Krishnaswami (University of Birmingham) António Ravara (New University of Lisbon) Vasco Vasconcelos (University of Lisbon)


Thesis Oral