Sites Inria

Version française

Séminaire des équipes de recherche

Formal Verification of Data Layout Transformations

© INRIA Sophie Auvin - G comme Grille

Data layout transformations such as array-of-structures to structure-of-arrays, peeling and splitting of records, can lead to significant performance improvement.

  • Date : 17/09/2018
  • Place : Inria de Paris, 2 rue Simone Iff (ou: 41 rue du Charolais) Salle A115, bâtiment A
  • Guest(s) : Ramon Fernandez I Mir (Inria)

Yet, these transformations are error-prone and hard to debug. In this work, we aim at formalizing in Coq the correctness of such transformations.
To that end, we consider a C-like language with arrays, records, and pointers. We assign this language both a high-level semantics, where record fields are accessed by name, and a low-level semantics, based on low-level
pointers.

Ultimately, transformations could be defined as type-directed source-to-source translations. For the moment, to simplify the proof, we describe them as relations, and prove a forward simulation result. The talk
will give a tour of the language, the formalization of the transformations, and the theorems proved.

Keywords: Inria de Paris Data Formal Séminaire Gallium Transformations Layout Verification

Top