Sounds cool. Not a proper hash cons, but an approximation to it and clearly very powerful. Larry
On 8 Aug 2012, at 09:54, David Matthews wrote: > The garbage collector now includes a pass that looks for cells that have the > same contents and merges them using the principle that equality in ML cannot > distinguish between two pointers to the same cell or two cells with the same > contents. There has been a PolyML.shareCommonData function for a long time > that does this but that has always had to be called explicitly by the user. > It has also required quite a lot of extra memory. Currently, I understand > Isabelle uses it just before it saves the state to reduce the sizes of saved > state files. > > Some time ago Makarius wondered if it was possible to have this invoked as > part of the GC. I couldn't see how to do this especially without adding any > extra memory overhead but gradually I've been improving it. The heap sizing > code now fires off this pass when memory is particularly short since it costs > several times the cost of a normal GC. The latest improvement was to find a > way to merge deep structures (lists and trees) something that > PolyML.shareCommonData has always done but at the cost of the extra memory. > This made a dramatic difference to JinjaThreads. It appears that it creates > many equal data structures and merging these can reduce the live data size by > some 80%. > > Actually, one has to be careful when interpreting the parallelism figures. > Much of the time an ML application is memory-bound which means that using > more processors can make an improvement in overall run-time but the overall > CPU usage will grow. As far as I can tell, the time that a processor spends > waiting for memory counts as its CPU time unlike when it is waiting for IO. > > David > > On 08/08/2012 09:00, Lawrence Paulson wrote: >> I understand about the parallelism, but what has cut back on the memory >> consumption? >> Larry _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
