OUPS décembre 2024

ATTENTION: l'horaire a été modifié par rapport aux éditions précédentes (18h30 au lieu de 19h)

Le prochain OUPS aura lieu le jeudi 12 décembre 2024. Le rendez-vous est fixé à 18h30 au 4 place Jussieu, Amphi Astier, dans le bâtiment Esclangon.

L'inscription est obligatoire pour pouvoir accéder au meetup !
Les exposés seront également retransmis en ligne sur le galène du OUPS.
Toutes les informations sont disponibles sur le site du OUPS.

Programme :

Snapshottable Stores -- Clément Allain & Gabriel Scherer

We say that an imperative data structure is *snapshottable* or *supports snapshots* if we can efficiently capture its current state, and restore a previously captured state to become the current state again. This is useful, for example, to implement backtracking search processes that update the data structure during search.

Inspired by a data structure proposed in 1978 by Baker, we present a *snapshottable store*, a bag of mutable references that supports snapshots. Instead of capturing and restoring an array, we can capture an arbitrary set of references (of any type) and restore all of them at once. This snapshottable store can be used as a building block to support snapshots for arbitrary data structures, by simply replacing all mutable references in the data structure by our store references. We present use-cases of a snapshottable store when implementing type-checkers and automated theorem provers.

Our implementation is designed to provide a very low overhead over normal references, in the common case where the capture/restore operations are infrequent. Read and write in store references are essentially as fast as in plain references in most situations, thanks to a key optimisation we call *record elision*. In comparison, the common approach of replacing references by integer indices into a persistent map incurs a logarithmic overhead on reads and writes, and sophisticated algorithms typically impose much larger constant factors.

The implementation, which is inspired by Baker's and the OCaml implementation of persistent arrays by Conchon and Filliâtre, is both fairly short and very hard to understand: it relies on shared mutable state in subtle ways. We provide a mechanized proof of correctness of its core using the Iris framework for the Coq proof assistant.

Safe, expressive and efficient FPGA programming -- Loïc Sylvestre

FPGAs (Field-Programmable Gate Arrays) are reconfigurable digital circuits: their behavior can be customized by logic synthesis of specification at the so-called register transfer level (RT level), in hardware description languages such as VHDL or Verilog. FPGAs are well suited to implement reactive systems, directly as synchronous circuits interacting with the external environment via I/O pins – the logic synthesizer ensuring that timing constraints are met, given the FPGA clock frequency. FPGAs are also used to implement hardware accelerators ; however, RT-level descriptions of transformational systems (or “computations”) – with latencies of several clock cycles – are difficult to debug, maintain and manually optimize. High-Level Synthesis (HLS) offers a simpler way of expressing computations, using a programming language compiled at the RT level. The advantage of this approach is to keep the implementation details hidden from the programmer, leaving the compiler responsible for scheduling computations over time. However, this leads to a loss of control over temporal behavior and therefore safety and efficiency for the circuits generated. As embedded systems, especially those based on FPGAs, need to perform more and more computations, while interacting with their environment, this thesis proposes a programming model to combine hardware description (data-flow oriented) and general-purpose parallel computation (control-flow oriented) using a synchronous approach. This programming model forms the basis for the design and implementation of Eclat, a functional-imperative, parallel and synchronous programming language, compiled to VHDL. Eclat is sufficiently precise to describe synchronous circuits at the RT level. It facilitates the programming of hardware accelerators, with a clear and predictable temporal semantics by which to exploit time-space trade-offs. Any Eclat program is reactive, with a mechanism for embedding computations within programs and thereby mix computation and interaction. Eclat also offers shared memory (in the form of RAM blocks), with deterministic concurrency. It is used to develop programming abstractions such as algorithmic skeletons and virtual machine implementations for high-level languages. This addresses, at various levels, the need to run general-purpose algorithms within FPGA-based reactive embedded applications.

***

Les présentations seront suivies par des discussions libres. Les pizzas seront offertes par la fondation OCaml !