FunLoft reactive, concurrent programming language

in the department of yet-another-take-on-reining-in-concurrency-for-mere-mortals, the FunLoft programming language ("Functional Language over Fair Threads") from those braininacs at inria:

FunLoft is an experimental language for concurrent programming, designed with the following objectives:

* make concurrent programming simpler by providing a framework with a clear and sound semantics.
* provide a safe language, in which, for example, data-races are impossible.
* control the use of resources (CPU and memory); for example, memory leaks cannot occur in FunLoft programs, which always react in finite time.
* have an efficient implementation which can deal with large numbers of concurrent components.
* benefit from the real parallelism offered by multicore machines.

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

What's inefficient about shared memory?

"This tends to be expensive to set up, and the costs of communicating between address spaces are often high, even in the presence of shared memory segments." - their paper quoting someone else but agreeing with them, http://hal.inria.fr/inria-00184100/en/

I'm not aware of any overhead associated with reads and writes to shared memory segments on any modern OS. I can see there being a penalty on a processor without an MMU or an OS that chooses not to use it, like MS's Blowfish where type safety gives them enough confidence to turn it off, but certainly the baseline for production OS's nowadays is to assume an in use MMU.

I'm not aware of any

I'm not aware of any overhead associated with reads and writes to shared memory segments on any modern OS.

I believe the overhead they're referring to is the CPU cache coherency protocols. Writes get progressively more expensive the more cores are added.

Other Costs

If you're just talking about the reads and writes, then I agree with you. But we could be generous and interpret this as referring to other costs that come with 'communicating between address spaces'.

For example, if we cannot use atomic CAS and increment to do everything we'll need, we'll instead need OS-level mutexes rather than user-level critical sections. We may need named, shared event or file-handles if we wish to avoid polling. There may be coordination issues for when memory may be recycled; certainly, no modern GC crosses memory-space boundaries to handle relocatable shared spaces. Shared memory is often at a different address for different processes, which requires (at least for complex structures) that we use relocatable pointer idioms - offsets, for example. Unlike thread-based shared memory, we may need to explicitly serialize data into the shared memory segments.

What does 'cost of communicating' really entail? I'd personally include any synchronization and serialization issues at least. And set up costs can reasonably be measured for both performance and development.

Re: Sandro's statement: I agree that shared memory also costs us in terms of cache coherency. (Not just that; shared memory also hinders leveraging heterogeneous memory models such as GPUs.) But since the comparison was to threads in the same process, I think these issues apply either way.

You're right, I shouldn't

You're right, I shouldn't write in a hurry. The mention on address spaces is the key element: TLB flushes on x86 are notoriously expensive since x86 CPUs don't implement tagged TLBs. If you don't implement the "small spaces" optimization that EROS and L4 exploit (using segmentation), then you incur an expensive flush on every context switch. This is a pretty heavy cost compared to switching thread contexts which do not need a TLB flush.

Context Switching

I thought about mentioning costs of context switching above, but that issue does readily apply if you're doing a process per core. Since the focus of the paper was leveraging multi-core systems, I decided to avoid mentioning concerns about context switch, address space switch, and resulting TLB flush.

But I agree they may be relevant issues to whomever was speaking about overheads in the quote.

Did this part surprise anyone else?

As a bit of a language geek newbie, this sentence fragment really surprised me, but I haven't seen anyone else comment on it yet:

"memory leaks cannot occur in FunLoft programs, which always react in finite time"

The bit about data-races and memory leaks being statically checked for is fascinating too, but I just haven't been able to get over that Funloft can statically verify that its programs terminate in finite time!

I didn't know this was possible! Is this old news? Has it been done before?

Finite time, Finite Memory

It has been done before. Agda and Coq programs, for example, are also guaranteed to terminate.

Ensuring finite time and finite memory are very useful features, as is avoiding data races. I'm wondering if FunLoft might be a decent compilation target for embedded systems programming.

But you should understand that it means a restricted language - one that is not Turing complete.

Also, don't confuse 'finite' time with 'bounded' time much less 'real' time. Finite time might be a few seconds past the heat-death of the universe. Guaranteeing finite time protects against subtle programmer errors, but real-time is the property most engineers want.

Thanks

But you should understand that it means a restricted language - one that is not Turing complete.

Ah, so there's the trade-off.

Programming languages that aren't Turing complete can be at different 'levels' of Turing-incompleteness, is that right? What I mean is maybe language x has a larger set of types of problems it can't solve than language y does.

If that's correct, then where can/should I start if I want to try and get an idea of how Agda, Coq, Funloft, and others compare to each other in this respect?

Thanks for your help.

Also, don't confuse 'finite' time with 'bounded' time much less 'real' time. Finite time might be a few seconds past the heat-death of the universe."

Right, that's a good point. In my head I was mixing that up a bit.

Prior Art

Expressions in the simply typed lambda calculus are guaranteed to normalize in a finite number of steps.

Static typing would usually lead to strong termination guarantees except that most programming languages poke a hole in the type system to make the language Turing complete.

Interesting

most programming languages poke a hole in the type system to make the language Turing complete

That's an interesting way of looking at it. :) No doubt when I understand some amount of lambda calculus I will be able to see more clearly how programming languages have each poked a hole.

If it ain't broke, don't fix(point) it

I will be able to see more clearly how programming languages have each poked a hole.

It's all really the same hole, one way or another: Allow infinite loops or bottomless recursion.

The simplest sort of "Turing incomplete" language has no looping at all--older versions of SQL, for instance, which aside from the implicit iteration of working on entire data sets have no looping or recursion whatsoever.

Slightly more sophisticated languages might have fixed-size loops--iterating over the elements of an immutable container, for instance. Adding more power requires progressively more elaborate ways to ensure termination, eventually reaching a point where a program must essentially be accompanied by a formal proof of termination.

Or, just take the shortcut and add direct recursion (letting definitions refer to themselves), unrestricted iteration such as standard "while" loops, a fixed-point combinator as a language primitive, subvert the type system to allow otherwise "infinite" types, or whatever else is appropriate depending on what restrictions would otherwise prevent it in some language.