 |
|
|
Computer Science >
Programming Languages and Software Engineering
> Conferences > 2002 Programming
Languages Day at Watson
|
|
| 2002 Programming Languages Day at Watson | |
|
The third annual Programming Languages Day will be held at the IBM Thomas J. Watson Research Center on Tuesday, May 7, 2002. The day will be held in cooperation with the New Jersey and New England Programming Languages and Systems Seminars. The main goal of the event is to increase awareness of each other's work, and to encourage interaction and collaboration. Location and Directions The Programming
Languages day will be held at room H0-F15 in the Hawthorne1 building
at 19, Skyline Drive, Hawthorne, New York 10532. Please follow directions at the site to visitor's entrance/ reception, which is on the BACK SIDE of the building. From the reception area, follow directions to room GN-F15. (You will be reaching Skyline drive via Rt. 9A. Both ends of Skyline drive meet Rt. 9A. If you come in via the south end of Skyline drive, IBM Research is the first building on the right. Move to the left lane, as the right lane leads to the employee's entrance (the first entrance). Take the next entrance (the second entrance) to reception. After you go through the gate, go to the parking lot on the right side.) Registration If you
plan to attend the Programming Languages Day, please register by
sending an e-mail with your name, affiliation, and contact information
to grama@us.ibm.com so that
we can plan for lunch and refreshments to be available. Program Committee Kathleen
Fisher,
AT&T Research Agenda Attendees
are welcome from 9:30 onwards and are encouraged to use this opportunity
to Session
1: 10:30 - 12:05 Session
2: 1:30 - 3:15 Perry
Cheng, IBM Research: Scott
Stoller, SUNY Stonybrook: Session 3: 3:45 - 5:00 Dan
Grossman, Cornell University: Nadeem
Abdul Hamid, Yale University: Abstracts: Next
Generation Software Systems and Programming Language Research 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 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 An
Analyzable Annotation Language 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 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 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. Domain
Partitioning for Open Reactive Systems 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 a most general environment of the system, i.e., one that exercises all possible behaviors of the system. The partition also helps the generated environment avoid exercising the same behavior multiple times. Many distributed systems with security requirements can be regarded as open reactive systems whose environment is an adversary-controlled network. We illustrate our 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 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 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.
Previous Events
|
|
|
|
|
