Difference between revisions of "TACL Seminar Spring '06"

From CSWiki
Jump to: navigation, search
m (Mike Hind)
m (Schedule)
Line 1: Line 1:
[[TACL Seminar]]
[[TACL Seminar]]
==Spring '06 Schedule==
{| cellpadding="1"
{| cellpadding="1"

Revision as of 22:00, 26 August 2006

TACL Seminar

Spring '06 Schedule

Date Speaker Title Links
Mar 1 Limin Jia and Frances Spalding Automated Reasoning about Pointer Programs using Linear Logic
Mar 8 Limin Jia ILC: A Foundation for Automated Reasoning About Pointer Programs Abstract
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 Specifying C++ Concepts Abstract
May 17 Mike Hind - IBM Online Performance Auditing: Using Hot Optimizations Without Getting Burned Abstract
May 18 Matthew Bridges Automatic Instruction Scheduler Retargeting by Reverse-Engineering


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.

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.

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.

TACL Seminar