Floating point #79

Open
konrad-slind opened this Issue Sep 21, 2015 · 8 comments

Projects

None yet

5 participants

@konrad-slind

Please consider supporting floating point. The semantics should already be
in src/floating-point. From the compiler point of view, it should be merely a matter
of adding a new primitive type and some basic operations. Probably the SML
structure Real could be used as guidance.

@myreen
Contributor
myreen commented Sep 22, 2015

The real effort comes at the lower levels of the compiler and particularly the target architectures, both in terms of modelling and proof work. So this work lands mostly on Anthony and me.

We might start with support for floating-point only for certain target architectures. Or even: compile to software implementations of floating-point operations. In the long run, we'll of course want to use the real floating-point instructions from each target architecture.

@michael-roe

As Magnus says, writing the an model of the CPU's floating-point instructions is likely to be a moderate amount of work.

Our BERI soft core, which is compatible with the MIPS III ISA, has a floating point unit And we already have a test suite for the floating point instructions in the MIPS ISA. So we could experimentally test the correctness of an L3 model of the MIPS floating point ISA by running it against our test suite, and fuzz testing it against the BERI soft core. Doing that testing would be interesting/useful for other reasons (e.g. it might find some bugs in BERI's floating point implementation...) but it's not very high up on my priority list of things we need to do.

One of the issues we'll need to deal with is that the IEEE floating point standard contains a substantial amount of non-determinism, but the L3/CakeML system likes to have deterministic specifications. We do know how the BERI soft core behaves when the IEEE spec allows more than one possible value to be returned, so modelling "what BERI does" is an option,

@michael-roe

Anthony and I have just taken a look at what would need to be added to the L3 language to do this.
We'd need to add to L3: floating point division; conversion of ints to/from floats; a compare operation that knows the result can be "unordered"; and maybe more. The SML backend for L3 currently compiles all floating point operations to just raise an exception: the SML backend would need to be extended to actually do some floating point operations. That in turn raises the question of how complete is the underlying ML compiler's support for IEEE floating point. MLton, at least, seems to support both single precision and double precision IEEE floats.

@michael-roe

If floating point is added to the language, will we have problems with operator overloading? Especially as CakeML currently doesn't have type annotations.

e.g. fun add(x)(y) = x+y;
Is that "+" over the integers, single precision floats or double precision floats?
(In SML, it defaults to type int).

You could of course do something like this:
fun add(x)(y) = Real64.+(x)(y);

@xrchz
Member
xrchz commented Nov 11, 2015

I expect CakeML will not have overloading. What we might have is open (or at least open within local) which will make using floating point operators easier (since you can shadow the integer operators selectively). (We might also have type annotations some day, but they won't help this situation if there's no overloading.)

@konrad-slind

I use

fun foo args =
let open
val ...
in
....
end

quite a bit. Is that usage going to be supported?

Konrad.

On Wed, Nov 11, 2015 at 7:23 AM, Ramana Kumar notifications@github.com
wrote:

I expect CakeML will not have overloading. What we might have is open (or
at least open within local) which will make using floating point
operators easier (since you can shadow the integer operators selectively).
(We might also have type annotations some day, but they won't help this
situation if there's no overloading.)


Reply to this email directly or view it on GitHub
#79 (comment).

@xrchz
Member
xrchz commented Nov 12, 2015

When we do add support for open, I expect that usage to be included.

@acjf3
Contributor
acjf3 commented Nov 20, 2015

L3 now has support for "floating point division; conversion of ints to/from floats; a compare operation". So this should help when it comes to specifying floating-point for MIPS.

The ARMv6 model already has some floating-point stuff (supporting a smallish set of 32-bit and 64-bit operations). I may look into what's possible for x86 (where we have 80-bit floating-point registers).

@myreen myreen added a commit that referenced this issue Feb 22, 2017
@myreen myreen Get semantics dir to build #79 ce10aaa
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment