[Colloq] Galen Williamson, PhD Dissertation Defense, Monday, March 29, Galen Williamson

[Rachel Bates]

*College** of **Computer** and Information Science*
presents**
*PhD Dissertation Defense*

by
*Galen Williamson*

Who will speak on
*Flow Analysis for Higher-Order Multithreaded Computations*

* *

*Monday, March 29, 2004*

*10:00am*

*406 Egan*

 

_Abstract_

 

In this dissertation, we present a modular, extensible proof technique 
for constraint-based control flow analysis with respect to small-step 
semantics, emphasizing clarity and simplicity of presentation and ease 
of extension for both the analysis and their proofs.  We establish the 
proof technique relative to the lambda-calculus under substitution 
semantics with unrestricted beta-reduction.  To demonstrate the 
extensibility of the technique, we develop a series of larger languages, 
proving soundness of the control flow analysis for each successive 
language.  We begin this development with an environment-based machine 
semantics for the sequential lambda-calculus, and then add a store to 
support mutable structures and mutable variables based on implicit 
references, in the fashion of Scheme.  We conclude the development by 
adding concurrency, with first-class threads and interthread 
synchronization primitives, along with a publish-subscribe mechanism for 
event-oriented programming.

 

Finally, we explore the application of constraint-based analysis to a 
problem in program understanding and verification, extending the control 
flow analysis to compute information about thread interactions involving 
both synchronization and event-notification operations.  We build 
constraints to discover violations of a high-level, informal invariant 
on thread interactions in an idealized example program designed to 
illustrate a bug found in a real-world multithreaded application.  We 
then show that the analysis is too conservative, leading to the flagging 
of false positives for invariant violations in a repaired version of the 
example program.  We conclude with remarks on the limitations of current 
control flow analysis technology to avoid such false positives, and 
suggestions for directions of future research.