Re: [isabelle] Word32/64 ?



On Fri, 5 Feb 2010, Michael Norrish wrote:

On 05/02/10 08:40, Makarius wrote:
On Wed, 27 Jan 2010, Rafal Kolanski wrote:

One approach for high-performance code seems to be going in reverse,
i.e. parsing annotated SML/C/Haskell/whatever into Isabelle, where you
can pick your own translation, but have to pay by having to specify
the semantics also.

BTW, "high-performance" in SML (as implemented in Poly/ML) means to use
the default int, i.e. the proper mathematical (unbounded) integers, not
machine words. Poly/ML optimizes the representation of values for the
demands of symbolic computation, not for bare metal operations. So
proper ints, lists (cons cells), datatypes are fast, but Word32 is
really slow.

But then, if you are emitting SML, and really wanting speed, you'll probably compile with MLton; at least until you can emit code to exploit Poly/ML threads. MLton uses the gmp library to implement its IntInf structure, so if you target that explicitly, you will get infinite integers. Otherwise, you will get native machine integers.

In the "long" form Poly/ML integers are definitely slower than anything more modern out there (even Java BigInt which appears to be pure Java). But the nice thing about the default int type in Poly/ML is that you get almost full speed machine arithmetic until you degrade gracefully to the long form. This works, because 1 or 2 bits are sacrificed for tagging of values.

So the reason why Word32 is slow (it needs to be boxed) is the same reason why proper int is fast (a machine word can be either a "short" int, or a boxed "long" one).

While this tagging business appears to be ancient LISP technology, nobody appears to be using it in the C-derived universe (including Java). This is one of the reasons why there is now so much opportunity to do verification involving unsafe word arithmetic as we all know ...


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.