Additional CS EVENT today

["Shai Rubin" <shai@xxxxxxxxxxx>]

> --- Wednesday, December 5 ---
> 4:00 pm, 1325 CS
> Programming Languages Seminar: Glenn Ammons and Shai Rubin, "POPL 2002 
>    double-header"
> 
>    The Programming Languages Seminar this week is a double-header of
>    papers accepted to POPL 2002.  First, Glenn presents his paper,
>    "Mining Specifications":
> 
>       Program verification is a promising approach to improving
>       program quality, because it can search all possible program
>       executions for specific errors.  However, the need to formally
>       describe correct behavior or errors is a major barrier to the
>       widespread adoption of program verification, since programmers
>       historically have been reluctant to write formal specifications.
>       Automating the process of formulating specifications would
>       remove a barrier to program verification and enhance its
>       practicality.
> 
>       This paper describes specification mining, a machine learning
>       approach to discovering formal specifications of the protocols
>       that code must obey when interacting with an application program
>       interface or abstract data type.  Starting from the assumption
>       that a working program is well enough debugged to reveal strong
>       hints of correct protocols, our tool infers a specification by
>       observing program execution and concisely summarizing the
>       frequent interaction patterns as state machines that capture
>       both temporal and data dependences.  These state machines can be
>       examined by a programmer, to refine the specification and
>       identify errors, and can be utilized by automatic verification
>       tools, to find bugs.
> 
>       Our preliminary experience with the mining tool has been
>       promising.  We were able to learn specifications that not only
>       captured the correct protocol, but also discovered serious bugs.
> 
>       This is joint work with Prof. Ras Bodik from UW and James
>       R. Larus, from Microsoft Research.
> 
>    Next, Shai presents his paper, "An Efficient Profile-Analysis
>    Framework for Data-Layout Optimization":
> 
>       Data-layout optimizations rearrange fields within objects,
>       objects within objects, and objects within the heap, with the
>       goal of increasing spatial locality. While the importance of
>       data-layout optimizations has been growing, their deployment has
>       been limited, partly because they lack a unifying framework.
> 
>       In this talk we present a parameterizable framework for
>       data-layout optimization of general-purpose
>       applications. Acknowledging that finding an optimal layout is
>       not only NP-hard, but also poorly approximable, our framework
>       finds a good layout by searching the space of possible layouts,
>       with the help of profile feedback. The search process
>       iteratively prototypes candidate data layouts, evaluating them
>       by "simulating" the program on a representative trace of memory
>       accesses. To make the search process practical, we develop
>       space-reduction heuristics and optimize the expensive simulation
>       via memoization.
> 
>       Equipped with this iterative approach, we can synthesize layouts
>       that outperform existing non-iterative heuristics, tune
>       application-specific memory allocators, as well as compose
>       multiple data-layout optimizations.
> 
>       This is a joint work with Prof. Ras Bodik from UW and Trishul
>       Chilimbi from Microsoft Research.
>