My email about PolyML and memory usage has generated some discussion,
perhaps I
should give some more context.
The L4.verified project has been stuck at Isabelle-2009-2 for years. Our
proofs
seem to be compatible with newer Isabelle versions, but we're running out of
(virtual) memory. We've been running PolyML in 32 bit mode on most of our
machines. As images grow beyond 4GB, we must switch to 64 bit mode, which
roughly doubles memory use to 8GB, which means replacing most of our
laptops.
Soon 16GB will be standard, I suppose.
In the meanwhile I've been having a look at Isabelle memory use. I've never
really understood why Isabelle images consume gigabytes of memory. With full
proofs off, the only real inputs should be the statements of hypotheses
and the
definitions of types and terms. Isabelle's output is many orders of
magnitude
bigger than these inputs.
The initial thought was that the record package would be representative. The
HOL image has grown because it has more in it, but the theorems generated in
defining a large record stay roughly constant. In addition, the L4.verified
proofs require a large record. I attach a graph of the memory cost of
defining
a 400-element record at various dates in Isabelle's development history. To
quote a Dilbert-like comic I read This graph clearly demonstrates up-ness.
The cost of defining the record has nearly tripled in this time.
We've had a look at some of the bigger spikes in this graph, and learned
very
little of use. What is clear is that nothing is constant: the record package
has been moved from the Typecopy package to the Typedef package, which
itself
has been growing in complexity, and throughout this time Florian has been
adding new hidden constants to the record package for code generation and
quickcheck. The record package uses multiple typedefs to simplify the
types of
some terms. In 2009-2 a typedef caused a theory to be checkpointed 8
times, in
2011-2 30 times.
This gives us a large collection of hypotheses, all of which are tedious to
investigate. Please appreciate how valuable empirical data from PolyML
is. Up
until now we've been poking at these issues in the dark.
One point of reference is that disabling the code generation and random
extensions saves us about 30% memory consumption, (roughly doubling over
2009-2 rather than tripling) which may be a sufficient stop-gap measure.
To address Andreas' concern: this is memory usage *after* finishing a theory
and garbage collection. If you're writing tactics, don't worry about it too
much. We don't have a problem with individual proofs exhauting memory and we
aren't using full proofs. I anticipate anyone using full proofs will do
so on a
machine with lots of memory.
Term sharing might be important for terms that are expected to end up at
global
scope, e.g. statements of theorems or terms stored in various kinds of Table
for internal use. In addition, it will only matter if these terms are really
big or produced very often. The last line in the HOL statistics line was 13
million words worth of type substitutions. I guess the interesting
question is
what terms are so large or being substituted so often.
The reason I'm sending these emails rather than proposing a patch is
that I've
got lost trying to figure out which functions matter and which don't. I
still
don't have any clear ideas.
Yours,
Thomas.
p.s. I attach the source of the graph as well. The columns are patch
date, patch ID (hg name) and heap size in bytes. The date here is given
in UNIX time for obscure reasons, gnuplot can read it with timefmt '%s'.
1282234761 004c35739d75 1342966296
1286379486 03174b2d075c 1330457808
1272362827 05209b869a6b 675239544
1269797642 095b1022e2ae 674991120
1286200717 0b8e19f588a4 1345002528
1271923982 0e24322474a4 806056288
1282722294 0e2596019119 1571638920
1285941925 10097e0a9dbd 1330533320
1283528624 12f3788be67b 134298
1286273097 132b79985660 1330457808
1283769525 14b16b380ca1 1571891264
1282806720 14c1085dec02 1425028072
1286267450 186a3b447e0b 1573254616
1278073397 19e8b730ddeb 1083742016
1284468473 1c4e38d635e1 1425157096
1269876649 1cd962a0b1a6 675207160
1277803530 1e99d8fc3d07 1326509472
1284300363 1f8131a7bcb9 1572107824
1282675008 20d82e98bcd7 1287225584
1282673370 20ff5600bd15 1569698432
1271862386 25e69e93954d 675437416
1269722068 26e820d27e0a 674980176
1289297835 27c1a1c82eba 1573443056
1284370555 27fae73fe769 1425167920
1285945609 2ffe7060ca75 1330538584
1286267291 317010af8972 1573254616
1288344928 323f7aad54b0 1573149976
1275474522 32b3d16b04f6 1266729032
1275383931 32c5251f78cd 675426536
1276866201 3489cea0e0e9 1326002400
1273626418 34dc65df7014 675258432
1275324572 3625d37a0079 675426536
1269711791 380b97496734 675066320
1282653389 38a926e033ad 1287225584
1278024058 40424fc83cc1 1073960320
1278084464 411717732710 1083742016
1284317267 44e4d8dfd6bf 1336187208
1282593352 458d6b12 1287225584
1290609215
