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  1342900008
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 45eeee8d6b12  1287225584
1290609215 4725ed462387  1569823376
1282063315 484e483eb606  1084605184
1275407539 4a7fe945412d  1266747184
1284319463 4b632bb847a8  1336185720
1272349059 4cd87067791e  675194472
1271698875 4d425766a47f  675294216
1281361417 502251f34bdc  1084153976
1284466338 520ea38711e4  1425157096
1272285881 5518de23101d  797046128
1296408995 57181bb1dfe0  1568226712
1287274223 57e7f651fc70  1344911912
1272311108 5ab0f8859f9f  675189624
1277918762 5cbd5d5959f2  1073960320
1286175915 61aa00205a88  1569275952
1284471597 61f0d36840c5  1425157096
1286379861 626b1d360d42  1345002528
1282310976 62b414d8051c  1342966296
1284329429 651e5a3e8cfd  1573555472
1272015289 6767999e8f9a  806047624
1275407501 694aebcd602b  675514192
1259751847 6a973bd43949  638737856
1271965188 6b330b1fa0c0  675444552
1283853113 6ceb8d38bc9e  1571891264
1286218555 6e9aff5ee9b5  1569275952
1284323339 6f085332c7d3  1573531184
1275653756 715d25555ca6  1507037312
1285965876 721ba2c1a799  1569275952
1282702653 72fd257f4343  1571638920
1288349345 73ecbe2d432b  1573149976
1284719217 742435a3a992  1317728496
1284545795 7565c649e7dd  1440801352
1283778097 75849a560c09  1571891264
1278319659 764d57a3a28d  1083742016
1269711747 78674c6018ca  594966760
1286225109 78faa9b31202  1573254616
1282745635 79d3cbfb4730  1425028072
1272290884 7b92238454d6  675189624
1278519443 7bf3ec9e7b0c  1083772752
1275385061 7c59ab0a419b  675426536
1270997467 7fa17a225852  675216920
1276164513 842fff4c35ef  1361888736
1275903774 865ad5634ed8  1361888736
1275472397 87988eeed572  1266729032
1282738689 8915e3ce8655  1425028072
1282655274 89d3550d8e16  1287225584
1283724527 8a2fb4ce1f39  1287000912
1289035508 8adcdd2c5805  1572201960
1284485898 8e585c7d418a  1561887704
1275423557 8e8e5f9d1441  1266803128
1277485924 9118ce1d1750  1326381496
1284314145 92b50c8bb67b  1572090576
1282575009 94ed0f34aea2  1342942176
1275383620 95bfc649fe19  1573747904
1269722770 95e67639ac27  674991120
1279015520 96551d6b1414  1083760384
1288982840 96c37a685a13  1572201960
1286176126 97b8051033be  1569275952
1284474818 9cab71c20613  1561887704
1269722318 9cc3df9a606e  675066008
1288353782 a03e288d7902  1573149976
1284055753 a0c0698e56c0  1571162688
1275658887 a1807bf72f76  1266729032
1275485784 a1b0201584cd  1266847968
1283373105 a2d7be688ea1  1342937584
1288299573 a2dde53b15ef  1326055368
1282732018 a365f1fc5081  1425028072
1275222095 a4b2bb0dab08  675428144
1286365692 a62e01e9b22c  1460444752
1275663188 a7a150650d40  1507037312
1282655285 a99fc8d1da80  1569698432
1282653697 aaee86c0e237  1424944992
1288190431 aee7ef725330  1340162408
1277743627 b3f572839570  1073565936
1275400741 b3ff14122645  1266830488
1282319215 b40524b74f77  1342932248
1285523162 b4e0bddc9e4c  1287345056
1283772131 b4f18ac786fa  1571891264
1284639888 b505208f435d  1438991704
1284562051 b6a77cffc231  1438993416
1288874556 b6ed3364753d  1559668208
1275383589 b78f31ca4675  1573747904
1275471369 b79df37bbdc4  1266820832
1286196408 b85bfa89a387  1460444752
1285951749 b93f27358100  1292698920
1288302879 bb433b0668b8  1326055368
1282678803 bdcb23701448  1569698432
1286294971 bebf1ff2c468  1460444752
1282232512 befdd6833ec0  1342966296
1275656977 bf5d936bb985  1266729032
1288334684 c03fc7d3fa97  1326055368
1275407128 c0f36d44de33  675514192
1270046681 c240b2a5df90  675202976
1282232233 c5eae9fc1fa4  1084601656
1282748386 c7f5f0b7dc7f  1425028072
1269250708 c93bda4fdf15  595137536
1284500300 ca81b7ae543c  1561887704
1275383776 cafcc42bae77  1266859064
1283721381 ccb53edd59f0  1287000912
1275746915 cdba266f0383  1507051288
1277802892 d30930f58006  1073565936
1286379847 d42ddd7407ca  1330457808
1284651769 d7caf48c4676  1438991704
1271844708 d7d1d87276b7  675437416
1282728645 d81f4d84ce3b  1425028072
1271926496 d868b34d604c  806056288
1275387400 d94459cf7ea8  1266830488
1275324666 da728f9a68e8  675426536
1288788863 daaa0b236a3f  1559668208
1271859679 dbbf4d5d584d  675437416
1275321628 e01c1fe245cd  675426536
1269786591 e031755609cf  674991120
1275407520 e0940e692abb  675514192
1282719922 e2d58749194b  1569698432
1282748393 e5508a74b11f  1425028072
1272237820 e5c785c166b2  675278256
1282209967 e5eed57913d0  1084601656
1283805114 e790a5560834  1571891264
1276272305 e8c34222814b  1325832200
1284134005 e98a06145530  1570273040
1272299191 ebaa558fc698  675278256
1288881048 f16ce22f34d0  1559668208
1275658982 f1734f3e9105  1507037312
1274608501 f1a07303d992  677696840
1284311042 f1ae2493d93f  1572090576
1282678478 f1ba2ae8e58a  1287225584
1286269152 f3c4849868b8  1330458552
1286281180 f4d3e70ed3a8  1460444752
1272043599 f4d84d84a01a  675444552
1282232444 f5bbfc019937  1084601656
1284028080 f94c53d9b8fb  1571475512
1282817989 f9837065b5e8  1425028072
1288343241 f99ec71de82d  1573149976
1282727638 fb30a006384a  1571638920
1272566464 fb69c8cd27bd  675164608
1282672534 fcb0fe4c2f27  1569698432
1282727607 fcd56e6a04b9  1287225584
1275336520 ffd587207d5d  675426536

Attachment: graph.pdf
Description: application/download-application-pdf

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to