Slowdown of AFP/SC_DOM_Components due to changes in "code-only operations"
Makarius
makarius at sketis.net
Sat Jul 26 18:11:29 CEST 2025
Here is a notable slowdown of SC_DOM_Components from some months ago:
AFP/42327343c286. "hg bisect" in the interval of Isabelle/b69e4da2604b ..
32dd31062eaa says:
The first bad revision is:
changeset: 82692:8f0b2daa7eaa
user: haftmann
date: Thu Jun 12 08:03:05 2025 +0200
summary: reorganized more code-only operations
Here are the timings on my local machine, before and after that change:
Finished HOL (0:01:51 elapsed time, 0:05:49 cpu time, factor 3.14)
Finished HOL-Library (0:01:21 elapsed time, 0:05:50 cpu time, factor 4.33)
Finished Core_SC_DOM (0:01:17 elapsed time, 0:04:43 cpu time, factor 3.63)
Finished Shadow_SC_DOM (0:03:24 elapsed time, 0:13:24 cpu time, factor 3.94)
Finished SC_DOM_Components (0:01:54 elapsed time, 0:09:45 cpu time, factor 5.11)
Finished HOL (0:01:49 elapsed time, 0:05:42 cpu time, factor 3.12)
Finished HOL-Library (0:01:21 elapsed time, 0:05:51 cpu time, factor 4.31)
Finished Core_SC_DOM (0:01:17 elapsed time, 0:04:39 cpu time, factor 3.62)
Finished Shadow_SC_DOM (0:03:22 elapsed time, 0:13:10 cpu time, factor 3.90)
Finished SC_DOM_Components (0:05:45 elapsed time, 0:14:29 cpu time, factor 2.52)
That also demonstrates my "cheap midrange workstation" from some months ago,
with AMD Ryzen 9 7950X 16-Core Processor at almost 5.8 GHz. Only 8 threads
have been used above.
Makarius
More information about the isabelle-dev
mailing list