DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

SEXC: Static EXtended Checking for Cyclone

Greg Morrisett,
Harvard University, USA

Friday, May 19th, 13:00-14:00(!)
IT University of Copenhagen, Rued Langgaards Vej 7, Auditorium 4

Abstract:

Cyclone is a type-safe dialect of C intended for systems programmers building low-level code such as device drivers, kernels, protocols, etc. where security and reliability are of greatest concern. The Cyclone type system ensures that programs will not end up with a corrupted memory, but of course, programs can still effectively crash with an uncaught exception due to division by zero, array index out of bounds, NULL pointer dereference, or more generally, failure to satisfy a pre-condition for some routine.

The goal of the SEXC project is to extend Cyclone with a program logic and semi-automatic tools for eliminating these potential failures. Today, with minimal user input, we are able to safely eliminate about 90% of the array bounds checks and null pointer checks, and do so with an analysis that takes about the same amount of time as a conventional type-checker.

I will discuss the engineering issues that arose in the current implementation, and the challenges we see in getting rid of the last 10% of the checks. I will also discuss the challenges we face in extending the system beyond the limited class of failures that we address today.

This is joint work with Yanling Wang and Aleks Nanevski.

Scientific host: Lars Birkedal. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org