*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h00                     *
*                           Salle S16, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************


***  Vendredi 13 juin 2008, 14h00-15h00 ****************************

Timing Analysis and Timing Predictability

Reinhard Wilhelm, Sarrebrucken University

Re'sume'/ Abstract:

On modern processor architectures, the execution time of a machine instruction
depends on the execution history. It can vary by several orders of magnitude.
Static program analysis is used to compute invariants about the set of all
execution states at an instruction to derive safe and tight upper bounds on
the execution time of the instruction in all these execution states. Based on
these upper bounds a longest path through the program is determined to verify
the time constraints.

The efficiency, even the feasibility, and the precision of the results of
timing analysis highly depend on predictability properties of the
architecture.
The predictability of architectures has been suffering from the optimization
of the wrong performance measure, namely average-case performance. Attempts to
improve predictability have often reduced the average-case performance.
We are looking for good compromises between predictability and (average-case)
performance.

Timing analysis `a la Saarbruecken uses several abstract interpretations,
 derived from a concrete model of the processor.
In terms of abstract interpretation this means that the concrete semantics of
the analyzed language contains the full architecture.
Different abstract semantics describe the cache behavior, the pipeline
behavior, and in the end the timing behavior.
Increasing predictability then means to change the architectural part of the
semantics to make the analyses more precise and more efficient.
The European ICT project Predator attempts to identify design principles for
predictable and performant architectures.


***  Vendredi 20 juin 2008, 14h00-15h00 ****************************

Static Analysis via Abstract Interpretation of the Happens-Before Memory Model

Pietro Ferrara (equipe/projet Abstraction)

Re'sume'/ Abstract:

Memory models define which executions of multithreaded programs are
legal. During this talk, I will present the formalization in a fixpoint
form of the happens-before memory model, an over-approximation of the
Java one, and I will define a static analysis of it using abstract
interpretation. Some preliminary experimental results will be presented
and discussed. This approach is completely independent on both the
programming language and the analysed property. It also appears to be a
promising framework in order to define, compare and statically analyse
other memory models.


***  Vendredi 27 juin 2008, 14h00-15h00 ****************************

Interprocedural Analysis of Concurrent Programs Under a Context Bound

Akash Lal (University of Wisconsin-Madison)

Re'sume'/ Abstract:

Analysis of recursive programs in the presence of concurrency and shared
memory is undecidable. In previous work, Qadeer and Rehof showed that
context-bounded analysis is decidable for recursive programs under a
finite-state abstraction of program data. In this talk, I will show that
context-bounded analysis is decidable for certain families of
infinite-state abstractions. Using weighted pushdown systems (WPDS) as
the model of a thread, we prove three key results: (i) the reachability
relation of a WPDS can be summarized using a weighted transducer; (ii)
these transducers can be composed when tensor products exist for the
weights; and (iii) tensor products do exist for a class of weight
domains.

This is joint work with Tayssir Touili, Nicholas Kidd, and Thomas Reps,
and was published in TACAS'08. Time permitting, I will also discuss how
we took lessons from this work and applied them in the concrete setting
to give us a way of reducing context-bounded analysis of concurrent
programs to analysis of sequential programs. This work is published in
CAV'08.

*********************************************************************
Pour recevoir l'annonce par courrier electronique:
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************