Difference between revisions of "TACL Seminar Spring '06"

From CSWiki
Jump to: navigation, search
m (Chris Richards)
m (Spring '06 Schedule)
 
(31 intermediate revisions by the same user not shown)
Line 1: Line 1:
 
[[TACL Seminar]]
 
[[TACL Seminar]]
  
==Schedule==
+
==Spring '06 Schedule==
{| cellpadding="1"
+
{| border="1"
 
!Date
 
!Date
 
!Speaker
 
!Speaker
Line 8: Line 8:
 
!Links
 
!Links
 
|-
 
|-
| Mar 1 || [http://www.cs.princeton.edu/~ljia/ Limin Jia] and< [http://www.cs.princeton.edu/~frances/ Frances Spalding] || Automated Reasoning about Pointer Programs using Linear Logic
+
| Mar 1 || [http://www.cs.princeton.edu/~ljia/ Limin Jia] and [http://www.cs.princeton.edu/~frances/ Frances Perry] || Automated Reasoning about Pointer Programs using Linear Logic
 
|-
 
|-
| Mar 8 || [http://www.cs.princeton.edu/~ljia/ Limin Jia] || ILC: A Foundation for Automated Reasoning About Pointer Programs || [[ TACL_Seminar_Spring_'06#Limin_Jia | Abstract]]
+
| Mar 8 || [http://www.cs.princeton.edu/~ljia/ Limin Jia] || ILC: A Foundation for Automated Reasoning About Pointer Programs || [[ TACL_Seminar_Spring_'06#Limin_Jia | Abstract]] / [http://www.cs.princeton.edu/~ljia/research/papers/ilc_esop.pdf Paper]
 
|-
 
|-
 
| Apr 5 || [http://www.cs.princeton.edu/~gewang/ Ge Wang] || [http://chuck.cs.princeton.edu/ ChucK] and [http://audicle.cs.princeton.edu/ Audicle]: Programming Language and Environment for Sound Synthesis || [[ TACL_Seminar_Spring_'06#Ge_Wang | Abstract ]]
 
| Apr 5 || [http://www.cs.princeton.edu/~gewang/ Ge Wang] || [http://chuck.cs.princeton.edu/ ChucK] and [http://audicle.cs.princeton.edu/ Audicle]: Programming Language and Environment for Sound Synthesis || [[ TACL_Seminar_Spring_'06#Ge_Wang | Abstract ]]
Line 16: Line 16:
 
| Apr 10 || [http://www.cs.princeton.edu/~richards/ Chris Richards] || A Refined Kripke Semantics for Hard-to-Model Types || [[TACL_Seminar_Spring_'06#Chris_Richards | Abstract]]
 
| Apr 10 || [http://www.cs.princeton.edu/~richards/ Chris Richards] || A Refined Kripke Semantics for Hard-to-Model Types || [[TACL_Seminar_Spring_'06#Chris_Richards | Abstract]]
 
|-
 
|-
| May 17 || Mike Hind (IBM) || Online Performance Auditing: Using Hot Optimizations Without Getting Burned
+
| Apr 11 || [http://www.research.att.com/~bs/ Bjarne Stroustrup (AT&T Research)] || Specifying C++ Concepts || [[TACL_Seminar_Spring_'06#Bjarne_Stroustrup | Abstract]] / [http://www.research.att.com/~bs/popl06.pdf Paper]
 
|-
 
|-
| May 18 || [http://www.cs.princeton.edu/~mbridges/ Matthew Bridges] || Automatic Instruction Scheduler Retargeting by Reverse-Engineering
+
| Apr 17 || align="center" colspan="3" | [http://research.ihost.com/plday06/ IBM Research Programming Languages Day]
 +
|-
 +
| May 17 || [http://www.research.ibm.com/people/h/hind/ Mike Hind (IBM Research)] || Online Performance Auditing: Using Hot Optimizations Without Getting Burned || [[TACL_Seminar_Spring_'06#Mike_Hind | Abstract]] / [http://researchweb.watson.ibm.com/people/h/hind/papers.html#pldi06 Paper]
 +
|-
 +
| May 18 || [http://www.cs.princeton.edu/~mbridges/ Matthew Bridges] || Automatic Instruction Scheduler Retargeting by Reverse-Engineering || [[TACL_Seminar_Spring_'06#Matthew_Bridges | Abstract]] / [http://liberty.cs.princeton.edu/Publications/index.php?abs=1&setselect=pldi06_ard Paper]
 
|}
 
|}
  
Line 26: Line 30:
  
 
This paper shows how to use Girard's intuitionistic linear logic extended with a classical sublogic to reason about pointer programs. More specifically, first, the paper defines the proof theory for ILC (Intuitionistic Linear logic with Constraints) and shows it is well-defined via a proof of cut elimination. Second, inspired by prior work of O'Hearn, Reynolds, and Yang, the paper explains how to interpret linear logical formulas as descriptions of a program store. Third, this paper defines a simple imperative programming language with mutable references and arrays and gives verification condition generation rules that produce assertions in ILC. Finally, we identify a fragment of ILC, ILC$^{-}$, that is both decidable and closed under generation of verification conditions. Since verification condition generation is syntax-directed, we obtain a decidable procedure for checking properties of pointer programs.
 
This paper shows how to use Girard's intuitionistic linear logic extended with a classical sublogic to reason about pointer programs. More specifically, first, the paper defines the proof theory for ILC (Intuitionistic Linear logic with Constraints) and shows it is well-defined via a proof of cut elimination. Second, inspired by prior work of O'Hearn, Reynolds, and Yang, the paper explains how to interpret linear logical formulas as descriptions of a program store. Third, this paper defines a simple imperative programming language with mutable references and arrays and gives verification condition generation rules that produce assertions in ILC. Finally, we identify a fragment of ILC, ILC$^{-}$, that is both decidable and closed under generation of verification conditions. Since verification condition generation is syntax-directed, we obtain a decidable procedure for checking properties of pointer programs.
 +
 +
[http://www.cs.princeton.edu/~ljia/research/papers/ilc_esop.pdf ESOP '06 Paper]
  
 
===Ge Wang===
 
===Ge Wang===
Line 46: Line 52:
  
 
This includes joint work with Andrew Appel, Paul-Andre Mellies, and Jerome Vouillon.
 
This includes joint work with Andrew Appel, Paul-Andre Mellies, and Jerome Vouillon.
 +
 +
===Bjarne Stroustrup===
 +
'''Specifying C++ Concepts'''
 +
 +
C++ templates are key to the design of current successful mainstream libraries and systems.  They are the basis of programming techniques in diverse areas ranging from conventional general-purpose programming to software for safety-critical embedded systems. Current work on improving templates focuses on the notion of ''concepts'' (a type system for templates), which promises significantly improved error diagnostics and increased expressive power such as concept-based overloading and function template partial specialization. This paper presents C++ templates with an emphasis on problems related to separate compilation.
 +
 +
We consider the problem of how to express concepts in a precise way that is simple enough to be usable by ordinary programmers. In doing so, we expose a few weakness of the current specification of the C++ standard library and suggest a far more precise and complete specification. We also present a systematic way of translating our proposed concept definitions, based on use-patterns rather than function signatures, into constraint sets that can serve as convenient basis for concept checking in a compiler.
 +
 +
[http://www.research.att.com/~bs/popl06.pdf POPL '06 Paper]
 +
 +
===Mike Hind===
 +
'''Online Performance Auditing: Using Hot Optimizations Without Getting Burned'''
 +
 +
The past decades have seen substantial advances in the way programs are developed, thus improving software developers' ability to construct sophisticated applications.  Over these same decades
 +
computer systems advanced as well, delivering the performance needed to run these complex applications.  However, future trends suggest that the complexity of software will continue to increase, yet the performance improvements obtained from processor technology will diminish.  This presents a significant challenge and opportunity for the 'old' field of software optimization.
 +
 +
Meanwhile, as hardware complexity increases and virtualization is added at more layers of the execution stack, predicting the performance impact of optimizations becomes increasingly difficult. Although optimizations typically perform well on average, they often have unpredictable impact on running time, sometimes degrading performance significantly. Today's VMs perform sophisticated
 +
feedback-directed optimizations, but these techniques do not address performance degradations, and they actually make the situation worse by making the system more unpredictable.
 +
 +
This talk presents the Performance Auditor, an online framework for evaluating the effectiveness of optimizations, which enable an online system to automatically identify and correct performance anomalies that occur at runtime.  With this technology an optimization system can utilize more aggressive optimizations with that knowledge that a significant degradation will be detected and fixed.  This work opens the door for a fundamental shift in the way optimizations are developed and tuned for online systems, and may allow the body of work in offline empirical optimization search to be applied automatically at runtime. We present our implementation and evaluation of this system in a product Java VM.
 +
 +
This work is in collaboration with Matt Arnold, Jeremy Lau, and Brad Calder and will appear in PLDI'06.
 +
 +
[http://researchweb.watson.ibm.com/people/h/hind/papers.html#pldi06 PLDI '06 Paper]
 +
 +
===Matthew Bridges===
 +
'''Automatic Instruction Scheduler Retargeting by Reverse-Engineering'''
 +
 +
In order to generate high-quality code for modern processors, a compiler must aggressively schedule instructions, maximizing resource utilization for execution efficiency. For a compiler to produce such code, it must avoid structural hazards by being aware of the processor's available resources and of how these resources are utilized by each instruction. Unfortunately, the most prevalent approach to constructing such a scheduler, manually discovering and specifying this information, is both tedious and error-prone.
 +
 +
This paper presents a new approach which, when given a processor or processor model, automatically determines this information. After establishing that the problem of perfectly determining a processor's structural hazards through probing is not solvable, this paper proposes a heuristic algorithm that discovers most of this information in practice. This can be used either to alleviate the problems associated with manual creation or to verify an existing specification. Scheduling with these automatically derived structural hazards yields almost all of the performance gain achieved using perfect hazard information.
 +
 +
[http://liberty.cs.princeton.edu/Publications/index.php?abs=1&setselect=pldi06_ard PLDI '06 Paper]
  
 
----
 
----
  
 
[[TACL Seminar]]
 
[[TACL Seminar]]

Latest revision as of 16:54, 27 August 2006

TACL Seminar

Spring '06 Schedule

Date Speaker Title Links
Mar 1 Limin Jia and Frances Perry Automated Reasoning about Pointer Programs using Linear Logic
Mar 8 Limin Jia ILC: A Foundation for Automated Reasoning About Pointer Programs Abstract / Paper
Apr 5 Ge Wang ChucK and Audicle: Programming Language and Environment for Sound Synthesis Abstract
Apr 10 Chris Richards A Refined Kripke Semantics for Hard-to-Model Types Abstract
Apr 11 Bjarne Stroustrup (AT&T Research) Specifying C++ Concepts Abstract / Paper
Apr 17 IBM Research Programming Languages Day
May 17 Mike Hind (IBM Research) Online Performance Auditing: Using Hot Optimizations Without Getting Burned Abstract / Paper
May 18 Matthew Bridges Automatic Instruction Scheduler Retargeting by Reverse-Engineering Abstract / Paper

Abstracts

Limin Jia

ILC: A Foundation for Automated Reasoning About Pointer Programs

This paper shows how to use Girard's intuitionistic linear logic extended with a classical sublogic to reason about pointer programs. More specifically, first, the paper defines the proof theory for ILC (Intuitionistic Linear logic with Constraints) and shows it is well-defined via a proof of cut elimination. Second, inspired by prior work of O'Hearn, Reynolds, and Yang, the paper explains how to interpret linear logical formulas as descriptions of a program store. Third, this paper defines a simple imperative programming language with mutable references and arrays and gives verification condition generation rules that produce assertions in ILC. Finally, we identify a fragment of ILC, ILC$^{-}$, that is both decidable and closed under generation of verification conditions. Since verification condition generation is syntax-directed, we obtain a decidable procedure for checking properties of pointer programs.

ESOP '06 Paper

Ge Wang

ChucK and Audicle: Programming Language and Environment for Sound Synthesis

ChucK is a domain-specific programming language for real-time sound synthesis; the Audicle is a graphical development environment for programming ChucK "on-the-fly", and for monitoring the ChucK virtual machine in real-time. Together, they form a theoretical and a practical framework for writing and experimenting with complex audio/multimedia programs that (1) have powerful control over time and concurrency, (2) can be created on-the-fly, and (3) can map many input media (MIDI, joystick, keyboard, network, etc.) to sound synthesis parameters. In this seminar we present the language and environment, and show how ChucK has evolved since the last ChucK TACL seminar (2003).

We hope to make this an interesting and amusing presentation for all.

ChucK homepage

Audicle homepage

Chris Richards

A Refined Kripke Semantics for Hard-to-Model Types

In the semantic approach to proving a type system sound (relative to an operational semantics), we give mathematical interpretations to type constructors and typing judgments -- the latter in such a way as to imply safety -- and prove each typing rule as a lemma. Certain desirable features, such as recursive types, mutable references, and impredicative polymorphism, have been challenging to model, especially in combination. Drawing particularly on the indexed model of Ahmed, Appel, and Virga, I show a uniform way to handle these "problem types" using techniques from the semantics of modal logic, allowing well-typedness to be relative to worlds, or states of computation. I look especially to the logic of provability, which interprets the modal operator \Box as "it is provable that", and whose characteristic axiom reflects, in the model, an induction principle on worlds.

The resulting model is better modularized than its ancestor models, avoids some previous technical restrictions on quantified types, and applies equally well to lambda-calculus and von Neumann machine models of computation. We conjecture that our technique is suitable for any such model with a small-step operational semantics.

This includes joint work with Andrew Appel, Paul-Andre Mellies, and Jerome Vouillon.

Bjarne Stroustrup

Specifying C++ Concepts

C++ templates are key to the design of current successful mainstream libraries and systems. They are the basis of programming techniques in diverse areas ranging from conventional general-purpose programming to software for safety-critical embedded systems. Current work on improving templates focuses on the notion of concepts (a type system for templates), which promises significantly improved error diagnostics and increased expressive power such as concept-based overloading and function template partial specialization. This paper presents C++ templates with an emphasis on problems related to separate compilation.

We consider the problem of how to express concepts in a precise way that is simple enough to be usable by ordinary programmers. In doing so, we expose a few weakness of the current specification of the C++ standard library and suggest a far more precise and complete specification. We also present a systematic way of translating our proposed concept definitions, based on use-patterns rather than function signatures, into constraint sets that can serve as convenient basis for concept checking in a compiler.

POPL '06 Paper

Mike Hind

Online Performance Auditing: Using Hot Optimizations Without Getting Burned

The past decades have seen substantial advances in the way programs are developed, thus improving software developers' ability to construct sophisticated applications. Over these same decades computer systems advanced as well, delivering the performance needed to run these complex applications. However, future trends suggest that the complexity of software will continue to increase, yet the performance improvements obtained from processor technology will diminish. This presents a significant challenge and opportunity for the 'old' field of software optimization.

Meanwhile, as hardware complexity increases and virtualization is added at more layers of the execution stack, predicting the performance impact of optimizations becomes increasingly difficult. Although optimizations typically perform well on average, they often have unpredictable impact on running time, sometimes degrading performance significantly. Today's VMs perform sophisticated feedback-directed optimizations, but these techniques do not address performance degradations, and they actually make the situation worse by making the system more unpredictable.

This talk presents the Performance Auditor, an online framework for evaluating the effectiveness of optimizations, which enable an online system to automatically identify and correct performance anomalies that occur at runtime. With this technology an optimization system can utilize more aggressive optimizations with that knowledge that a significant degradation will be detected and fixed. This work opens the door for a fundamental shift in the way optimizations are developed and tuned for online systems, and may allow the body of work in offline empirical optimization search to be applied automatically at runtime. We present our implementation and evaluation of this system in a product Java VM.

This work is in collaboration with Matt Arnold, Jeremy Lau, and Brad Calder and will appear in PLDI'06.

PLDI '06 Paper

Matthew Bridges

Automatic Instruction Scheduler Retargeting by Reverse-Engineering

In order to generate high-quality code for modern processors, a compiler must aggressively schedule instructions, maximizing resource utilization for execution efficiency. For a compiler to produce such code, it must avoid structural hazards by being aware of the processor's available resources and of how these resources are utilized by each instruction. Unfortunately, the most prevalent approach to constructing such a scheduler, manually discovering and specifying this information, is both tedious and error-prone.

This paper presents a new approach which, when given a processor or processor model, automatically determines this information. After establishing that the problem of perfectly determining a processor's structural hazards through probing is not solvable, this paper proposes a heuristic algorithm that discovers most of this information in practice. This can be used either to alleviate the problems associated with manual creation or to verify an existing specification. Scheduling with these automatically derived structural hazards yields almost all of the performance gain achieved using perfect hazard information.

PLDI '06 Paper


TACL Seminar