Semantic foundations for cost analysis of pipeline-optimized programs
Résumé
In this paper, we develop semantic foundations for precise cost analyses of programs running on architectures with multi-scalar pipelines and in-order execution with branch prediction. This model is then used to prove the correction of an automatic cost analysis we designed. The analysis is implemented and evaluated in an extant framework for high assurance cryptography. In this field, developers aggressively hand-optimize their code to take maximal advantage of micro-architectural features while looking for provable semantic guarantees.
Domaines
Langage de programmation [cs.PL]
Origine : Fichiers produits par l'(les) auteur(s)