Re: [isabelle] Creating ML data is slow. No sharing/caching?



On Tue, 28 Jul 2015, C. Diekmann wrote:

Doesn't ML use sharing or caching? I always assumed that, if I have expressions e1 and e2, then constructing "And e1 e2" would reuse the values e1 and e2 and this operation would be independent of the sizes of e1 and e2.

That is occasionally called "hash consing", but it would introduce a central (synchronized) place for construction data structures. Not very efficient in the multicore era ...

Even in ancient single-core times, this old idea did not became very popular, probably because most data is rather short-lived and it is better not to make such a fuss about its allocation.


The Poly/ML runtime-system has other means to organize long-time survivers on the heap efficiently, by re-introducing sharing on demand. You won't see that in such micro-benchmarks, though. In AFP/JinjaThreads you do see the CPU crunching a lot, to fit the resulting heap into the tiny 4 GB address space: the Monitor/Heap dockable in Isabelle/jEdit gives an impression of what is going on in the ML RTS.


	Makarius





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