Lambda the Ultimate

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.

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 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.

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.

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.

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.

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.

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.

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.