Additional CS EVENT on WEDNESDAY

[Glenn Ammons <ammons@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.