FunLoft stands for "Functional Language over Fair Threads". FairThreads is the basic model which has been implemented in several languages (C, Scheme, Java) and Loft is a language which implements FairThreads in C. Both FairThreads and Loft are very close to FunLoft, the main difference being that, by contrast with FunLoft, they do not address the issue of safety nor the issue of resource control.

The language is functional: functions are definable to produce new values from existing ones. FunLoft is first-order (as opposed to higher-order languages like ML): functions cannot be passed as parameters nor returned as result of a function. However, FunLoft is not purely functional (like Haskell, for example) as one has references in it, like in ML. Data with dynamically changing size in memory (like lists) are definable through inductive types. Recursive functions are used to manipulate such data. In FunLoft, these functions are proved to always terminate.

FunLoft is a thread-based concurrent language. Two levels of threads are available: fair threads linked to the same scheduler are run cooperatively; unlinked threads (not linked to any scheduler) are run preemptively, under the control of the operating system only. Threads can dynamically unlink from one scheduler and link to another one, or temporarily stay unlinked.

FunLoft is safe. In particular, a static analysis ensures that programs are free from data-races and from memory leaks. More specifically, there always exists a bound on the memory used by any program: if the available memory is larger than the bound, no out-of-memory error can occur. The system does not compute the actual value of the bound, but only test for its existence.

For resource control purposes, one has to detect the termination of functions manipulating data structures of inductive types, and control the size of the system. Detection of termination uses techniques from the area of rewriting terms. At the present moment, these techniques, in conjunction with resource control, do not support higher-order functions.

The Synchronous-pi-calculus can be seen as the purely functional basic model on which FunLoft is based. It is a variant of the pi-calculus in which processes are synchronous and the one-to-one communication through channels is replaced by a many-to-many communication based on broadcast events. The standard approach developed around the pi-calculus (mainly the notion of bisimulation) has been transposed in the new setting provided by the Synchronous-pi-calculus.

FunLoft is based on the FairThreads model which originated from reactive programming. However, it is the first attempt to consider both safety and resource control in this framework. In FunLoft, programs are proved to be reactive (that is, to terminate within each instant), which was not the case with previous reactive formalisms.

The syntax of FunLoft is inspired from ML, and it uses type inference as ML does. However, ML is higher-order and uses standard preemptive threads for concurrency. Present implementations of ML (OCAML) do not benefit from multicore architectures, as opposed to FunLoft.

Programs which need unbounded memory cannot be coded in FunLoft. This is for example the case of the well-known stream-based version of the Eratosthenes sieve to produce the infinite list of prime numbers. Programs which need to store in references data of unbounded size are also not definable. An example of such program is one that accumulates inputs and starts processing them only when a dynamic condition is met.

To let a single application benefit from multicores, one needs to use several schedulers and/or unlinked threads, each of them being mapped onto a system thread. Execution is of course optimal when the system threads do not communicate at all. Simulation examples show that one can also benefit from multicores in the presence of communication.

Yes and no. The present implementation basically translates FunLoft programs in C through Loft and the FairThreads in C library. This library is the result of several years of efforts to make reactive programming efficient. In particular, it can deal with very large numbers of concurrent entities. From this point of view, the FunLoft implementation can certainly be considered as extremely efficient. However, the implementation of values is not optimised at all in the present implementation.

Immediate termination is tested for first-order recursively defined functions having parameters of inductive type. Global termination of instants is also tested for functions that do not immediately terminate (these functions are called modules and only terminal resursion is allowed for them). Note that termination detection of functions is independent of the actual values of references. Thus, termination detection can be locally computed, even in concurrent contexts.

There exists formally proved results on resource control in the Synchronous-pi-calculus. Formally proved results also exist on absence of data-races in PACT which is a formalism very close to FunLoft. However, FunLoft includes several features that are not included by any of the two formal models (for example, the join primitive, and the possibility to synchronise schedulers). Thus, the conservative answer is that no property of FunLoft is formally proved. But an alternative optimistic answer would be that FunLoft has a formally stated basis. Let us say that we leave it to the reader to choose between these two answers...

All is experimental in FunLoft!