[isabelle-dev] Poly/ML x86_64_32 available for testing

Tue Jan 22 12:27:03 CET 2019

On 19/01/2019 21:43, Makarius wrote:
> Thanks to great work by David Matthews, there is now an Isabelle
> component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be
> enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this:
> 
>   init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc"
> 
> It requires the usual "isabelle components -a" incantation afterwards.

Here are some performance measurements on the best hardware that I have
presently access to (not at TUM):

  Intel Xeon Gold 6148 CPU @ 2.40GHz
  20 CPU cores * 2 hyperthreads * 2 nodes
  64 GB memory
  SSD

Isabelle/2633e166136a + AFP/ba82c831e5c2
isabelle build -N -j2 -o threads=8

x86-linux --minheap 1500 --maxheap 3500
Finished HOL (0:02:36 elapsed time, 0:08:46 cpu time, factor 3.37)
Finished HOL (0:02:36 elapsed time, 0:08:46 cpu time, factor 3.37)
Finished HOL-Analysis (0:03:49 elapsed time, 0:21:11 cpu time, factor 5.55)
Finished HOL-Analysis (0:03:50 elapsed time, 0:21:19 cpu time, factor 5.55)
Finished HOL-Data_Structures (0:01:39 elapsed time, 0:11:30 cpu time,
factor 6.91)
Finished HOL-Data_Structures (0:01:43 elapsed time, 0:11:52 cpu time,
factor 6.87)
Finished HOL-Nominal (0:00:28 elapsed time, 0:01:07 cpu time, factor 2.34)
Finished HOL-Nominal (0:00:29 elapsed time, 0:01:08 cpu time, factor 2.33)
Finished HOL-Nominal-Examples (0:02:57 elapsed time, 0:14:11 cpu time,
factor 4.80)
Finished HOL-Nominal-Examples (0:03:09 elapsed time, 0:14:55 cpu time,
factor 4.73)
Finished HOL-Proofs (0:09:52 elapsed time, 0:23:45 cpu time, factor 2.41)
Finished HOL-Proofs (0:09:52 elapsed time, 0:24:04 cpu time, factor 2.44)

x86_64_32-linux --minheap 1500 --maxheap 3500
Finished HOL (0:02:32 elapsed time, 0:08:50 cpu time, factor 3.49)
Finished HOL (0:02:32 elapsed time, 0:08:50 cpu time, factor 3.48)
Finished HOL-Analysis (0:03:41 elapsed time, 0:20:56 cpu time, factor 5.67)
Finished HOL-Analysis (0:03:39 elapsed time, 0:20:50 cpu time, factor 5.70)
Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:33 cpu time,
factor 7.16)
Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:35 cpu time,
factor 7.20)
Finished HOL-Nominal (0:00:12 elapsed time, 0:00:24 cpu time, factor 2.07)
Finished HOL-Nominal (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.06)
Finished HOL-Nominal-Examples (0:02:53 elapsed time, 0:13:54 cpu time,
factor 4.82)
Finished HOL-Nominal-Examples (0:02:51 elapsed time, 0:13:51 cpu time,
factor 4.83)
Finished HOL-Proofs (0:09:55 elapsed time, 0:23:48 cpu time, factor 2.40)
Finished HOL-Proofs (0:09:48 elapsed time, 0:23:35 cpu time, factor 2.40)

x86_64_32-linux --minheap 3000 --maxheap 7000
Finished HOL (0:02:32 elapsed time, 0:08:53 cpu time, factor 3.50)
Finished HOL (0:02:32 elapsed time, 0:08:51 cpu time, factor 3.49)
Finished HOL-Analysis (0:03:26 elapsed time, 0:20:06 cpu time, factor 5.84)
Finished HOL-Analysis (0:03:45 elapsed time, 0:21:20 cpu time, factor 5.67)
Finished HOL-Data_Structures (0:01:35 elapsed time, 0:11:32 cpu time,
factor 7.26)
Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:36 cpu time,
factor 7.20)
Finished HOL-Nominal (0:00:12 elapsed time, 0:00:25 cpu time, factor 2.08)
Finished HOL-Nominal (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.10)
Finished HOL-Nominal-Examples (0:02:45 elapsed time, 0:13:26 cpu time,
factor 4.88)
Finished HOL-Nominal-Examples (0:02:45 elapsed time, 0:13:26 cpu time,
factor 4.87)
Finished HOL-Proofs (0:08:10 elapsed time, 0:19:17 cpu time, factor 2.36)
Finished HOL-Proofs (0:08:23 elapsed time, 0:19:13 cpu time, factor 2.29)

x86_64-linux --minheap 1500 --maxheap 7000
Finished HOL (0:02:48 elapsed time, 0:09:46 cpu time, factor 3.48)
Finished HOL (0:02:46 elapsed time, 0:09:34 cpu time, factor 3.45)
Finished HOL-Analysis (0:04:01 elapsed time, 0:22:39 cpu time, factor 5.64)
Finished HOL-Analysis (0:04:00 elapsed time, 0:22:27 cpu time, factor 5.60)
Finished HOL-Data_Structures (0:01:58 elapsed time, 0:12:49 cpu time,
factor 6.47)
Finished HOL-Data_Structures (0:01:58 elapsed time, 0:12:42 cpu time,
factor 6.46)
Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.05)
Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.04)
Finished HOL-Nominal-Examples (0:03:03 elapsed time, 0:14:39 cpu time,
factor 4.80)
Finished HOL-Nominal-Examples (0:02:58 elapsed time, 0:14:29 cpu time,
factor 4.88)
Finished HOL-Proofs (0:10:16 elapsed time, 0:25:24 cpu time, factor 2.47)
Finished HOL-Proofs (0:10:21 elapsed time, 0:25:35 cpu time, factor 2.47)

x86_64-linux --minheap 3000 --maxheap 14000
Finished HOL (0:02:44 elapsed time, 0:09:31 cpu time, factor 3.46)
Finished HOL (0:02:44 elapsed time, 0:09:31 cpu time, factor 3.47)
Finished HOL-Analysis (0:04:06 elapsed time, 0:22:40 cpu time, factor 5.51)
Finished HOL-Analysis (0:04:06 elapsed time, 0:22:54 cpu time, factor 5.57)
Finished HOL-Data_Structures (0:01:44 elapsed time, 0:12:28 cpu time,
factor 7.14)
Finished HOL-Data_Structures (0:01:43 elapsed time, 0:12:21 cpu time,
factor 7.14)
Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.03)
Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.04)
Finished HOL-Nominal-Examples (0:02:56 elapsed time, 0:14:18 cpu time,
factor 4.87)
Finished HOL-Nominal-Examples (0:02:56 elapsed time, 0:14:21 cpu time,
factor 4.88)
Finished HOL-Proofs (0:08:48 elapsed time, 0:20:31 cpu time, factor 2.33)
Finished HOL-Proofs (0:08:55 elapsed time, 0:20:43 cpu time, factor 2.32)

Interpretation of the data:

  * There is no penalty for x86_64_32 with its unusual heap indexing
model, instead of native addressing of x86.

  * x86_64_32 is slightly faster than x86 for the same heap size,
presumably due to the improved programming model of x86_64 and extra
memory outside the heap (virtual address space is not limited to 4 GB).

  * x86_64_32 is significantly faster than x86 (or x86_64) for
applications that require a lot of memory, such as HOL-Proofs above.

The latter is further supported by AFP "slow" sessions, especially
JinjaThreads:

x86_64_32-linux --minheap 3000 --maxheap 7000
Finished AODV (0:50:24 elapsed time, 5:08:27 cpu time, factor 6.12)
Finished AODV (0:48:47 elapsed time, 5:03:17 cpu time, factor 6.22)
Finished ConcurrentGC (0:33:45 elapsed time, 3:19:18 cpu time, factor 5.90)
Finished ConcurrentGC (0:35:55 elapsed time, 3:23:29 cpu time, factor 5.67)
Finished JinjaThreads (0:28:23 elapsed time, 2:35:52 cpu time, factor 5.49)
Finished JinjaThreads (0:34:08 elapsed time, 3:08:09 cpu time, factor 5.51)

x86_64_32-linux --minheap 3000 --maxheap 14000
Finished AODV (0:49:12 elapsed time, 5:05:57 cpu time, factor 6.22)
Finished AODV (0:49:23 elapsed time, 5:07:28 cpu time, factor 6.23)
Finished ConcurrentGC (0:36:08 elapsed time, 3:24:55 cpu time, factor 5.67)
Finished ConcurrentGC (0:34:21 elapsed time, 3:19:38 cpu time, factor 5.81)
Finished JinjaThreads (0:16:30 elapsed time, 1:38:22 cpu time, factor 5.96)
Finished JinjaThreads (0:16:31 elapsed time, 1:40:33 cpu time, factor 6.08)

x86_64-linux --minheap 3000 --maxheap 7000
Finished AODV (0:56:08 elapsed time, 5:28:05 cpu time, factor 5.84)
Finished AODV (0:58:24 elapsed time, 5:36:58 cpu time, factor 5.77)
Finished ConcurrentGC (0:43:40 elapsed time, 3:52:08 cpu time, factor 5.32)
Finished ConcurrentGC (0:42:53 elapsed time, 3:50:21 cpu time, factor 5.37)
Finished JinjaThreads (1:05:27 elapsed time, 5:37:53 cpu time, factor 5.16)
Finished JinjaThreads (1:16:26 elapsed time, 6:34:49 cpu time, factor 5.16)

x86_64-linux --minheap 3000 --maxheap 14000
Finished AODV (0:58:41 elapsed time, 5:27:48 cpu time, factor 5.59)
Finished AODV (0:55:00 elapsed time, 5:31:09 cpu time, factor 6.02)
Finished ConcurrentGC (0:40:42 elapsed time, 3:46:33 cpu time, factor 5.57)
Finished ConcurrentGC (0:41:58 elapsed time, 3:47:12 cpu time, factor 5.41)
Finished JinjaThreads (0:24:16 elapsed time, 2:11:52 cpu time, factor 5.43)
Finished JinjaThreads (0:28:04 elapsed time, 2:30:09 cpu time, factor 5.35)

	Makarius