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.