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

[David Matthews]

On 28/01/2019 09:20, Bertram Felgenhauer wrote:

I've made sure that the machine is mostly idle; things will be much
different if several processes start competing for the ressources.

I intended to experiment with smaller numbers but have not yet done so.
On another, similar machine, --gcthreads=2 was just as fast as 6.



It is increasingle clear that the limiting factor is the bandwidth 
between main memory and the processors.  There needs to be sufficient 
parallelism to saturate this channel; more than that will not help and 
may well make things worse.


How many threads are needed to saturate the memory channel depends on 
the processor speed, the memory speed and the application so there's no 
single answer to this.  Garbage collection can be particularly bad. 
Each word in the live data is read in and if it is a pointer it is 
followed.  There's no reuse so caching doesn't help.


The idea behind developing the 32-bit value model for the 64-bit 
processor was that by reducing the size of an ML cell more cells could 
be transferred through the memory channel in a given time.  That seems 
to have been borne out by the results.


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

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

[Lawrence Paulson]

Last January 24, I moved Fpow into Main and introduced 
Library/Equipollence.thy. Hope you like it.

Larry

> On 26 Jan 2019, at 15:14, Andrei Popescu  wrote:
> 
> Sorry for my late reply. I agree it makes sense to move such basic operators 
> (and facts) into Main. The Ordinals and Cardinals development was "destined" 
> to this sort of exports from the very beginning.
> 
> Best wishes, 

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

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

[Bertram Felgenhauer]

Makarius wrote:
> There was indeed something odd with sharing: David Matthews has changed
> that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46).

I may give it another try later...

> > Hardware:
> >   i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD
> > 
> > Common build flags:
> >   ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2"
> > 
> > Configurations:
> >   polyml 5.7.1x86_64ML_OPTIONS="--maxheap 24G -H 500 
> > --gcthreads 6"
> >   polyml-a444f281ccec x86_64ML_OPTIONS="--maxheap 24G -H 500 
> > --gcthreads 6"
> 
> For this hardware I recommend threads=6.

In the sessions beyond HOL, I see a speedup from threads=12. The timings
are basically the same with threads=10, but I have not checked the full
range of possibilities.

I've made sure that the machine is mostly idle; things will be much
different if several processes start competing for the ressources.

Configurations:
  threads=6
  threads=10
  threads=12

Times:
  Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.12)
  Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)
  Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)
  
  Finished HOL (0:02:21 elapsed time, 0:07:47 cpu time, factor 3.30)
  Finished HOL (0:02:25 elapsed time, 0:08:56 cpu time, factor 3.68)
  Finished HOL (0:02:32 elapsed time, 0:09:46 cpu time, factor 3.84)
  
  Finished HOL-Lib (0:05:47 elapsed time, 0:25:18 cpu time, factor 4.37)
  Finished HOL-Lib (0:05:12 elapsed time, 0:32:29 cpu time, factor 6.24)
  Finished HOL-Lib (0:05:10 elapsed time, 0:35:32 cpu time, factor 6.88)
  
  Finished HOL-AFP (0:06:33 elapsed time, 0:27:55 cpu time, factor 4.26)
  Finished HOL-AFP (0:05:51 elapsed time, 0:34:10 cpu time, factor 5.83)
  Finished HOL-AFP (0:05:41 elapsed time, 0:35:44 cpu time, factor 6.28)
  
  Finished IsaFoR_1 (0:05:11 elapsed time, 0:22:30 cpu time, factor 4.34)
  Finished IsaFoR_1 (0:05:04 elapsed time, 0:27:15 cpu time, factor 5.38)
  Finished IsaFoR_1 (0:05:21 elapsed time, 0:29:58 cpu time, factor 5.59)
  
  Finished IsaFoR_2 (0:05:57 elapsed time, 0:21:49 cpu time, factor 3.66)
  Finished IsaFoR_2 (0:05:43 elapsed time, 0:26:24 cpu time, factor 4.61)
  Finished IsaFoR_2 (0:05:40 elapsed time, 0:27:39 cpu time, factor 4.87)
  
  Finished IsaFoR_3 (0:07:13 elapsed time, 0:31:05 cpu time, factor 4.30)
  Finished IsaFoR_3 (0:06:51 elapsed time, 0:40:15 cpu time, factor 5.87)
  Finished IsaFoR_3 (0:06:45 elapsed time, 0:43:32 cpu time, factor 6.45)
  
  Finished IsaFoR_4 (0:08:37 elapsed time, 0:24:58 cpu time, factor 2.90)
  Finished IsaFoR_4 (0:08:48 elapsed time, 0:27:08 cpu time, factor 3.08)
  Finished IsaFoR_4 (0:08:47 elapsed time, 0:27:52 cpu time, factor 3.17)
  
  Finished Code (0:08:04 elapsed time, 0:08:12 cpu time, factor 1.02)
  Finished Code (0:08:00 elapsed time, 0:08:08 cpu time, factor 1.02)
  Finished Code (0:07:59 elapsed time, 0:08:08 cpu time, factor 1.02)

> Moreover note that --gcthreads is automatically provided, if ML_OPTIONS
> does not say anything else.

I intended to experiment with smaller numbers but have not yet done so.
On another, similar machine, --gcthreads=2 was just as fast as 6.

Cheers,

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