Jeudi 14 février, 14h en salle Minquiers
An abstract stack based approach to verified compositional compilation to machine code
A key ingredient contributing to the success of CompCert, the state-of-the-art verified compiler for C, is its block-based memory model, which is used uniformly for all of its languages and their verified compilation. However, CompCert's memory model lacks an explicit notion of stack. Its target assembly language represents the runtime stack as an unbounded list of memory blocks, making further compilation of CompCert assembly into more realistic machine code difficult since it is not possible to merge these blocks into a finite and continuous stack. Furthermore, various notions of verified compositional compilation rely on some kind of mechanism for protecting private stack data and enabling modification to the public stack-allocated data, which is lacking in the original CompCert. These problems have been investigated but not fully addressed before, in the sense that some advanced optimization passes that significantly change the ways stack blocks are (de-)allocated, such as tailcall recognition and inlining, are often omitted. We propose a lightweight and complete solution to the above problems. It is based on the enrichment of CompCert's memory model with an abstract stack that keeps track of the history of stack frames to bound the stack consumption and that enforces a uniform stack access policy by assigning fine-grained permissions to stack memory. Using this enriched memory model for all the languages of CompCert, we are able to reprove the correctness of the full compilation chain of CompCert, including all the optimization passes. In the end, we get Stack-Aware CompCert, a complete extension of CompCert that enforces the finiteness of the stack and fine-grained stack permissions. Based on Stack-Aware CompCert, we develop CompCertMC, the first extension of CompCert that compiles into a low-level language with flat memory spaces. Based on CompCertMC, we develop Stack-Aware CompCertX, a complete extension of CompCert that supports a notion of compositional compilation that we call contextual compilation by exploiting the uniform stack access policy provided by the abstract stack.
Exposés des semaines suivantes
Vos propositions sont les bienvenues !
Mardi 5 mars, 14h30 en salle Minquiers
Jeudi 14 mars, 14h00 en salle Minquiers
Didier Lime (Ecole central de Nantes - LS2N)
Mardi 19 mars, 14h00 en salle Petri-Turing
A Different View of Multi-Body Systems Simulation
Multi-body systems such as robot mechanisms are usually modelled numerically by a Lagrangian approach, using a generalised coordinate vector q to describe system position. In the much used Independent Coordinates method, q has as many components as there are degrees of freedom. The equations of motion (EoM) reduce to an ODE - straightforward to solve but messy, with no clear connection to the physics. At an opposite extreme are Natural Coordinates (NCs), where q holds world-frame cartesian coordinates of suitable points on the moving parts. Then the EoM are an index 3 differential algebraic equation (DAE) system - the numerics are harder - typically using index reduction methods and a solver of the DASSL family - but the Lagrangian formulation is simple, sparse and human-readable. DAETS is a DAE code to solve high-index DAEs by Taylor series expansion, developed by Ned Nedialkov and me over the last 15 years. It is ideally suited to (smooth) mechanism problems, which it solves directly with no index-reduction stage. Using DAETS, algorithmic differentiation (AD) and our take on NCs, we create and solve the EoM directly from the Lagrangian function in a seamless run time process, with no computer algebra system used. Though the architecture of a classical NCs algorithm and of ours seem utterly different, they are surprisingly alike "under the bonnet". For instance a key Jacobian matrix turns out to be identical in both methods. The talk will explore similarities and differences, and issues of computational efficiency and user convenience.
Jeudi 4 avril, 14h00 en salle Minquiers
Francois Schwarzentruber (Logica)
Exposé-cours dans le cadre du séminaire Complexité