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, whichroughly 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 fullproofs 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.verifiedproofs 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 packagehas 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 andquickcheck. 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 toinvestigate. 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 wearen'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 13million 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
graph.pdf
Description: application/download-application-pdf
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
