Optimizing Prestate Copies in Runtime Verification of Function Postconditions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Optimizing Prestate Copies in Runtime Verification of Function Postconditions

Résumé

In behavioural specifications of imperative languages, postconditions may refer to the prestate of the function, usually with an old operator. Therefore, code performing runtime verification has to record prestate values required to evaluate the postconditions, typically by copying part of the memory state, which causes severe verification overhead, both in memory and CPU time. In this paper, we consider the problem of efficiently capturing prestates in the context of Ortac, a runtime assertion checking tool for OCaml. Our contribution is a postcondition transformation that reduces the subset of the prestate to copy. We formalize this transformation, and we provide proof that it is sound and improves the performance of the instrumented programs. We illustrate the benefits of this approach with a maze generator. Our benchmarks show that unoptimized instrumentation is not practicable, while our transformation restores performances similar to the program without any runtime check.
Fichier principal
Vignette du fichier
main.pdf (379.62 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03690675 , version 1 (08-06-2022)
hal-03690675 , version 2 (13-10-2022)

Identifiants

  • HAL Id : hal-03690675 , version 2

Citer

Jean-Christophe Filliâtre, Clément Pascutto. Optimizing Prestate Copies in Runtime Verification of Function Postconditions. RV 2022 - 22nd International Conference on Runtime Verification, Sep 2022, Tbilisi, Georgia. ⟨hal-03690675v2⟩
151 Consultations
49 Téléchargements

Partager

Gmail Facebook X LinkedIn More