why does compiling Coq snapshot need 96GB

[aa755]

I would like to get it to be less memory consuming. Do you already know where the bottlenecks are?

[aa755]

both for the compilation time and understandability, would it help to break down aarch64.v into smaller files? e.g. decoder, emulator, etc. It seems the contents of aarch64_mem.sail, aarch64_vector.sail, aarch64_decode.sail all go into aarch64.v. Can these be put into respective .v files?

[Alasdair]

I personally don't know where the bottlenecks are. I think what we do is build the model on a powerful compute server then transfer the results to an ordinary desktop/laptop. @bacam will likely know more

[bacam]

The biggest contributor is that our Coq translations attempt to capture the rich type information from the Sail model. However, the SMT proofs from the Sail type checking can't be reasonably reused, so the Sail Coq library has a tactic which attempts to construct similar proofs. Unfortunately this can be quite fragile and sometimes expensive, particularly when Coq's linear arithmetic solver is used in a context that it doesn't like. That said, more recent versions of the model tend to use much less memory, somewhere below 32GB. (I notice from your pull request that you're using Coq 8.11 - I think that changes the linear solver and I don't know what effect that will have on memory usage.)

Note that the memory consumption is just for building the model. After building it you can use it on another machine with much less memory as long as you use exactly the same build of OCaml and Coq. I've done some work with the Arm model on an old 8GB laptop in this way.

Another factor in the memory use is the size and structure of the decode functions. Currently it has a backtracking mechanism built in because there's something similar in Arm's specification and does make the decoder much larger and deeper than is strictly necessary. We'd like to make it simpler but haven't had the resources to do it yet.

One possible variation that may make a large difference is to drop the extra type information. This requires making versions of the library functions that are defined in badly-formed situations (e.g., bitvectors which appear to have negative lengths). The downside of doing this is that we would lose some of this detailed automatic information. However, from our experience with other proof assistants and our limited experience of working with the Coq model we suspect this may not be a major problem.

If you have some particular use for the model it would be helpful to know what kind of requirements you have so that we can bear them in mind during future Sail development.