Séminaire des équipes de recherche
Formal Verification of Data Layout Transformations
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
For information
- Date : 17/09/2018
- Time : 10:30
- Free entrance
See also
