Fast Machine Words in Isabelle/HOL
| Autor: | Andreas Lochbihler |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Programming language
Computer science HOL 020207 software engineering 02 engineering and technology Term (logic) computer.software_genre TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Test case TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 020204 information systems 0202 electrical engineering electronic engineering information engineering Code (cryptography) Code generation Rewriting computer Word (computer architecture) Normalisation by evaluation |
| Zdroj: | Interactive Theorem Proving ISBN: 9783319948201 ITP |
| Popis: | Code generated from a verified formalisation typically runs faster when it uses machine words instead of a syntactic representation of integers. This paper presents a library for Isabelle/HOL that links the existing formalisation of words to the machine words that the four target languages of Isabelle/HOL’s code generator provide. Our design ensures that (i) Isabelle/HOL machine words can be mapped soundly and efficiently to all target languages despite the differences in the APIs; (ii) they can be used uniformly with the three evaluation engines in Isabelle/HOL, namely code generation, normalisation by evaluation, and term rewriting; and (iii) they blend in with the existing formalisations of machine words. Several large-scale formalisation projects use our library to speed up their generated code. To validate the unverified link between machine words in the logic and those in the target languages, we extended Isabelle/HOL with a general-purpose testing facility that compiles test cases expressed within Isabelle/HOL to the four target languages and runs them with the most common implementations of each language. When we applied this to our library of machine words, we discovered miscomputations in the 64-bit word library of one of the target-language implementations. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|