Note: You are viewing an old revision of this page. View the current version.

The following is a list of people who will be speaking at the weekly Sable meetings. Please add your talk title and abstract below your name.

Summer 2005

Winter 2005

We designed and implemented a new algorithm of handling Java synchronization primitives. This algorithm is based on existing works in this area, i.e. it uses bimodal locking to achieve maxiumum performance when there is no contention, while in presence of contention it provides additional guarantees, mainly as to the maximum number of fat locks in a system.

The goal of this thesis is to design techniques related to the automatic analysis of computer programs. One major application is the creation of tools to discover bugs before they actually happen, an important goal in a time when critical yet complex tasks are performed by computers. We will work in the Abstract Interpretation framework, a theory of sound approximation of program semantics. We will focus, in particular, on numerical abstract domains that specialize in the automatic discovery of properties of the numerical variables of programs.

In this thesis, we introduce new numerical abstract domains: the zone abstract domain (that can discover invariants of the form X - Y <= c), the zone congruence domain (X - Y in c + b Z), and the octagon domain (+/- X +/- Y <= c), among others. These domains rely on the classical notions of potential graphs, difference bound matrices, and algorithms for the shortest path closure computation. They are in-between, in terms of cost and precision, between non-relational domains (such as the interval domain), that are very imprecise, and classical relational domains (such as the polyhedron domain), that are very costly. We will call them `weakly relational'. We also introduce some methods to apply relational domains to the analysis of floating-point numbers, which was previously only possible using imprecise, non-relational domains. Finally, we introduce so-called `linearization' and `symbolic constant propagation' generic methods to enhance the precision of any numerical domain, for a low increase in cost.

The analysis framework presented in this thesis has been integrated within Astrée, an analyzer for critical embedded software, and were instrumental in proving the absence of run-time errors in fly-by-wire softwares. Experimental results show the usability of our methods in the context of real-life applications.

See also

Fall 2004

Speculative multithreading (SpMT) is a technique for automatic parallelisation of single-threaded programs. Speculative Method-Level Parallelism (SMLP), a variant of SpMT, performs significantly better in the presence of accurate return value prediction. We previously implemented and characterized some common value predictors in SableVM, and introduced a new memoization-based predictor. We now look to improving return value prediction further using Soot, our Java bytecode optimization and transformation framework. We present an interprocedural parameter dependence analysis that eliminates parameter inputs to our memoization predictor that do not affect the return value. This increases sharing in memoization lookup tables, improving accuracy and reducing size. We also present a return value use analysis to determine which return values are consumed, and furthermore label those that are only used inside boolean and branch expressions. This allows us to increase accuracy by substituting incorrect predictions at runtime, provided the relaxed constraints given by this analysis are met. We use Soot's attribute generation framework to enable SableVM to exploit the results of these analyses. This work has implications for non-speculative memoization strategies, and for general purpose load value prediction.

The Sable research group from McGill? University and the Programming Tools Group from Oxford University have recently developed abc, a research framework for the AspectJ programming language. The abc compiler is publicly-avaliable under the GNU LGPL license. The toolkit has been designed with research in mind, for both experimentation with new aspect-oriented language features and research into optimizations for aspect-oriented languages.

This talk introduces AspectJ language, presents the highlights of the abc compiler framework, and discusses some preliminary experimental data comparing the performance of the existing ajc compiler with the abc compiler.