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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and