A Functional Synchronous Language with Integer Clocks

A Functional Synchronous Language with Integer Clocks

Mardi 31/03/2015, LUG, salle du bas, 10h30 (to be confirmed)

Adrien Guatto ENS Ulm/Parkas

Résumé:

Synchronous languages in the vein of Lustre are first-order functional languages dedicated to stream processing. Lustre compilers use a type-like static analysis, the clock calculus_, to reject programs that cannot be implemented as finite state machines. The broad idea is to assign to each element of a stream a logical computation date in a global, discrete time scale. When this analysis succeeds, the types obtained guide the code generation phase of the compiler, which produces transition functions. In practice, these functions consists in simple, bounded memory C code featuring only assignments and conditional statements.

This talk presents a variation on Lustre and its compilation. Our proposal is twofold. First, we add a new construct that creates a local time scale whose internal steps are invisible from the outside. Second, we change the clock calculus to allow several elements of a stream to be computed during the same time step. I will discuss the resulting type system, and how the code generation scheme of Lustre, once adapted to this new setting, generates code featuring nested loops.

Validation of Memory Accesses Through Symbolic Analyses

Validation of Memory Accesses Through Symbolic Analyses

Exposé invité Aric, 12 mars 2015, 10h30

Laure Gonnord, UCBL / Compsys

Résumé:

Joined work with F. Pereira and his collegues @Univ Mineas Gerais,
Bresil. Published at oopsla’14
The C programming language does not prevent out-of-bounds memory
accesses. There exist several techniques to secure C programs;
however, these methods tend to slow down these programs substantially,
because they populate the binary code with runtime checks. To deal
with this problem, we have designed and tested a succession of static
analyses to remove the majority of these guards.

We validate these static analyses by incorporating our findings into
AddressSanitizer : we generate SPEC CINT 2006 code that is 17% faster
and 9% more energy efficient than the code produced originally by this
tool.

In this talk I will present some of the static analyses that we
designed in this paper, focusing on our new “symbolic range” analysis,
and also the techniques we use to be able to scale well.