New England Programming Languages and Systems Symposium Series (NEPLS): Abstracts

N
E
P
L
S
These abstracts are for talks at this event.
NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source.
Compiling Cryptographic Protocols for Deployment on the Web

Jay McCarthy (Brown), Joshua Guttman (MITRE), John Ramsdell (MITRE), Shriram Krishnamurthi (Brown)
Cryptographic protocols are useful for trust engineering in Web transactions. The Cryptographic Protocol Programming Language (CPPL) provides a model wherein trust management annotations are attached to protocol actions, and are used to constrain the behavior of a protocol participant to be compatible with its own trust policy. The first implementation of CPPL generated stand-alone, single-session servers, making it unsuitable for deploying protocols on the Web. We describe a new compiler that uses a constraint-based analysis to produce multi-session server programs. The resulting programs run without persistent TCP connections for deployment on traditional Web servers. Most importantly, the compiler preserves existing proofs about the protocols. We present an enhanced version of the CPPL language, discuss the generation and use of constraints, show their use in the compiler, formalize the preservation of properties, present subtleties, and outline implementation details.
This paper will appear at WWW 2007 and is available at http://www2007.org/paper140.php.
Verification of Network Flows Using a Type System with Constrained Polymorphism

LiKai Liu, Azer Bestavros, Assaf Kfoury, Abraham Matta (Boston University)
We propose a typed domain-specific language TRAFFIC(X) for the specification and analysis of end-to-end network flow configurations. TRAFFIC(X) is inspired by HM(X), a framework that augments the familiar Hindley-Milner polymorphic type system for ML-like functional languages with a constraint system X. In TRAFFIC(X), the constraint system X can be instantiated to different constraint-rewriting rules, corresponding to the verification of different properties of network flows. To illustrate our methodology, we examine two examples: (1) proper nesting of tunneled streams by means of lossy or lossless compression and encryption; and (2) computing round-trip time using linear-programming constraints.
This talk presents work done in collaboration with Azer Bestavros, Abraham Matta, and Assaf Kfoury at Boston University. For more information on this project, see csr.bu.edu/traffic.
Jeannie: making the Java Native Interface Pretty and Light-Weight

Martin Hirzel (IBM), Robert Grimm (NYU)
Many programs are written in more than one language. Reasons for this include reuse of legacy libraries, access to platform functionality, and efficiency. Jeannie is a language design for integrating Java with C, aiming at programmer productivity, static and dynamic error checking, portability, and efficiency. Both Java code and C code are nested in each other in the same file, and compile down to traditional JNI. Jeannie performs static semantic checks and facilitates dynamic resource management and exception handling, two concerns that otherwise make JNI applications ugly and heavy-weight. This talk reports on our experiences from a prototype Jeannie compiler, and highlights areas for future work on language interoperability.
LADDIE: The Language for Automated Device Drivers

Lea Wittie, Derrin Pierret (Bucknell University)
Device drivers are known to be a main source of OS bugs. Several research groups have created driver specification languages that dynamically check pre- and postconditions on the IO operations of a device driver. Low level type safe languages exist that can statically check function pre- and postconditions. However, these low level languages are too general to make the specific task of driver writing simple. This research presents Clay, a low level type safe language that has the facilities to statically check the safety of a device driver, and Laddie, a device driver specification language which compiles to Clay thus leveraging its static safety checking while remaining simple to use. Clay, developed at Dartmouth, is a C-like language which dependent types, like those of DML, to track program values statically. It builds on the linear logic of Girard to produce linear capabilities which guard access to memory and to logical system state and prevent aliasing errors. Clay also incorporates the arithmetic constraints of Xi and Pfenning into function pre- and postconditions to produce Hoare Triples, {P} f {Q} where P and Q are pre- and postconditions on function f. Clay statically enforces linear access to memory and statically checks all pre- and post conditions on function calls. When successfully type checked, a Clay program then compiles to C++. There are several existing specification languages for device drivers including Devil, NDL, and Hail. All of these perform dynamic safety checks. To move the safety checks to compile time, we created Laddie, a language for specifying the IO communication between a driver and its device. Devices are typically accessed via a set of locations called registers. Each register has rules governing how and when it can be accessed. These rules may depend on the logical state of the device, which is not usually stored in driver memory. (This state might include the status of device interrupts). Laddie uses syntax similar to that of Hail to allow a simple encoding of the complex rules and logical device state into pre- and postconditions on access to registers. Laddie compiles to Clay which checks the pre- and postconditions statically.
This talk presents work done in collaboration with Chris Hawblitzel (Microsoft Research) and Derrin Pierret (undergraduate at Bucknell University). For more information on Laddie and Clay, see http://www.eg.bucknell.edu/~lwittie/research.html.
Building an Efficient Generational Garbage Collector for Java Application Servers

Feng Xian, Witawas Srisa-an, ChengHuan Jia, Hong Jiang (University of Nebraska, Lincoln)
Recent studies have found that generational collection strategies employing only one nursery do not not perform well in application servers due to their inability to efficiently manage objects with diverse lifespans. In this presentation, we introduce a generational collector that takes advantage of an intrinsic behavior of many application servers; that is remotable objects are commonly used as gateways for client requests, and objects instantiated as part of these requests (remote objects) tend to live longer than objects not created to serve remote requests (local objects). This insight is used to segregate remote and local objects in two separate nurseries; each is properly sized to allow sufficient time for objects to die. We have implemented the proposed collector in the HotSpot virtual machine and evaluated its performance in a real-world application server setting. Given the same heap size, the proposed scheme can improve the maximum throughput by as much as 14% over the default generational collector. In addition, the proposed scheme allows the application server to handle a 10% higher workload before memory is exhausted. Our collector can achieve such performance benefits because it can reduce the frequency of full collection invocations, paging effort, average pause time, and overall garbage collection time.
This is a joint work with Feng Xian, ChengHuan Jia, and Hong Jiang. More information about this work can be found here.
Exterminator: Automatically Correcting Memory Errors with High Probability

Gene Novark (UMass Amherst)
Programs written in C and C++ are susceptible to memory errors, including buffer overflows and dangling pointers. These errors, which can lead to crashes, erroneous execution, and security vulnerabilities, are notoriously costly to repair. Tracking down their location in the source code is difficult, even when the full memory state of the program is available. Once the errors are finally found, fixing them remains challenging: even for critical security-sensitive bugs, the average time between initial reports and the issuance of a patch is nearly one month. We present Exterminator, a system that automatically corrects heap-based memory errors without programmer intervention. Exterminator exploits randomization to pinpoint errors with high precision. From this information, Exterminator derives runtime patches that fix these errors both in current and subsequent executions. In addition, Exterminator enables collaborative bug correction by merging patches generated by multiple users. We present analytical and empirical results that demonstrate Exterminator's effectiveness at detecting and correcting both injected and real faults.
This talk presents joint work with Emery Berger (UMass Amherst) and Ben Zorn (Microsoft Research). Our paper can be found at http://www.cs.umass.edu/~emery/pubs/pldi028-novark.pdf
Space-Efficient Gradual Typing

David Herman (Northeastern University), Aaron Tomb, Cormac Flanagan (UC Santa Cruz)
Gradual type systems offer a smooth continuum between static and dynamic typing by permitting the free mixture of typed and untyped code. The runtime systems for these languages---and other languages with hybrid type checking---typically enforce function types by dynamically generating function proxies. This approach can result in unbounded growth in the number of proxies, however, which drastically impacts space efficiency and destroys tail recursion. We present an implementation strategy for gradual typing that is based on coercions instead of function proxies, and which combines adjacent coercions to limit their space consumption. We prove bounds on the space consumed by coercions as well as soundness of the type system, demonstrating that programmers can safely mix typing disciplines without incurring unreasonable overheads. Our approach also detects certain errors earlier than prior work.
This talk presents joint work done with Aaron Tomb and Cormac Flanagan (University of California, Santa Cruz). Our paper can be found at http://www.ccs.neu.edu/home/dherman/research/publications/tfp07-gradual-typing.pdf.
Spatial Computing with Proto

Jonathan Bachrach, Jacob Beal (MIT)
Spatial computing is an increasingly prevalent mode of computing, in which a program runs on a collection of devices spread through space whose ability to interact is strongly dependent on their geometry. Spatial computing arises in many domains: sensor networks, smart materials, swarm robotics, biofilms, and modular robotics, to name a few. Programmability has been a major barrier to the deployment of spatial computing systems. Applications become entangled with the details of coordination and robustness, and as a result we see a plethora of niche solutions which often do not scale or compose well, let alone translate to other application domains. We offer an alternate approach, in which the application programmer expresses programs in terms of the global behavior of an {\em amorphous medium}---a continuous computational material filling the space of interest. We accomplish this with two components: a programming language, called Proto, for a spatial computer which implements the {\em amorphous medium} abstraction and a distributed operating system which marshalls a collection of devices into a virtual spatial computer implementing Proto semantics approximately. Proto has been demonstrated on platforms in three spatial computing domains: sensor networks, swarm robotics, and modular robotics.