I observed about 10% performance improvements in HOL4, between 5.7.1 release (x86_64) and latest master with the --enable-compact32bit option.
—Chun > Il giorno 20 gen 2019, alle ore 19:17, David Matthews > <[email protected]> ha scritto: > > I've now merged a major piece of development work into GitHub master. This is > a variant of 64-bit mode that uses 32-bit values. It was triggered by the > observation that Isabelle often peformed better with the 32-bit version than > the 64-bit despite the 64-bit version allowing a much larger heap and having > more registers. It appears that Isabelle, at any rate, is limited more by > the bandwidth between the processors and main memory than by the processors > themselves. This may well be the result of the work on parallelising the > application and the garbage collector. > > In effect there are now three versions on the X86: native 64-bit, native > 32-bit and 32-bits on 64-bits. The new version can be built with the > --enable-compact32bit option to configure. It allows a heap size of up to > 16Gbytes by using 31-bit "object ids", essentially indexes into an array of > 8-byte cells. This heap contains only the data. Code, thread stacks and > other support structures are outside this. > > It has been extensively tested with Isabelle (thanks to Makarius) and seems > to perform better than either of the native address versions. I started the > development about a year ago; development of the final stages were supported > by Data61 and CSIRO through Gerwin Klein. > > I would be interested in feedback on this and also the native address > versions. Whether it well help other applications may depend on whether the > limitation is processor speed or memory bandwidth. It's likely that many > applications will continue to perform best with native addressing. > > The update also includes changes to the X86 code-generator that affect all > the variants. These changes improve the way boolean values and conditionals > are handled. There also other changes to the IO system. Garbage-collection > of streams has been removed and overlapped IO is now used on Windows which > should improve performance and responsiveness. There have been changes to the > handling of floating point and Real32 has been added. > > Let me have any feedback. > > Regards, > David > > _______________________________________________ > polyml mailing list > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
