Arrival and Coffee: 9:30 - 10:00
Session 1: 10:00 - 10:45
Stephen Tse (University of Pennsylvania)
Lattice and Information-flow
Break: 10:45 - 11:00
Session 2: 11:00 - 12:30
Robert Grimm (New York University)
Towards Extensible C - Step 1: The Parser
Michael Hicks (University of Maryland)
Dynamic update system
Lunch: 12:30 - 1:50
Business meeting: 1:50 - 2:00
Session 3: 2:00 - 3:30
David Naumann (Stevens Institute of Technology)
Towards imperative modules
Mike Plusch (Clear Methods, Inc)
Understanding complex Web services requirements through rapid
prototyping with Water
Abstract: Operating and distributed systems can significantly benefit from language and compiler support, even if they are written in C or C++ and not in a fully type-safe or functional programming language. Examples include libasync for building event-driven distributed services, Capriccio for building scalable multi-threaded servers, and MACEDON for building overlay networks. Unfortunately, existing solutions for extending C-like languages are either not expressive enough or targeted at compiler experts, thus preventing other system builders from reaping similar benefits. To address this problem, we are exploring a new macro facility for C, called xtc for eXTensible C, which will allow system builders to easily realize their application-specific extensions.
Our first step towards realizing xtc is a parser generator that supports easily modifiable grammars and avoids the complexities associated with extending bottom-up (LR) grammars or top-down (LL) grammars with lookahead. Our work builds on recent research on packrat parsers, which are top-down parsers that backtrack but also memoize each intermediate result (hence their name), thus ensuring linear-time performance. Our work makes this parsing technique, which has been developed in the context of functional languages, practical for C-like languages (currently, Java). Furthermore, our parser generator supports simpler grammar specifications and more convenient error reporting, while also producing better performing parsers through aggressive optimizations. In this talk, I motivate our overall research, describe our parser generator in detail, and reflect on how to structure extensible source-to-source transformers.
Abstract: Dynamic software updates can be used to fix bugs or add features to a running program without downtime. Essential for some applications and convenient for others, low-level dynamic updating support has been used for many years. However, there is little high-level understanding that would support programmers in writing dynamic updates effectively.
In an effort to bridge this gap, we present a formal calculus called Proteus for modeling dynamic software updating in C-like languages that is flexible, safe, and predictable. Proteus supports dynamic updates to functions (even those that are active) and types, allowing on-line evolution to match source-code evolution as we have observed it in practice. All updates are provably type-safe and *representation-consistent*, meaning that only one version of a given type may exist in the program at any time, simplifying reasoning and avoiding unintuitive copy-based semantics. Finally, Proteus's novel and efficient static _updateability analysis_ allows a programmer to automatically prove that an update is independent of the on-line program state, and thus predict it will not fail dynamically. Proteus admits a straightforward implementation, and we sketch how it could be extended to more advanced language features including threads.
Joint work with Gareth Stoyle, Peter Sewell, Gavin Bierman, and Iulian Neamtiu.
Abstract: Imperative and object-oriented programs make ubiquitous use of shared mutable objects. Updating a shared object can and often does transgress a boundary that was intended to be established using static constructs such as a class with private fields. We show how auxiliary fields can be used to express two state-dependent encapsulation disciplines: ownership, a kind of separation, and local co-dependence, a kind of sharing. The use of auxiliary state offers considerably more flexibility than type-based alias control. The disciplines support modular specification and verification of encapsulated object invariants and also simulations for proving program equivalence.
Based on joint work with Mike Barnett and with Anindya Banerjee.
Abstract: Designing and testing XML Web services pose special challenges to organizations and enterprises; challenges that can be uniquely addressed by rapid prototyping. Typically, Web services involve multiple evolving standards and APIs, a variety of XML encoding styles, and numerous languages and technologies. Web services can be especially hard to completely test and understand before they are fully deployed. Yet, because Web services are extremely difficult and expensive to modify after they are deployed, it is particularly important to resolve conceptual flaws early in the process. The concept of rapid prototyping with the Water language is the solution to these challenges.