TY - GEN
T1 - Optimizing Prestate Copies in Runtime Verification of Function Postconditions
AU - Filliâtre, Jean Christophe
AU - Pascutto, Clément
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022/1/1
Y1 - 2022/1/1
N2 - 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.
AB - 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.
KW - Memory management
KW - OCaml
KW - Optimized code generation
KW - Runtime assertion checking
U2 - 10.1007/978-3-031-17196-3_5
DO - 10.1007/978-3-031-17196-3_5
M3 - Conference contribution
AN - SCOPUS:85140454630
SN - 9783031171956
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 85
EP - 104
BT - Runtime Verification - 22nd International Conference, RV 2022, Proceedings
A2 - Dang, Thao
A2 - Stolz, Volker
PB - Springer Science and Business Media Deutschland GmbH
T2 - 22nd International Conference on Runtime Verification, RV 2022
Y2 - 28 September 2022 through 30 September 2022
ER -