[Haskell-cafe] MVar considered harmful
jo at durchholz.org
Wed Dec 26 07:33:23 UTC 2018
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
> This is my very personal interpretation of the Godel Theorem and pure
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.
More information about the Haskell-Cafe