[isabelle-dev] Multicore timings

Makarius makarius at sketis.net
Fri Jan 15 21:35:25 CET 2016


On Fri, 15 Jan 2016, Lawrence Paulson wrote:

> It’s almost a shame how years of work can be executed in minutes.

Lets say that's the struggle for survival of maintainers behind the scenes 
:-)  Both Intel/AMD contributed a little, but David Matthews also did a 
great job.

For the release, I routinely tried SML/NJ as well, but did not get very 
far.  For more than half of the sessions there is a fatal hit on the 
memory wall.  MicroJava still happens to work (lxbroy10 with AMD Opteron 
6176):

   Finished HOL-MicroJava (6:01:55 elapsed time, 6:00:49 cpu time, factor 0.99)
   Finished HOL-MicroJava (5:28:47 elapsed time, 5:28:02 cpu time, factor 0.99)


 	Makarius


More information about the isabelle-dev mailing list