[Colloq] REMINDER - Galen Williamson, PhD Dissertation Defense,
TODAY, March 29, 10AM
Rachel Bates
rachelb at ccs.neu.edu
Mon Mar 29 09:49:57 EST 2004
*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.
_______________________________________________
Colloq mailing list
Colloq at lists.ccs.neu.edu
https://lists.ccs.neu.edu/bin/listinfo/colloq
_______________________________________________
Colloq mailing list
Colloq at lists.ccs.neu.edu
https://lists.ccs.neu.edu/bin/listinfo/colloq
More information about the Colloq
mailing list