[MLton] Writing memory to disk ...

[Wesley W. Terpstra]

On May 24, 2006, at 2:56 PM, Henry Cejtin wrote:
> I would rather that it is in /tmp because on Debian /tmp is  
> automatically
> cleaned up but /var/tmp is not.

MLton does seem likely to delete it, judging from the surrounding  
code, so /var/tmp might be ok. Also, on debian /tmp is often tmpfs,  
which is backed by RAM/swap (but usually with a limit well under the  
available memory, like 200-500Mb).

I really dislike this approach in general. This definitely violates  
the 'least surprise' design principle. I also don't see the real  
benefit; it would only help you if you're riding the edge of the 32- 
bit address space. Is that extra bit of wriggle room really worth the  
potential side-effects that dumping 2Gb to disk without warning might  
cause? I bet a lot of programs break if /tmp is out of space. Also,  
MLton doesn't even confirm it wrote the whole core out. After  
reloading the core, who knows what the state is. Then too there's  
security concerns about what the MLton core might contain. Perhaps  
this memory should never touch disk, as it contains passwords!

I think this is just a bad idea.