Email Gateway (Aug 22 2022 at 16:47): Email Gateway (Aug 22 2022 at 16:47):From: Gerwin.Klein@data61.csiro.au
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
Email Gateway (Aug 22 2022 at 16:47):From: Makarius <makarius@sketis.net>
On 15/02/18 00:46, Gerwin.Klein@data61.csiro.au wrote:
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.
I now recall that Norbert Schirmer made the first major scalability
changes for the record package.
Earlier it was actually based on datatypes, since I did not want to
fiddle with typedefs manually, but that was very slow (as expected).
We could synthesise a manual definition that simulates this situation if it helps.
For the moment it is sufficient to get an idea about:
(1) typical number of record fields
(2) typical number of record extensions (i.e. the depth of the hierarchy)
Makarius
Email Gateway (Aug 22 2022 at 16:49):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Email Gateway (Aug 22 2022 at 16:50):From: Gerwin.Klein@data61.csiro.au
Tom has answered most of it already, the short version:
We could synthesise a manual definition that simulates this situation if it helps.
For the moment it is sufficient to get an idea about:
(1) typical number of record fields
700 to about 1000
(2) typical number of record extensions (i.e. the depth of the hierarchy)
The large records are not extended, but there are a few smaller ones. I don’t think we have more than a depth of 2 extensions anywhere.
Cheers,
Gerwin
Last updated: Apr 26 2024 at 01:06 UTC