On 20/09/16 14:15, David Matthews wrote:
On 19/09/2016 21:15, Makarius wrote:
The handling of return addresses from functions has been simplified. A consequence of this is that when pieces of code are compiled they are stored in a separate area of memory rather than in the general heap and not garbage-collected.
Does that mean that run-time (re)compilation is a now potential memory leak?
I've heard that the JVM has only recently learned to do proper garbage collection of dynamically loaded modules.
Yes. I can't see a way round it at the moment. It would be difficult to produce an example where the only reference to the code of a function was through the return address but it could happen if a thread started to execute a function contained in a reference and then the reference was overwritten.
Currently, there is a leak because each top-level expression is compiled down to machine code even though the code is only executed once. My plan is to avoid that by interpreting the top-level rather than fully compiling it.
That reminds me a bit of OCaml.
I have always considered it one of the big assets of Poly/ML that fully native compilation can be performed at run-time, without any difference to off-line compiled code.
Just a few weeks ago, I explained that to an audience that only knew boring static compilation in the manner of cc.
My understanding of an LCF-style proof assistant is that compilation and execution of the program can happen continuously all the time: new code is added (to implement tools and packages), then new definitions and proofs are performed, this is repeated indefinitely.
This is also the deeper reason, why we could never use Mlton. (Another reason is that compilation needs to be fast, in order to be able to develop all these fine tools interactively.)
Since Isabelle manages the invocation of the Poly/ML compiler itself, we can probably easily cope with that either way: keeping full compilation or degrading to interpretation. Although, I would probably just keep compilation let memory fill up in regular applications: not so much code is loaded after the main HOL image is finished.
I do wonder how the classic LCF-style proof assistants would cope with that, notably ProofPower and HOL4.
Makarius