FacebookTwitterGoogle PlusRSS News Feed

Computer Science Thesis Proposal

Thesis Proposals
Ph.D. Student
Computer Science Department
Carnegie Mellon University
Rely-Guarantee Protocols
Thursday, July 24, 2014 - 10:00am to 12:00pm
7101 
Gates&Hillman Centers
Abstract:

The use of shared mutable state, commonly seen in object-oriented systems and in imperative languages, is often problematic due to the potential conflicting interactions between aliases to the same state. This thesis proposes 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.

Thesis Committee:
Jonathan Aldrich (Co-Chair)
Luís Caires (Co-Chair)
Frank Pfenning
Karl Crary
António Ravara (Universidade Nova de Lisboa)

Thesis Summary

Keywords:
For More Information, Please Contact:

deb [atsymbol] cs ~replace-with-a-dot~ cmu ~replace-with-a-dot~ edu