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
begin
repeat n do begin
res:=!res*!i;
i--
end;
!res
end
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);
cooperate
end
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
n:=S(!n);
cooperate;
n:=Z;
end
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 () =
loop
begin
thread m ();
cooperate
end
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
end
let module tree_processing () =
let t = ref L (0) in
loop
begin
t:=get_tree ();
join map_on_leaf (!t);
end
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.
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
begin
x:=y;
unlink y:=0;
end
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.
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;
v++;
cooperate;
end
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
loop
begin
generate e with Cons_list (0,head (!r));
get_all_values e in r;
end
By accepting it, one would cyclically store in the reference values with
increasing sizes, which is a memory leak.