NU Programming Languages Seminar Wednesday, June 1, 2005 11:45-1:15 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Patrick Cousot Ecole Normale Superieure, Paris Visiting MIT Aero-Astro Department
A basic property of software is that there should be no reachable state of the computations in which an undefined operation can be performed. For example in synchronous software, as found in safety critical embedded application such as electric flight control, a runtime error might raise an interrupt whence break the synchrony.
The state space of such huge programs (hundreds of thousands of lines) is so large that it cannot be explored explicitly by model-checking nor reasonably covered by testing. A (computer-aided) formal proof would be humanely insurmountable and economically very costly.
An alternative is to use static analysis where an abstraction of the semantics of the programs is automatically computed which leaves out all information about reachable states which is not strictly necessary for the proof. Of course if the abstraction is too precise, the computation cost are too high (resource exhaustion) and if it is too rough, nothing can be proved (false alarm). Although the best abstraction does exist, it is not computable, and so, must be found experimentally.
We will provide an intuition for the underlying theory, that of abstract interpretation, and then report on an application to the proof of absence of runtime errors in the electric flight control system of commercial planes. In this project the abstraction has been tuned manually to get no false alarm, whence a correctness proof, certainly a world premiere for a program of that size (see the ASTREE project, http://www.astree.ens.fr/).
We will conclude by grand challenges for static program/specification analysis the next 5 to 10 years.
NU Programming Languages Seminar Wednesday, April 20, 2005 11:45-1:15 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Gene Cooperman
TOP-C, Aspects, and a Vision of Semi-Automatic Parallelism
This will be an informal talk discussing some of the background of high performance computing, and where there _ought_ to be some opportunities for aspects. A grand vision for parallel computing is semi-automatic parallelism. In this vision, one writes a sequential program (or takes a pre-existing program), adds a small number of high-level annotations (comments), and then transforms the program to a parallel program.
Such transformations can be handled by compileres, by preprocessors, by transformation programs (such as CIL), or by aspects. Such strategies are required for a variety of transformations. Some examples are: 1) transformation of 'for' and 'while' loops to the trivial loop parallelism; 2) transformation of complex data structures to stub functions for marshalling those data structures; 3) transformation of recursive programs to invoke parallelism (see, for example, the Cilk package for parallelism using 'spawn' and 'sync'); 4) insertion of synchronization for the shared memory version of TOP-C; and 5) insertion of checkpointing code transparently to the application writer.
TOP-C (Task Oriented Parallel C/C++) is a parallel package providing a compiler script that links a TOP-C application to a run-time library. TOP-C supports a single API that can link with run-time libraries both for distributed and shared memory computation. It has been used, for example, to parallelize Geant4, a million line C++ program used to design experiments for the largest collider in the world, at CERN.
NU Programming Languages Seminar Wednesday, April 6, 2005 12:00-1:15 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Eli Barzilay
Implementing Syntactic Reflection in Nuprl
Reflection is the ability of some entity to refer to itself. In a logical context, it is the ability of a logic to reason about itself. Reflection is, therefore, placed at the core of meta-mathematics, making it an important part of formal reasoning; where it revolves mainly around syntax and semantics --- the main challenge is in making the syntax of the logic become part of its semantic domain.
Given its importance, it is surprising that logical computer systems tend to avoid the subject, or provide poor tools for reflective work. This is in sharp contrast to the area of programming languages, where reflection is well researched and used in a variety of ways where it plays an central role. One factor in making reflection inaccessible in logical systems is the relative difficulty that is immediately encountered when formalizing syntax: dealing with formal syntax means dealing with structures that involve bindings, and in a logical context it seems natural to use the same formal tools to describe syntax --- often limiting the usability of such formalizations to specific theories and toy examples. Godel numbers are an example for a reflective formalism that serves its purpose, yet is impractical as a basis for syntactical reasoning in applied systems.
In programming languages, there is a simple yet elegant strategy for implementing reflection: instead of making a system that describes itself, the system is made available to itself. We name this strong reflection, where the representation of language features via its semantics is actually part of the semantics itself --- unlike the usual practice in formal systems of employing weak reflection. The advantages of this approach is the fact that both the system and its reflected counterpart are inherently identical, making for a lightweight implementation.
In this work we develop the formal background and the practical capabilities of an applied system, namely Nuprl, that are needed to support strong reflection of its own syntax. Achieving this is a major milestone on the road for a fully reflected logical system. As we shall demonstrate, our results enable dealing with syntactical meta-mathematical content.
NU Programming Languages Seminar Wednesday, March 30, 2005 11:45-1:15 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Felix Klock
The Space Efficiency of Garbage Collection with a Partitioned Heap
Many virtual machine implementations employ a generational garbage collection system to perform automated memory management. Researchers have experimented with several variants of generational garbage collection, all of which maintain some partitioning of the heap and employ some policy to determine which partitions to garbage collect.
In this talk, I will first describe one abstract machine that represents a large class of such garbage collection algorithms, and prove that it computes the same answers as an abstract machine with no heap partitioning. Then I will describe a second abstract machine representing the class of 2-space younger-first garbage collectors, prove that it computes the same answers as the other machines, and prove that it and the machine with no heap partitioning are in the same space complexity class (in the sense of Clinger's "Proper Tail Recursion and Space Efficiency"). Finally I will discuss research-in-progress on modeling the Garbage-First collector of Detlefs et al. in this same framework.
NU Programming Languages Seminar Wednesday, March 23, 2005 11:45-1:15 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Cormac Flanagan UC Santa Cruz
Type Systems for Multithreaded Software
Developing correct multithreaded software is very challenging, due to the potential for unintended interference between threads. We present type systems for verifying two key non-interference properties in multithreaded software: race-freedom and atomicity. Verifying atomicity is particularly valuable since atomic procedures can be understood according to their sequential semantics, which significantly simplifies subsequent (formal and informal) correctness arguments. We will describe our experience applying these type systems and corresponding type inference algorithms to standard multithreaded benchmarks and other applications, and illustrate some defects revealed by this approach.
NU Programming Languages Seminar Two talks: Tuesday, March 22, 2005, and Wednesday March 23, 2005
Tuesday, March 22, 2005 2:00-3:00pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Jim Miller Microsoft
Innovation in the Real World: Making Generics Mainstream The notion of generic types, in one form or another, has been around for over 25 years. But their introduction into Java, C#, Visual Basic, COBOL, C++, FORTRAN, and PASCAL will make them available to "the average programmer." This talk describes the real-world engineering issues involved in making this happen - from the technical difficulties, to the scheduling issues, to the political realities of changing a platform that's in use by (literally) millions of developers. We'll also talk about the very tricky process by which innovations move from research prototypes into fully supported, widely deployed systems.
Wednesday, March 23, 2005 11:45-1:15 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Cormac Flanagan UC Santa Cruz
Type Systems for Multithreaded Software
Developing correct multithreaded software is very challenging, due to the potential for unintended interference between threads. We present type systems for verifying two key non-interference properties in multithreaded software: race-freedom and atomicity. Verifying atomicity is particularly valuable since atomic procedures can be understood according to their sequential semantics, which significantly simplifies subsequent (formal and informal) correctness arguments. We will describe our experience applying these type systems and corresponding type inference algorithms to standard multithreaded benchmarks and other applications, and illustrate some defects revealed by this approach.
NU Programming Languages Seminar Wednesday, January 26, 2005 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) 11:45am-1:30pm
Martin Hirzel, IBM
Connectivity-based garbage collection
Heap objects are connected to each other and to roots by pointers. Garbage collection traverses pointers to discover connectivity between objects, and reclaims objects that are not connected to program variables anymore. One can speed up that traversal by analyzing the program code for a conservative approximation of where pointers may exist. As it turns out, that pointer analysis information can also help focus garbage collection effort, by avoiding repeated traversal of long-lived objects. Connectivity-based garbage collection is designed for exploiting connectivity information from a pointer analysis. I will present connectivity-based garbage collection, along with a pointer analysis that works in the presence of dynamic class loading in a Java virtual machine.
NU Programming Languages Seminar Wednesday, January 19, 2005 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) 11:45am-1:30pm
Kathi Fisler (WPI) and Shriram Krishnamurthi (Brown)
Modular Verification of Software Systems
Aspect-oriented programming (AOP) has become an increasingly important programming paradigm. AOP is one of a family of means for expressing abstractions that cut across the program's dominant modularity; these techniques enable the construction of software by composing features. Despite their importance, feature-based programming methods lack supporting computer-aided verification techniques, which are necessary for increasing reliability and developing confidence in systems.
This talk presents a technique for verifying feature-based programs (expressed as state machines). By analogy with modular compilation, we support modular verification, to both enable independent development and to reduce the computational cost of verification. We present the analysis and discuss subtleties that arose as we applied our prototype verifiers to real case studies.
NU Programming Languages Seminar Wednesday, November 17, 2004 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) 11:45am-1:30pm
A Core Calculus of Metaclasses
Sam Tobin-Hochstadt
Metaclasses provide a useful method of abstraction for programmers working with object-oriented languages, but they have not seen the formal exploration applied to more conventional object-oriented programming features. In order to elucidate the structure of metaclasses and their relationship with static typing, we present a core calculus for a nominally-typed object-oriented language with metaclasses and prove type soundness over this core. This calculus is presented as an adaptation of Featherweight GJ, and is powerful enough to capture metaclass relationships beyond what are expressible in common object-oriented languages, including arbitrary metaclass hierarchies and classes as values. We also explore the integration of object-oriented design patterns with metaclasses, and show how our calculus integrates several such patterns cleanly.
NU Programming Languages Seminar Wednesday, October 27, 2004 Room **166** West Village H (http://www.ccs.neu.edu/home/wand/directions.html) 11:45am-1:30pm
Joe Marshall, NU PRL
Integrating the .NET Libraries with Scheme or Look, Ma! No FFI!
Common Larceny.NET is a Scheme implementation hosted on Microsoft's .NET framework. One goal of the project is to make it easy for Scheme to use the libraries provided by the .NET framework. Another goal is to make it easy for Scheme to interoperate with other programs hosted by the .NET framework. I have adapted Ken Anderson and Timothy Hickey's `Java-dot' notation to enable Scheme programs to construct and manipulate .NET objects. .NET methods are integrated as first-class Scheme procedures. A traditional `foreign function interface' is unnecessary with this approach.
This short talk covers the Java-dot notation and provides some simple examples in how to use it. A few of the underlying details will be described, and some of the tricks of using Scheme to script other .NET applications will be discussed.
NU Programming Languages Seminar Wednesday, October 20, 2004 Room 366 West Village H (http://www.ccs.neu.edu/home/wand/directions.html) 11:45am-1:30pm
Summer Adventures in Subtyping and Inference
Carl Eastlund, NU PRL
Abstract:
This talk will present the content of Eifrig, Trifonov, and Smith's early papers on a type inference system for OOP which includes subtyping, polymorphism, and recursive types. This system can infer types for previously difficult programs using an algorithm similar to Hindley-Milner inference. Some of the drawbacks of this system will also be presented, including the lack of primary types and the difficulty of providing signatures for functions and modules.
NU Programming Languages Seminar Wednesday, September 15, 2004 Room 366 West Village H (http://www.ccs.neu.edu/home/wand/directions.html) 11:45am-1:30pm
Object-Oriented Programming Considered Harmful
Mike Sperber, DeinProgramm
When prescribing how to solve a problem, object-oriented analysis, design, and programming teaches to translate the world of the problem into the world of classes, methods, and mutable objects. Unfortunately, not all problems readily lend themselves to such a translation. Consequently, many object-oriented programs contain mismatches between the natural mental model for an entity in the problem solution and its representation in the code. Object-oriented programmers have accepted this rift as natural and necessary. It is not. Frequently, this merely leads to awkward and hard-to-understand code. Sometimes, however, this practice is outright dangerous, leading to incorrect implementation models that are very difficult to rectify once the programmer has made them.
This talk will be an anecdotal rant on the subject, and will showcase the problem (along with a better, non-object-oriented solution) by discussing real-world models for financial market data.
NU Programming Languages Seminar Monday, August 9, 2004 Room 366 West Village H (http://www.ccs.neu.edu/home/wand/directions.html) 11:45am-1:30pm
Algorithmic Differentiation of Functional Programs
Jeffrey Mark Siskind School of Electrical and Computer Engineering Purdue University
Algorithmic Differentiation (AD) is an established enterprise that seeks to take the derivatives of functions specified as programs through symbolic manipulation rather than finite differencing. AD has traditionally been applied to imperative programs. We have developed a novel framework for performing AD within modern functional programming languages, treating AD operators as first-class higher-order functions that take first-class function objects as arguments and produce first-class function objects as results. Doing so offers seven important advantages over the traditional imperative framework for AD.
- Functional programs represent the underlying mathematical notions more closely than imperative programs. - This formulation is modular and allows a library of functions to be built compositionally: root finders built on a derivative-taker, line search built on root finders, multivariate optimizers built on line search, other multivariate optimizers (with identical APIs) build on Hessian-vector multipliers, themselves built on AD operators, and so forth. - By allowing the callee to specify the necessary AD, rather than insisting that the caller provide appropriately transformed functions, internals can be hidden and changed, maintaining a modular structure previously not possible in AD codes. - It is straightforward to generate higher-order derivatives, i.e. derivatives of derivatives. - Differential forms become first-class higher-order functions that can be passed to optimizers or PDE solvers as part of an API. This allow one to easily express programming patterns, i.e. algorithm templates, that can be instantiated with different components as fillers. For example, one can construct an algorithm that needs an optimizer and leave the choice of optimizer unspecified, to be filled in later by passing the particular optimizer as a function parameter. - Gradients can even be taken through processes that themselves involve AD-based optimization or PDE solution. - In traditional AD formulations, the output of an AD transformation is a `tape' that is a different kind of entity than user-written functions. It must be interpreted or run-time compiled. In contrast, in our approach, user-written functions, and the input and output of AD operators, are all the same kind of entity. Standard compilation techniques for functional programs can eliminate the need for interpretation or run-time compilation of derivatives and generate, at compile-time, code for derivatives that is as efficient as code for the primal calculation.
We illustrate the above advantages with examples that run in an implemented system. Our techniques can be applied to problems in such diverse fields as engineering design, scientific computing, and machine learning, where researchers regularly need to take derivatives of complex models specified as programs.
Joint work with Barak Pearlmutter.
Last modified: Mon Aug 21 15:06:24 EDT 2006