On 16/02/16 00:54, Makarius wrote:
People at former NICTA now Data61 have started to reduce heap file sizes recently. So my questions go ultimately in the direction: What are typical heap sizes seen in these big L4.verified applications? How is the "before" and "after" situation?
I wasn't at the coalface of that work, so I'm not well placed to comment on it. My current attempts at reducing heap sizes may be inconsequential to others. The sizes of the heaps I see are typically around a few GBs at most, but I have many of them hosted on a small SSD in one of my machines so a factor of 4 compression is a giant productivity boost for me there. From what I understand, the most punishing L4.verified session is currently CRefine, which I have rarely had cause to build in recent times.
On 16/02/16 00:12, David Matthews wrote:
From a quick look at the code the main effect that child states have is that StateLoader::LoadFile needs to seek within the saved state file to get the name of the parent file. That has to be loaded before the child because the child may, almost certainly will, overwrite some of the parent data. That may affect how you compact the data. How well do the compression libraries cope with seeking within the file?
Admittedly this is not something I had thought to look for, and now that I do I note there are seeks performed during state *saving* as well where Poly/ML overwrites data at the start of the stream. A cursory glance at the LZO API makes it seem like a requirement to seek the stream may well be a deal breaker... Rafal Kolanski, can you comment any more on this?
WRT the trade offs between time and space in loading/saving, my brief experiments and others' advice strongly suggested to me that the time cost was negligible in relation to everything else going on in the system. However, it's difficult to quantify this in any meaningful way without an implementation on hand. I'm travelling right now and in and out of internet range, but I can put together something when I'm back that can serve as a drop-in replacement for you both and myself to try out our use cases. If no one has given a canonical answer one way or the other by then, this effort would also answer whether it is possible to seek these streams.