Semantic reasoning about the sea of nodes

Delphine Demange 1 Yon Fernández de Retana 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The Sea of Nodes intermediate representation was introduced by Cliff Click in the mid 90s as an enhanced Static Single Assignment (SSA) form. It improves on the initial SSA form by relaxing the total order on instructions in basic blocks into explicit data and control dependencies. This makes programs more flexible to optimize. This graph-based representation is now used in many industrial-strength compilers, such as HotSpot or Graal. While the SSA form is now well understood from a semantic perspective – even formally verified optimizing compilers use it in their middle-end – very few semantic studies have been conducted about the Sea of Nodes. This paper presents a simple but rigorous formal semantics for a Sea of Nodes form. It comprises a denotational component to express data computation, and an operational component to express control flow. We then prove a fundamental , dominance-based semantic property on Sea of Nodes programs which determines the regions of the graph where the values of nodes are preserved. Finally, we apply our results to prove the semantic correctness of a redundant zero-check elimination optimization. All the necessary semantic properties have been mechanically verified in the Coq proof assistant.
Type de document :
Communication dans un congrès
CC 2018 - 27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. ACM Press, pp.163-173, 〈10.1145/3178372.3179503〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01723236
Contributeur : Yon Fernández de Retana <>
Soumis le : lundi 5 mars 2018 - 14:01:00
Dernière modification le : mercredi 16 mai 2018 - 11:24:14
Document(s) archivé(s) le : mercredi 6 juin 2018 - 15:36:32

Fichier

sea-of-nodes-hal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Delphine Demange, Yon Fernández de Retana, David Pichardie. Semantic reasoning about the sea of nodes. CC 2018 - 27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. ACM Press, pp.163-173, 〈10.1145/3178372.3179503〉. 〈hal-01723236〉

Partager

Métriques

Consultations de la notice

604

Téléchargements de fichiers

318