[Pl-seminar] IBM Watson PL Day schedule

[Shriram Krishnamurthi]

Attendees are welcome from 9:30 onwards and are encouraged to use this
opportunity to meet other researchers.

Session 1: 10:30 - 12:05
        (Keynote presentation)
        Matthias Felleisen, Northeastern University:
        Next Generation Software Systems and Programming Language Research

        Dominic Duggan, Stevens Institute of Technology:
        Cryptographic Types

Session 2: 1:30 - 3:15
        Darko Marinov, MIT:
        An Analyzable Annotation Language

        Perry Cheng, IBM Research:
        A Defragmenting, Mostly Non-moving Garbage Collector

        Scott Stoller, SUNY Stonybrook:
        Generation of Environments for Distributed Systems

Session 3: 3:45 - 5:00

        Dan Grossman, Cornell University:
        Cyclone: A Safe Language at the C Level of Abstraction

        Nadeem Abdul Hamid, Yale University:
        A Syntactic Approach to Foundation Proof-Carrying Code

=============================================================
Talk Abstracts:

Next Generation Software Systems and Programming Language Research
Matthias Felleisen, Northeastern University:

Future software systems will consist of reusable components. They will also
provide interfaces for third-party programmers to extend the systems
statically as well as dynamically. A Web browser, for example, allows users
to add plug-ins and applets. Similarly, mail clients can execute attached
"macro" programs, and users can specify mime-type specific application
tools.

Programming language research must support this emergent form of system
design because it poses new problems for programmers and systems
architects. Researchers will have to study a wide range of problems,
including the design of constructs for the implementation and composition
of components; the development of mechanism for monitoring and enforcing
invariants across components; the development of run-time systems in
support of dynamic extensibility; and the evolution of new programming
paradigms. Programming environments that assist with the analysis and
synthesis of componential and extensible software will be an additional
focus of programming language research.

In my talk, I will first present the basic problems with a concrete
example: the design and implementation of a Web server for fast and
convenient dynamic content generation. Based on this example, I will
provide an overview of my team's recent and future research efforts on
programming language support for building such extensible systems: language
support for reusable components; the design and implementation of
extensible abstract data types; the administration of resources; and the
specification and enforcement of behavioral contracts for components.

=============================================================
Cryptographic Types
Dominic Duggan  Stevens Institute of Technology

Networks secured by cryptographic techniques can be likened to programming
languages where all type-checking is performed at run-time: cryptographic
operations such as signature checking and decryption are analogous to
run-time dynamic type-checking.  Languages such as Java allow a combination
of static and dynamic type-checking in distributed programming.
Cryptographic types are a way to express cryptographic guarantees (of
secrecy and integrity) in a type system for a network programming language.
This allows some of these guarantees to be checked statically, before a
network program executes.  Where dynamic checks are required, these are
represented at the source language level as dynamic checking, and are
translated by the compiler to lower level cryptographic operations for
encryption/decryption and signing/authentication.  Static checking avoids
the unnecessary overhead of run-time cryptographic operations where
communication is through a trusted medium (e.g. the OS kernel, or a trusted
subnet), and also provides static guarantees of the reliability of a
network application.  Cryptographic types can also be used to build
application-specific security protocols, where
type-checking in the lower layers of the protocol stack verifies security
properties for upper layers.  Cryptographic types are described formally
using a process calculus, the ec-calculus, allowing the correctness to be
verified for a scheme for compiling type operations to cryptographic
operations.

=============================================================
An Analyzable Annotation Language
Sarfraz Khurshid, Darko Marinov, and Daniel Jackson
LCS, MIT

The Alloy Annotation Language (AAL) is a language for annotating Java code
based on the Alloy modeling language.  It offers a syntax similar to the
Java Modeling Language (JML), and the same opportunities for generation of
run-time assertions.  In addition, however, AAL offers the possibility of
fully automatic compile-time analysis.  Several
kinds of analyses are supported, including: checking the code of a method
against its specification; checking that the specification of a method in a
subclass is compatible with the specification in the superclass; and
checking properties relating method calls on different objects, such as
that the equals methods of a class (and its overridings) induce an
equivalence.  Using partial models in place of code, it is also possible to
analyze object-oriented designs in the
abstract: investigating, for example, a view relationship amongst objects.

The paper gives examples of annotations and such analyses.  It presents
(informally) a systematic translation of annotations into Alloy, a simple
first-order logic with relational operators.  By doing so, it makes Alloy's
automatic analysis, which is based on state-of-the-art SAT solvers,
applicable to the analysis of object-oriented programs, and demonstrates
the power of a simple logic as the basis for an annotation language.
=============================================================
A Defragmenting, Mostly Non-moving Garbage Collector
David Bacon, Perry Cheng
IBM Research

Our goal is to design a real-time garbage collector for Java targeted for
uniprocessor embedded systems.  The most basic choice in designing a
collector is choosing whether it will be copying or non-copying. While
previous work has demonstrated the feasibility of developing real-time
copying collectors, the factor of two in space overhead inherent in copying
collectors makes this choice unattractive for embedded systems.  On the
other hand, mark-sweep collectors do not have to pay the doubled space
cost.  Instead, they are subject to fragmentation which effectively
increases memory consumption.

To achieve the goal of real-time collection with good bounded memory usage,
we designed our collector to be a mostly non-moving collector with
on-demand incremental defragmentation.  We present initial results for a
stop-the-world prototype to show the feasibility of the design.  Our
experiments show that a Brooks-style read barrier can be implemented in an
optimizing compiler with under 5% overhead on the SPECjvm98 benchmarks.

We implemented our defragmenting collector in a segregated free-list
allocator and showed that the SPECjvm98 benchmarks can be run with no more
than 10% over the theoretical minimum heap size.  For the SPECjvm98
benchmarks, we found the conventional wisdom that programs only allocate
objects from a small set of sizes is false.  We explore the implications of
this property on both segregated free-list and defragmenting systems.


=============================================================
Generation of Environments for Distributed Systems
Scott Stoller, SUNY Stonybrook

Testing or model-checking an open reactive system often requires generating
a model of the environment.  We describe a static analysis for Java that
computes a partition of a system's inputs: inputs in the same equivalence
class lead to identical behavior.  The partition provides a basis for
generation of code for the system's most general environment, i.e., one
that efficiently exercises all possible behaviors of the system.  Many
distributed systems with security requirements can be regarded as open
reactive systems whose environment is an adversary-controlled network.  We
illustrate the approach by applying it to a fault-tolerant and
intrusion-tolerant distributed voting system and model-checking the system
together with the generated environment.

=============================================================
Cyclone: A Safe Language at the C Level of Abstraction
Dan Grossman, Cornell University

Memory safety and type safety are invaluable features for constructing
reliable software and enforcing abstractions such as abstract data types
and access controls.  However, most safe safe languages are at a high level
of abstraction; programmers cede almost all control over data
representation and memory management.  For this (and other) reasons, C
remains the de facto standard for writing systems software or extending
legacy systems already written in C.

The Cyclone project aims to bring safety to C-style programming without
sacrificing the programmer control necessary for low-level software.  Of
course, this task involves difficult trade-offs among performance, language
expressiveness, and programmer convenience.  This talk will highlight
Cyclone's design principles with an emphasis on how its advanced type
system captures important C idioms while remaining usable by C programmers.
Examples will give the flavor of Cyclone programming and give a sense of
how the language "all fits together".

Cyclone is joint work with Trevor Jim (AT&T Research), Greg Morrisett,
Michael Hicks, James Cheney, and Yanling Wang (Cornell University)

=============================================================

A Syntactic Approach to Foundation Proof-Carrying Code
Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and
Zhaozhong Ni
Yale University

Proof-Carrying Code (PCC) is a general framework for verifying the safety
properties of machine-language programs. PCC proofs are usually written in
a logic extended with language-specific typing rules; they certify safety
but only if there is no bug in the typing rules. Foundational
Proof-Carrying Code (FPCC), on the other hand, constructs and verifies its
proofs using strictly the foundations of mathematical logic, with no
type-specific axioms. FPCC is more flexible and secure because it is not
tied to any particular type system and it has a smaller trusted base.

Foundational proofs, however, are much harder to construct. Previous
efforts on FPCC all required building sophisticated semantic models for
types. Furthermore, none of them can be easily extended to support mutable
fields and higher-order polymorphism.

In this talk, we present a syntactic approach to FPCC that avoids all of
these difficulties. Under our new scheme, the foundational proof for a
typed machine program simply consists of the typing derivation plus the
syntactic soundness proof for the underlying type system. The former can be
readily obtained from a type-checker while the latter is known to be much
easier to construct than the semantic soundness proofs. We present a
comprehensive translation from a typed assembly language into FPCC,
demonstrate the advantages of our new system, and describe an
implementation in the Coq proof assistant.