Programming Languages Seminar, Spring 2005

This is the home page for the Spring 2005 Programming Languages seminar. You can get information about the upcoming talk, as well as about past talks this semester.

This Week's Talk

Future Talks for Fall 2005

Past Talks from Fall 2005

Past Talks from 2004

This Week's Talk

Thursday, May 5, 2005 , 11:00 - 12:00, 3401 Siebel Center

Speaker: Radu Rugina, Cornell
Title: Error Detection using Shape Analysis with Local Reasoning
Time: Thursday May 5, 11:00am
Place: 3401 SC

Abstract:

Shape analyses are static analyses aimed at extracting invariants that describe the "shapes" of dynamically allocated recursive structures.
Although existing shape analyses have been successful at verifying complex heap manipulations, they have had limited success at being practical for larger programs. In particular, they have not been incorporated in scalable error-detection tools so far.

In this talk I will present a novel approach to shape analysis: using local reasoning about individual heap locations, instead of global reasoning about entire heap abstractions. The key feature of this approach is a novel memory abstraction that models the heap using a set of independent configurations, each of which characterizes one single heap location. This approach makes it easier to build efficient inter-procedural and incremental heap analyses.

I will also present a prototype implementation that uses shape analysis to detect memory leaks and accesses through dangling pointers in C programs.
The current results suggest that the local reasoning approach is both sufficiently precise to accurately analyze a large class of heap manipulation algorithms, and sufficiently lightweight to scale to larger programs.

Speaker Bio:

Radu Rugina is an Assistant Professor in the Department of Computer Science at Cornell University. He received his Ph.D. from the University of California, Santa Barbara in 2001. Between 1997 and 2001, he was a visiting scholar at the M.I.T. Laboratory for Computer Science. Radu Rugina's research interests are in static analysis and compilation techniques for program understanding, verification, and transformation.
He is particularly interested in the analysis of pointer-based programs and its applications to error detection and memory management.

Future Seminar Talks

Date	Speaker/Topic

Past Seminar Talks

Date	Speaker/Topic
February 10 2005	T. Baris Aktemur spoke on the runtime generation of marshalling code in Java using Jumbo, a runtime program generation system. You can download the presentation using the following link: ppt
February 17 2005	Darko Marinov will present Object Equality Profiling. Description: We present Object Equality Profiling (OEP), a technique for helping programmers discover optimization opportunities in programs. OEP discovers opportunities for replacing a set of equivalent object instances with a single representative object. Such a set represents an opportunity for automatically or manually applying optimizations such as hash consing, heap compression, lazy allocation, object caching, invariant hoisting, and more. To evaluate OEP, we implemented a tool to help programmers reduce the memory usage of Java programs. Our tool performs a dynamic analysis that records all the objects created during a particular program run. The tool partitions the objects into equivalence classes, and uses collected timing information to determine when elements of an equivalence class could have been safely collapsed into a single representative object without affecting the behavior of that program run. We report the results of applying this tool to benchmarks, including two widely used Web application servers. Many benchmarks exhibit significant amounts of object equivalence, and in most benchmarks our profiler identifies optimization opportunities clustered around a small number of allocation sites. We present a case study of using our profiler to find simple manual optimizations that reduce the average space used by live objects in two SpecJVM benchmarks by 47% and 38% respectively. Joint work with Robert O'Callahan (Novell) done at IBM T. J. Watson Research Center
February 24 2005	Alejandra Garrido will present Representing and Analyzing Programs that Use the C Preprocessor Description: C preprocessor directives are heavily used in C programs since they provide useful and even necessary additions to the C language. However, they are usually executed and discarded before any analysis is applied on C programs. In refactoring, for example, preprocessor directives must be preserved through the whole process of parsing, analysis and transformation. In this talk we describe our pseudo-preprocessing and parsing techniques in CRefactory, a refactoring tool for C. These techniques create program representations that allow a program to be analyzed and transformed without losing its preprocessor directives. These representations will be useful for any program analysis tool that needs to preserve the unpreprocessed source code in the presence of a macro preprocessor.
March 3 2005	Luddy Harrison will present Programming Using Partial Orders and Fixed Points Description: I will describe the design of a programming language in which the types are partial orders, the statements are constraints over variables and monotonic expressions, and the result of the program is a fixed point over the constraints, i.e., a minimal setting of the variables with respect to their partial orders that satisfies the constraints. The language is straightforward to implement, and I will sketch a simple implementation. I will argue that the language has many of the desirable attributes of a functional or single-assignment language but has a slight edge over those languages in terms of expressiveness. I will illustrate some interesting types that are natural in this paradigm. This is very preliminary work, so attendees are encouraged to come with modest expectations.
March 10, 2005	Grigore Rosu will present Rewriting Logic Definitions of SIMPLE and FUN Programming Languages Description: We discuss a methodology to define executable semantics of programming languages in rewriting logic. Our definitions are modular and are based on a first order representation of continuations. Consequently, one can define programming language features independently and then put them together and thus design different programming languages. Once a language is defined this way, one obtains essentially for free an interpreter for that language together with various language analysis tools as instances of general purpose tools supporting rewriting logic. Languages like Java and Scheme have already been defined following the presented methdology, and many others are currently under development. In this talk we will discuss two toy languages, one called SIMPLE and the other called FUN. The later is a multi-threaded high-order language with support for thread synchronization and exceptions.
March 17, 2005	TITLE: Modular Static Analysis with Sets and Relations SPEAKER: Viktor Kuncak SPEAKER AFFILIATION: MIT CSAIL ABSTRACT: Ensuring data structure consistency is important for constructing reliable software systems. With the advances of modern memory-safe programming languages that eliminate low-level errors, high-level data structure consistency properties will become one of the main sources of errors in programs. This talk presents a framework for modular static analysis of data structure consistency properties. The framework uses data abstraction and assume/guarantee reasoning techniques to separate 1) the analysis of data structure implementations using precise analyses and 2) the analysis of data structure uses using more scalable analysis. We have developed three analyses in our framework: a flag analysis for modules in which abstract set membership is determined by a flag field in each object, a shape analysis for modules that encapsulate linked data structures such as lists and trees, and a theorem proving analysis for verifying arbitrarily complicated data structures including data structures that use arrays. Our experience shows that our system can effectively 1) verify the consistency of data structures encapsulated within a single module and 2) combine results from different analyses to verify properties involving objects shared by multiple modules analyzed by different analyses. The first version of our framework uses MONA decision procedure with custom formula simplifications to reason about global data structures represented as sets. We are currently extending the framework to support the analysis of binary relations. We will compare several candidate decision procedures suitable for reasoning about relations, including universal fragment of first-order logic, two-variable logic with counting, and Nelson-Oppen combination of multisorted theories. BIO: Viktor Kuncak is a PhD student at MIT working on static program analysis and verification. The work described in this talk is implemented in the context of the projects Hob and Jahob; additional details are available at http://www.mit.edu/~vkuncak/projects/jahob/.
April 7, 2005	Danny Dig will present "Refactoring - fearlessly changing the existing code" Description: Change is the only guaranteed constant in this world. Rather then running from change, we must learn how to cope with change. Refactoring is a change made to the internal structure of software to make it easier to understand and cheaper to modify without changing the observable behavior. In this talk we look at the manual and automated refactoring. We assess how long we have come so far and what are the challenges ahead.
April 21, 2005	Description: Speaker: Koushik Sen, UIUC Title: CUTE: A Concolic Unit Testing Engine for C Time: Thursday April 21, 11:00am Place: 3401 SC Abstract: We present a novel technique that automates unit testing based on a cooperative concrete and symbolic (concolic) execution of the code under test. Unit testing executes different paths of a software unit to check its correctness. Traditional techniques use either (1) concrete execution or (2) symbolic execution that builds constraints and is followed by a generation of concrete test inputs from these constraints. In contrast, our technique tightly couples both concrete and symbolic executions: they run simultaneously, and each gets feedback from the other. We have implemented our technique in a publicly available tool, called CUTE (Concolic Unit Testing Engine), for testing units written in C. The experiments on a security protocol, a popular data-structure library, and the tool itself show that CUTE can efficiently detect bugs and achieve high branch coverage.
April 28, 2005	Sam Kamin will present Source-level Optimization of Run-Time Program Generators (joint work with Baris Aktemur and Philip Morton) Abstract: We describe our efforts to use source-level rewriting to optimize run-time program generators written in Jumbo, a run-time program generation system for Java. Jumbo is a compiler written in \emph{compositional} style, which brings the advantage that any program fragment can be abstracted out and compiled to an intermediate form. These forms can be put together at run-time to build complete programs. This principle provides a high level of flexibility in writing program generators. However, this comes at the price of inefficient run-time compilation. Fortunately, generators are potentially subject to optimization. By using the information that a program fragment gives us and applying source-level transformations, we partially evaluate the program which generates the fragment. We achieve measurable speedups in run-time program generation. In this paper, we discuss the optimization process and give several examples.