NJPLS

Friday, 7 March 2008

Agenda

Arrival and Coffee: 9:30 - 10:00

Session 1: 10:00 - 10:45

Break: 10:45 - 11:00

Session 2: 11:00 - 12:30

Lunch: 12:30 - 1:50

Business meeting: 1:50 - 2:00

Session 3: 2:00 - 3:30

Abstracts

Title: Coqa: Concurrent Objects with Quantized Atomicity
Yu David Liu, Xiaoqi Lu and Scott Smith.

This talk introduces a new language model, Coqa, for deeply embedding concurrent programming into objects. Every program written in our language has the desirable behaviors of atomicity, mutual exclusion, and race freedom automatically built in. A key property of our model is the notion of *quantized atomicity*: every concurrent program execution can be viewed as being divided into quantum regions of atomic execution, greatly reducing the number of interleavings to consider. Rather than building atomicity locally, i.e. declaring some code blocks as atomic blocks and leaving other code segments with no guarantee of any atomicity property, we build it in globally, so that a form of atomicity, quantized atomicity, ubiquitously exists at all program points. We justify our approach both from a theoretical basis by showing that a formal representation has provable quantized atomicity properties, and by implementing CoqaJava, a Java extension incorporating all of the Coqa features.

Fable: A Language for Enforcing User-defined Security Policies
Nikhil Swamy, Brian J. Corcoran and Michael Hicks

This paper presents Fable, a core formalism for a programming language in which programmers may specify security policies and reason that these policies are properly enforced. In Fable, security policies can be expressed by associating security labels with the data or actions they protect. Programmers define the semantics of labels in a separate part of the program called the enforcement policy. Fable prevents a policy from being circumvented by al- lowing labeled terms to be manipulated only within the enforcement policy; application code must treat labeled values abstractly. Together, these features facilitate straightforward proofs that programs implementing a particular policy achieve their high-level security goals. Fable is flexible enough to implement a wide variety of security policies, including access control, information flow, provenance, and security automata. We have implemented Fable as part of the Links web programming language; we call the resulting language SELinks. We report on our experience using SELinks to build two substantial applications, a wiki and an on-line store, equipped with a combination of access control and provenance policies. To our knowledge, no existing framework enables the enforcement of such a wide variety of security policies with an equally high level of assurance.

J&s: Toward Flexible and Efficient Family Extensibility
Xin Qi and Andrew Myers

Object-oriented languages aim to support software extensibility and reuse with the mechanisms of subtyping and inheritance, but ordinary inheritance is limited in at least two important ways. First, a group of interacting classes cannot be extended at the same time while preserving their relationships, and second, new functionality cannot be added to the objects of an existing class without modifying the class.

This talk introduces J&s, a language that simultaneously addresses these two limitations on extensibility. In J&s, as in its predecessors Jx and J&, families can be extended and composed; moreover, classes in different families can be shared: an object that is an instance of one class can be used as an instance of a class it shares with, each class becoming a "view" of the object. Objects can safely move between families by changing their views.

Given such a feature-rich language, it remains a practical problem how to implement it efficiently. This talk also presents our latest effort on a scalable and efficient implementation of the language, based on the Java classloader. It generates a small amount of code that has a low overhead.

HardBound: Architectural Support for Spatial Safety of the C Programming Language
Joe Devietti, Colin Blundell, Milo M. K. Martin, and Steve Zdancewic

The C programming language is at least as well known for its absence of spatial memory safety guarantees (i.e., lack of bounds checking) as it is for its high performance. C's unchecked pointer arithmetic and array indexing allow simple programming mistakes to lead to erroneous executions, silent data corruption, and security vulnerabilities. Many prior proposals have tackled enforcing spatial safety in C programs by checking pointer and array accesses. However, existing software-only proposals have significant drawbacks that may prevent wide adoption, including: unacceptably high runtime overheads, lack of completeness, incompatible pointer representations, or need for non-trivial changes to existing C source code and compiler infrastructure.

Inspired by the promise of these software-only approaches, this paper proposes a hardware bounded pointer architectural primitive that supports cooperative hardware/software enforcement of spatial memory safety for C programs. This bounded pointer is a new hardware primitive datatype for pointers that leaves the standard C pointer representation intact, but augments it with bounds information maintained separately and invisibly by the hardware. The bounds are initialized by the software, and they are then propagated and enforced transparently by the hardware, which automatically checks a pointer's bounds before it is dereferenced. One mode of use requires instrumenting only malloc, which enables enforcement of per-allocation spatial safety for heap-allocated objects for existing binaries. When combined with simple intra-procedural compiler instrumentation, hardware bounded pointers enable a low-overhead approach for enforcing complete spatial memory safety in unmodified C programs.

Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
Chung-chieh Shan, Jacques Carette and Oleg Kiselyov

This "functional necklace" aims to change how you try to write your next interpreter: by deforesting the object language, to exhibit more static safety in a simpler type system. We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value CPS transformers.

Our main idea is to encode abstract syntax using cogen functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the lambda-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck.

Steve Zdancewic put together the schedule.