FFI call semantics

[ramsdell]

The FFI is supposed to be used with stateless C functions so as to ensure referential transparency. However, there is a use case in which one wants to use a stateful C routine to generate a sequence of random values by repeatedly calling the C function with a call of the same form. Here is an example.

Suppose you load the K&R rand function that is available on the net with:

foreign rand: () -> [64]

Currently, in the interpreter, if one types rand () repeatedly, one gets different values.

cryptol -b rand.bat
Loading module Cryptol
Loading module Cryptol
Loading module Main
Loading dynamic library rand.dylib
0x00000000000041c6
0x000000000000167e
0x0000000000002781
0x000000000000446b
0x000000000000794b
ramsdell@MM270114-PC ffi_rand % 

Where rand.bat is

:load rand.cry
rand ()
rand ()
rand ()
rand ()
rand ()

Are future versions of cryptol guaranteed to preserve this behavior?

[RyanGlScott]

What precisely do you mean when you say "this behavior"?

Do you mean "preserve the internal state of rand.dylib in between invocations of rand"? This might be possible to guarantee in a limited context, but it would be fragile, since we don't preserve the internal state between module reloads. That is, this script would print three different random numbers:

:load rand.cry
rand ()
rand ()
rand ()

$ ~/Software/cryptol-3.0.0/bin/cryptol -b script1.icry 
Loading module Cryptol
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
0x00000000000041c6
0x000000000000167e
0x0000000000002781

But this script would print the same number three times:

:load rand.cry
rand ()
:load rand.cry
rand ()
:load rand.cry
rand ()

$ ~/Software/cryptol-3.0.0/bin/cryptol -b script2.icry 
Loading module Cryptol
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
0x00000000000041c6
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
0x00000000000041c6
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
0x00000000000041c6

Even if we restrict ourselves to a single-module-load assumption, it would be tricky to make particular guarantees about the order in which multiple calls to rand are invoked. As a example to illustrate what I mean, note that these two commands will return different answers depending on how your machine schedules threads:

$ ~/Software/cryptol-3.0.0/bin/cryptol -c "parmap rand [(), (), (), (), (), (), (), ()]" rand.cry +RTS -N8 -RTS
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
[0x00000000000041c6, 0x000000000000167e, 0x00000000000015fb,
 0x0000000000001cfb, 0x000000000000446b, 0x00000000000059e2,
 0x0000000000002781, 0x000000000000794b]

$ ~/Software/cryptol-3.0.0/bin/cryptol -c "parmap rand [(), (), (), (), (), (), (), ()]" rand.cry +RTS -N8 -RTS
Loading module Cryptol
Loading module Bug
Loading dynamic library rand.so
[0x000000000000167e, 0x000000000000794b, 0x0000000000002781,
 0x00000000000041c6, 0x00000000000059e2, 0x000000000000446b,
 0x0000000000001cfb, 0x00000000000015fb]

This is a rather contrived example, but this issue could arise in more subtle ways. For instance, if you are lazily evaluating an infinite sequence, the order of evaluation might determine whether rand gets invoked in a certain order or not, and this could be difficult to predict.

This is all to say: I don't think we are planning to deliberately change the behavior of the Cryptol FFI to make something like a foreign rand declaration unusable, but anyone who wants to do this will need to take precautions so that they don't wind up with surprising results.

[ramsdell]

In a nutshell, should I choose to include C functions that are stateful, what I want to know is what semantics can I depend on into the future. You point out that the state is not preserved over module reloads. Good to know, and of course, it makes a lot of sense. Lack of commitment to evaluation order when calling stateful C functions also makes sense. In the case in which one is producing pseudo random numbers, it may be okay that there is no a commitment to an explicit order. If there is no parallelism, can a user depend on reproducibility? Finally, when there is parallelism, one obviously cannot depend on reproducibility. May a user depend on the fact that calls to C code are atomic? Inquiring minds want to know.

[yav]

My gut feeling is that one should not do this sort of thing. The way I decide what's a "good" FFI function is if the same function could be implemented in Cryptol in some way (no matter how inefficient). If yes, then it's good, otherwise questionable. Of course, nothing prevents one from using questionable functions, and that might work OK for a paritcular configuration (e.g., fixed version of Cryptol/hardware/compilers etc), but this is threading on thin ice.

Btw, if the persistent state is not large, one option would be to modify the C function to pass it around (e.g., the seed for the random number generator).

[ramsdell]

As a long time advocate of pure functional programming, this sort of thing is abhorrent to me too. But you know people are going to do this. The manual should let users know what they can depend on and emphasize the world of hurt they are entering into if they are not careful.

[RyanGlScott]

I agree that we should document the pitfalls of using impure functions in the FFI somewhere. I'm not sure if we want to guarantee anything about the behavior of impure FFI functions at this point, other than a generic "you are on your own" disclaimer.

[RyanGlScott]

I've submitted #1558 with a clarification to the reference manual.