F* Challenge or The Tale of Tails

[ 2 ] Comments

[This blog was moved here]

F* is a verification-oriented programming language developed at Microsoft Research. If you already know F#, or OCaml, or Haskell, or another language from ML family, you’ll find it familiar.

Resources

To start experimenting with the language on your machine you need .NET 4.0. With Windows that’s it – just start enjoying verifications. But things are getting more interesting if you’re a mono user, when you want to compile the “right” compiler with blackjack and everything.

F* Download includes the sources and some binaries to bootstrap the compiler.

There is a dependency on Z3, we need F# PowerPack libs, fslex, fsyacc and i386 version of dylib for Mac and mono version of Microsoft.Z3.dll library (either compile a new one or download here or here).

But first of all, need to admit it works only for the small programs now. That’s why I ain’t gonna list the steps now. They are actually quite straightforward – update the paths 1 and fix the errors if any (e.g. I replaced the reserved word “const” with “cnst”). You can also define MONO symbol and add references to z3mono.dll.

The first wall is Certify.dll rule – got StackOverflow here. Given the .dll which is in bin folder by default, everything else compiles, including fstar.exe.

At this point only the simplest programs can be successfully verified. Why only them?

F* relies on tail call optimizations – lots and lots of recursive functions here. Consider the following simple function, it does nothing usefull but illustrates the problem:

 1: let rec f x cont =
 2:     if x < 0 then 0
 3:     elif x = 0 then cont x
 4:     else f (x-1) (fun x -> f x cont)
 5: 
 6: f 250000 id //SOF# Web Snippets

val f : int -> (int -> int) -> int

Full name: Test.f

val x : int

type: int
implements: System.IComparable
implements: System.IFormattable
implements: System.IConvertible
implements: System.IComparable<int>
implements: System.IEquatable<int>
inherits: System.ValueType

val cont : (int -> int)

val id : ‘T -> ‘T

Full name: Microsoft.FSharp.Core.Operators.id

We can verify that the .tail instructions are where expected:

 1: .method public static 
 2:   int32 f (int32 x,
 3: 	 class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32> cont
 4: 	 ) cil managed	
 5: {	
 6:  .custom instance void [FSharp.Core]Microsoft.FSharp.Core
	.CompilationArgumentCountsAttribute::.ctor(int32[]) = (
 7: 		01 00 02 00 00 00 01 00 00 00 01 00 00 00 00 00
 8: 	)
 9: 	// Method begins at RVA 0x2050
10: 	// Code size 35 (0x23)
11: 	.maxstack 8
12: 	// loop start
13: 	 IL_0000: nop
14: 	 IL_0001: ldarg.0
15: 	 IL_0002: ldc.i4.0
16: 	 IL_0003: bge.s IL_0007
17:   
18: 	 IL_0005: ldc.i4.0
19: 	 IL_0006: ret
20:   
21: 	 IL_0007: ldarg.0
22: 	 IL_0008: brtrue.s IL_0014
23:   
24: 	 IL_000a: ldarg.1
25: 	 IL_000b: ldarg.0
26: 	 IL_000c: tail.  // cont x
27: 	 IL_000e: callvirt instance !1 class 
           [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>::Invoke(!0)                                                                  
28: 	 IL_0013: ret
29:   
30: 	 IL_0014: ldarg.0
31: 	 IL_0015: ldc.i4.1
32: 	 IL_0016: sub
33: 	 IL_0017: ldarg.1
34: 	 IL_0018: newobj instance void Tailcalls/f@4::.ctor(
           class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>) 
35: 	 IL_001d: starg.s cont
36: 	 IL_001f: starg.s x
37: 	 IL_0021: br.s IL_0000
38: 	 // end loop
39: }  // end of method Tailcalls::f
 1: .method public strict virtual 
 2: instance int32 Invoke (int32 x) cil managed 
 3: {
 4: 	// Method begins at RVA 0x2084
 5: 	// Code size 16 (0x10)
 6: 	.maxstack 8
 7: 
 8: 	IL_0000: nop
 9: 	IL_0001: ldarg.1
10: 	IL_0002: ldarg.0
11: 	IL_0003: ldfld class 
          [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32> Tailcalls/f@4::cont
12: 	IL_0008: tail.  // f x cont
13: 	IL_000a: call int32 Tailcalls::f(int32, 
          class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>)
14: 	IL_000f: ret
15: }  // end of method f@4::Invoke

Does it work? Well, for .NET the answer is yes. But on mono the continuation part makes the stack grow. Manipulations with stack size are not the solution, so the sources modification seems to be a way to go.

There’s an old issue with tail calls when called and caller functions have different number of parameters. I thought that can be the case, because of FSharpFunc Invoke/InvokeFast methods, and created a special type for arguments, so all functions had a single parameter. It isn’t.

I still believe it is possible to get F* working on mono 2. Hope to find some spare time to dig into the logic and check how it can be rewritten with a simpler recursion, just extremely busy right now ). I also shared some ideas with Nikhil Swamy from F* team – he experimented with mono builds too and definitely knows much better what can be done. That’s an interesting challenge and, of course, the fresh ideas are very welcome!

 

 

  1. it’s better to include the full paths – for example I usually happily forget that fsc on my machine means Fast Scala Compiler and waste the time trying to get why it rejects .fs files
  2. everything comes to electricity at the end, right? 😉
  • Mono is still horribly broken in terms in tail call support.

    • luajalla

      Well, to be fair it works for the most-used straightforward cases I needed before. But suddenly trolling scala devs with tco is not that fun anymore )
      And it’s frustrating that I don’t really understand the why part here as it goes somewhere to implementation details. Looking for a workaround seems to be the most realistic solution.