[Haskell-cafe] MVar considered harmful

[Joachim Durchholz]

Am 26.12.18 um 00:04 schrieb Станислав Черничкин:
> Ok, somewhere at deeper level it’s actually CAS/LL-SC, but one of the 
> threads should be able to HLT (privileged instruction). Otherwise 
> non-busy waiting would not be possible.

HLT stops the entire processor, including operating system. No way a 
user process should ever execute *that*.
What actually happens is that threads are simply not scheduled, with 
strongly implementation-dependent means of making them runnable again 
(some schedulers require that you state runnability upfront, in the form 
of a mutex, futex, semaphore, monitor, or whatever; others allow one 
thread to change the runnability of another thread post-hoc).

> Composability is not a point at all currently. I’m not after 
> composability I’m after completeness. Let me speculate a bit and presume 
> that any sufficiently complex composable system (i.e. such a system 
> which would hold some “correctness” properties over allowed composition 
> operations) will necessary be incomplete (i.e. some “correct” 
> expressions will be inexpressible due to the lack of compositions rules 
> and there is no way to supplement the system without making it 
> controversial).
> 
> This is my very personal interpretation of the Godel Theorem and pure 
> speculation,

The computer science equivalent of the Godel Theorem is 
"undecidability". That's well-trodden ground.

In practice, the options are:
1. Giving up correctness is not very useful. (There are extremely rare 
exceptions - be prepared to strongly defend any a suggestion of that kind.)
2. Giving up completeness can still be useful. You do not get true 
universality, but you get a correctness guarantee.
3. You can still have both correctness and completeness. If your 
heuristics are good, you'll get a result in the vast majority of cases 
in practice. The cases that don't work out will simply run into an 
endless loop; just add a timeout to the computation.
Obviously, you don't want such an approach for time-critical stuff like 
thread scheduling, but it's been used successfully e.g. for type systems 
that are more powerful than Hindley-Milner.
4. Do not solve the problem at all. E.g. don't prevent deadlocks by 
inspecting code and determining whether it can deadlock or not; detect 
deadlocks after they happen and report them as errors.

> but look, every non-Turing complete language will prohibit 
> correct programs, on the other hand, every Turing complete will allow 
> you to write non-terminating programs (contradictions). I believe, same 
> property holds with concurrency.

You get into undecidability issues at the point where an algorithm needs 
to analyze a program for termination.
So people have been using algorithms don't inspect programs, but which 
inspect data (Haskell's infinite data structures would be categorized as 
program in this discussion, because it's code that will return finite 
portions of the infinite data structure).
Even with finite data, algorithms can be undecidable. It's rare and 
usually doesn't happen, but it can happen if the data structure somehow 
expresses a Turing-complete language.

Note that compilers and such never actually analyze the full program, 
they just apply patterns that a programmer has decided preserve 
semantics. (Mistakes here usually lead to compiler bugs.)

 > If some system prohibits you from
> deadlocks, it will also prohibit you from some correct synchronization 
> strategies (once again, it’s my speculations, maybe there is a proof of 
> contrary, but I haven't found them yet).

Correct, but this is only a problem in practice if you need a locking 
scheme that can express undecidable locking strategies.
I am not a grand master of locking strategies, but I see locking 
strategies move from semaphores (undecidable) towards higher-level 
constructs that do not allow all kinds of locking anymore. I don't think 
that futures etc. exclude deadlocks by construction, but I do see that 
deadlocks have become a less common problem.

> Standing from this point, it’s worth to have some complete and 
> controversial (uncomposable) API at low level and having several 
> composable implementations over it with their restrictions.

That's one of today's difficult goals: Designing a locking API that's 
both composable and useful.
I'm not sure whether such a thing has even been thought of yet.