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



On 15 Feb 2018, at 08:45, Makarius <makarius at sketis.net<mailto:makarius at sketis.net>> wrote:

On 14/02/18 22:12, Gerwin.Klein at data61.csiro.au<mailto:Gerwin.Klein at data61.csiro.au> wrote:

It is presently unclear to me, where the scalability features are used
in practice. If L4.verified no longer requires that, we can probably
remove 80% of the record package and then update it easily. If scalable
records are still required, it will need more work to update.

Can some Data61 people say more about their current applications of the
record package?

We still do require it, and in fact make more use of the scalability than ever, because seL4 keeps growing and we keep adding support for further architectures.

We also depend on extensibility of records in a few places.

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



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