1 Search Results for "Kanabar, Hrutvik"


Document
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification

Authors: Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


Abstract
Machine-readable specifications for the Armv8 instruction set architecture have become publicly available as part of Arm’s release processes, providing an official and unambiguous source of truth for the semantics of Arm instructions. To date, compiler and machine code verification efforts have made use of unofficial theorem-proving-friendly specifications of Armv8, e.g. CakeML uses an L3-based specification. The validity of these verification efforts hinges upon their unofficial ISA specifications being valid with respect to the official Arm specification. Leveraging the Sail language ecosystem, we bridge this validation gap by formally verifying that an L3-based specification simulates the official Arm specification using the HOL4 interactive theorem prover. We exercise this simulation by proving a novel compiler correctness result for CakeML with respect to Arm’s official specification of the Armv8.6 A-class instruction set.

Cite as

Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen. Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{kanabar_et_al:LIPIcs.ITP.2022.20,
  author =	{Kanabar, Hrutvik and Fox, Anthony C. J. and Myreen, Magnus O.},
  title =	{{Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{20:1--20:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.20},
  URN =		{urn:nbn:de:0030-drops-167295},
  doi =		{10.4230/LIPIcs.ITP.2022.20},
  annote =	{Keywords: Compiler verification, ISA specification, HOL4, interactive theorem proving}
}
  • Refine by Author
  • 1 Fox, Anthony C. J.
  • 1 Kanabar, Hrutvik
  • 1 Myreen, Magnus O.

  • Refine by Classification
  • 1 Hardware → Theorem proving and SAT solving
  • 1 Software and its engineering → Domain specific languages
  • 1 Software and its engineering → Software verification

  • Refine by Keyword
  • 1 Compiler verification
  • 1 HOL4
  • 1 ISA specification
  • 1 interactive theorem proving

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail