Examples of Correct and Incorrect Programs
March 2007
This page contains small examples of FunLoft programs which are correct (accepted by the compiler), incorrect (rejected by the compiler for good reasons), or acceptable (rejected for compiler weakness reasons).

1 Termination of Functions

Let us consider the inductive type of naturals:
type nat = Z | S of nat
The recursive function that returns the integer value of a natural is:
let nat2int (n) =
   match n with Z -> 0 | S (m) -> 1 + nat2int (m) end
This function is proved to always terminate because in the recursive calls the size of the parameters always decreases.

Here is the example of an incorrect function, i.e. that cannot be proved to always terminate (actually, it does not):
let bad (n) =
   match n with Z -> 0 | S (m) -> bad (S (m)) end
If this function were accepted, a thread calling it and linked to a scheduler could never return the control, which would definitively prevent from running the other threads linked to the same scheduler.

In the present version of FunLoft, termination detection is performed only for parameters of inductive types. The following function is thus rejected, despite the fact that it always terminates:
let fact (n) =
  if n < 1 then 1 else n*fact (n-1)
Note that, however, the previous function can be coded using a repeat loop which is proved to terminate:
let fact (n) =
  let res = ref 1 in
  let count = ref n in
    repeat n do begin 

2 Accumulation in References

References are stratified: there should be an order on reference accesses and no cycle is allowed to appear on these. Here is an incorrect function that violates stratification:
let nat_increm (n) = n:=S(!n)
A memory leak could appear if the function were accepted, as in:
let module memory_leak () =
   let r = ref Z in
   loop begin
     nat_increm (r);
Only inductive types are concerned by stratification; the following function is thus correct:
let int_increm (i) = i:=!i+1
The following module is rejected despite the fact that the reference is reset at each instant, which actually prevents from memory leak:
let module m (n) =
 loop begin 

3 Thread Creation

Thread creation has to be controlled, in order to preserve reactivity. For example, in the following code, the number of running threads is forever increasing:
let module m () = loop cooperate

let module too_much_threads () = 
        thread m ();
Such a program has a memory leak, as the active threads never terminate (and thus cannot be collected) and therefore have to be stored somewhere. As the number of cycles that has to be performed at each instant cannot be bound, the system is not reactive.

Threads can be safely created cyclically at a given point in a loop when it can be proved that the threads previously created at that point are terminated before passing that point; these points correspond to the join primitive. For example, consider:
type tree = L of int | T of tree * tree

let map_on_leaf (t) =
   match t with L (n) -> thread leaf_processing (n) 
          | T (t1,t2) -> 
             begin map_on_leaf (t1); map_on_leaf (t2); end

let module tree_processing () = 
  let t = ref L (0) in
        t:=get_tree ();
        join map_on_leaf (!t);
In this example, the loop stays bloqued on the join instruction until all the threads created for processing the leaves are terminated. At each cycle, the number of created threads depends on the number of leaves of the tree t. However, as the size of t is bounded, this number is also bounded, like is the number of active threads in the system.

4 Data Races

A reference accessed by a thread while unlinked is private to the thread and thus should not be accessible by another thread (either linked or unlinked):
let module data_race (r) = unlink r:=1
In this code, the parameter r should be public, because it is given initially to the thread; but, it should be private because it is accessed by the thread while unlinked. The system detects the contradiction and reject the program.

No reference should be shared by two distinct schedulers (either synchronised or not):
let module access1 () = link s1 do r:=1
let module access2 () = link s2 do r:=2
In this code, the reference r is public because it is global; but it should belong to both schedulers, which is rejected.

For data-race avoidance, arrays are considered as if they were one unique reference; thus the following code is rejected, despite the fact that no data-race actually occurs:
let s1 = scheduler
let s2 = scheduler
let array = ref [2] 0
let module first () = link s1 do array[0]:=1
let module second () = link s2 do array[1]:=2
The type system is not able to detect disjointness of the parts of the array accessed by the two modules. Note that the program is also rejected if the two schedulers are synchronised.

Private references should not be embedded in public ones, as otherwise other threads could access them, like in:
let x = ref ref 0

let module m () = 
   let y = ref 0 in
         unlink y:=0;
Reference y is private as it is accessed while unlinked, but it is also embedded in x which is global, thus public. Thus, the program is incorrect.

5 Events

In FunLoft, an event is associated to one unique scheduler, or to an area of synchronised schedulers. There should be impossible to remotely generate events when schedulers are not synchronised:
let s1 = scheduler
let s2 = scheduler
let e = event

let module wait () = link s1 do await e

let module gen () =
  let v = ref 0 in 
    link s2 do 
       loop begin 
          generate e with v; 
Indeed, the number of generations to be stored is not bounded (it actually depends on the relative speed of the two schedulers) which produces a memory leak.

However, use of events becomes possible between synchronised schedulers because they share the same instants:
let s1 = scheduler
and s2 = scheduler
let e = event
let module wait () = link s1 do await e
let module gen () = link s2 do generate e
There should be no way for an event to be generated cyclically during the same instant, as in:
let module cycle (e) =
   for_all_values e with v -> generate e with v+1
The way to avoid this kind of problem is rather rough: no event should be generated during evaluation of the callback expression of a for_all_values instruction.

Events also participate to stratification. For example, the following module is rejected as it violates stratification:
let head (l) =
  match l with Nil_list -> Nil_list | Cons_list (a,m) -> a end

let module m (e) =
  let r = ref Nil_list in
           generate e with Cons_list (0,head (!r));
           get_all_values e in r;
By accepting it, one would cyclically store in the reference values with increasing sizes, which is a memory leak.

This Html page has been produced by Skribe.
Last update Wed Apr 4 15:53:19 2007.