Fast Machine Words in Isabelle/HOL

被引：7

作者：

Lochbihler, Andreas ^{[1
]}

机构：

[1] Swiss Fed Inst Technol, Dept Comp Sci, Inst Informat Secur, Zurich, Switzerland

来源：

INTERACTIVE THEOREM PROVING, ITP 2018 | 2018年 / 10895卷

关键词：

PROOF; GENERATION;

D O I：

10.1007/978-3-319-94821-8_23

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：388 / 410

页数：23

共 52 条

[11]

Crow J., 2001, TECHNICAL REPORT

[12]

Dawson J., 2017, MACHINE WORDS ISABEL

[13] Isabelle Theories for Machine Words [J].

Dawson, Jeremy .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 250 (01) :55-70

[14]

Delaware B, 2015, ACM SIGPLAN NOTICES, V50, P689, DOI [10.1145/2676726.2677006, 10.1145/2775051.2677006]

[15] A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm [J].

Divason, Jose ;

Joosten, Sebastiaan ;

Thiemann, Rene ;

Yamada, Akihisa .

PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17, 2017, :17-29

[16]

Esparza Javier, 2013, Computer Aided Verification. 25th International Conference, CAV 2013. Proceedings. LNCS 8044, P463, DOI 10.1007/978-3-642-39799-8_31

[17]

Farzan A, 2004, LECT NOTES COMPUT SC, V3116, P132

[18]

Greve D., 2000, ADVAN FORM METHODS, P113

[19]

Haftmann F, 2007, LECT NOTES COMPUT SC, V4502, P160

[20]

Haftmann F, 2013, LECT NOTES COMPUT SC, V7998, P100, DOI 10.1007/978-3-642-39634-2_10

← 1 2 3 4 5 6 →