A Type System for Borrowing Permissions

Tuesday, February 28^th, 2012 from 12-1 pm in GHC 4303.

Karl Naden, CSD

In imperative object-oriented programming, programmers must consider the impacts of aliasing when reasoning about their programs and proving properties such as consistency of typestate and noninterference of concurrency. Access permission annotations are a lightweight mechanism for reasoning about aliasing in which references are characterized in terms of the access granted to the object and what other aliases to the object might exist. For example, a unique permission grants full access and guarantees no other aliases to the object exist, while an immutable permission grants non-modifying access and guarantees that all other aliases also only have non-modifying access.

In order to be useful in practice, tools based on access permissions must support common programming paradigms such as borrowing, where a unique permission is temporarily made immutable but regained at a later point, and extracting permissions from object fields. Existing tools support borrowing through heavy-weight alias analyses or manual accounting through fractional permissions. Previous systems have modeled field reads as an awkward swap operation. This work proposes local permissions and implicit unpacking of fields as lightweight and natural abstractions for dealing with these problems. In each case, the our type system does all necessary accounting under the hood leaving the exposed language simple.

In this talk, I will motivate the need for tools to reason about aliases, particularly in the context of typestate in the Plaid programming language, and introduce our use of access permissions through a series of examples.

This is joint work with Jonathan Aldrich, Robert Bocchino, and Kevin Bierhoff.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

Spring 2012 Schedule

Tue, Jan 17	GHC 4303	Severin Hacker	Duolingo
Fri, Jan 20	GHC 4303		Expired
Tue, Jan 24	GHC 4303		Expired
Fri, Jan 27	GHC 4303		Expired
Tue, Jan 31	GHC 4303	B. Aditya Prakash	Influence Propagation in Large Graphs
Fri, Feb 3	GHC 4303	Wittawat Tantisiriroj	On the Duality of Data-intensive File System Design: Reconciling HDFS and PVFS
Tue, Feb 7	GHC 4303	Severin Hacker	Duolingo
Fri, Feb 10	GHC 4303		Expired
Tue, Feb 14	GHC 4303		Expired
Fri, Feb 17	GHC 4303		Expired
Tue, Feb 21	GHC 4303		AVAILABLE
Fri, Feb 24	GHC 4303		AVAILABLE
Tue, Feb 28	GHC 4303	Karl Naden	A Type System for Borrowing Permissions
Fri, Mar 2	GHC 4303		AVAILABLE
Tue, Mar 6	GHC 4303		AVAILABLE
Fri, Mar 9	GHC 4303	Midsemester Break	By request only
Tue, Mar 13	GHC 4303	Spring Break	By request only
Fri, Mar 16	GHC 4303	Spring Break	By request only
Tue, Mar 20	GHC 4303		AVAILABLE
Fri, Mar 23	GHC 4303		AVAILABLE
Tue, Mar 27	GHC 4303		AVAILABLE
Fri, Mar 30	GHC 4303	Luke Zarko	TBD
Tue, Apr 3	GHC 4303		AVAILABLE
Fri, Apr 6	GHC 4303		AVAILABLE
Tue, Apr 10	GHC 4303		AVAILABLE
Fri, Apr 13	GHC 4303		AVAILABLE
Tue, Apr 17	GHC 4303		AVAILABLE
Fri, Apr 20	GHC 4303	Spring Carnival	By request only
Tue, Apr 24	GHC 4303		AVAILABLE
Fri, Apr 27	GHC 4303		AVAILABLE
Tue, May 1	GHC 4303		AVAILABLE
Fri, May 4	GHC 4303		AVAILABLE

General Info

The Student Seminar Series is an informal research seminar by and for SCS graduate students from noon to 1 pm on Tuesdays and Fridays. Lunch is provided by the Computer Science Department (personal thanks to Sharon Burks and Debbie Cavlovich!). At each meeting, a different student speaker will give an informal, 40-minute talk about his/her research, followed by questions/suggestions/brainstorming. We try to attract people with a diverse set of interests, and encourage speakers to present at a very general, accessible level.

So why are we doing this and why take part? In the best case scenario, this will lead to some interesting cross-disciplinary work among people in different fields and people may get some new ideas about their research. In the worst case scenario, a few people will practice their public speaking and the rest get together for a free lunch.

Guideline & Speaking Requirement Need-to-Know

Note: Step #1 below are applicable to all SSS speakers. You can schedule AT MOST THREE talks per semester.

SSS is an ideal forum for SCS students to give presentations that count toward fulfilling their speaking requirements. The specifics, though, vary with each department. For instance, students in CSD will need to be familiar with the notes in Section 8 of the Ph.D. document and follow the instructions outlined on the Speakers Club homepage. Roughly speaking, these are the steps:

1. Schedule a talk with SSS by sending your talk title, abstract, additional info (like "Joint work with..." or "In Partial Fulfillment of the Speaking Requirement"), and a picture of yourself (preferably jpeg) to sss@cs at least TWO WEEKS before your scheduled talk.
2. After you are confirmed with your SSS slot, go to the Speakers Club Calendar and schedule your talk at least THREE WEEKS in advance of the talk date.
   
3. On the day of your talk, make sure you print Speakers Club evaluation forms for your evaluators to use.

Students outside of CSD will need to check with their respective departments regarding the procedure. As another example, ISRI students fulfill their speaking requirements by attending a semesterly Software Research Seminar and giving X number of presentations per school year. If you have experience with your department that might help others in your department, please feel free to contribute your knowledge by emailing us. Thank you!

SSS Coordinators

Anthony Gitter, CSD
Kevin Killourhy, CSD