Re: [isabelle] [ExternalEmail] Proof of concept: BNF-based records



Thomas Bauereiß from Peter Sewell's group in Cambridge sent me his experience with the record package:

"I have not really had major problems with records so far. I'm currently working on the translation of specifications of Instruction Set Architectures of processors from a language called Sail to Isabelle (via Lem). The Sail language (https://github.com/rems-project/sail) supports user-defined record types, and the translation generates a few (e.g. for processor register state), but most of the records I've seen in the specs we have are rather small. There are just a few cases where the size becomes mildly annoying. For example, the record that we generate for the register state of the ARMv8 spec has ~120 fields, which takes ~20s to process on my machine, and we have another ISA spec (not public) where the register state record has ~300 fields, and this takes a few minutes to parse. I wouldn't say this is a major problem, though, as these record types do not change very often, so we can put them into a separate theory and build a heap image.

Our main concern at the moment is scalability, I would say. Whatever record package we use, it should be able to handle records with possibly hundreds of fields."

Tobias

On 15/02/2018 00:46, Gerwin.Klein at data61.csiro.au wrote:
No sure what happened to the quoting in my email client, sorry. This is the relevant part:


Can you point to the sources of a few such big record definitions?

They get produced by the C parser, e.g. at this call:

https://github.com/seL4/l4v/blob/3d225cde694ba60a/spec/cspec/X64/Kernel_C.thy#L78

The record becomes large, because Norbert's SIMPL framework expects one record field per local variable in the union of all functions of the program. The final state record is an extension of a default state record + these local variables.

We could synthesise a manual definition that simulates this situation if it helps.

Cheers,
Gerwin



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.