> > Szczerze mówiąc to co piszesz jest dla mnie zaskakujące.
> > Tzn. dla mnie słowo "precyzja" do tej pory miało zawsze
> > to samo znaczenie, niezależnie od kontekstu. Mógłbyś
> > spróbować jakoś wyeksplikować te różne znaczenia tego
> > słowa?
>
> Podajemy definicję sposobu wybierania owoców. Definicja
> jest precyzyjna, ponieważ zdefiniowany nią sposób,
> wybiera dokładnie jeden gatunek jabłek. Ale jednocześnie
> definicja nie jest precyzyjna, bo w ramach jednego
> gatunku wybiera jabłka duże i małe. Gdy ktoś skupi uwagę
> na rozmiarze jabłek, to dla niego definicja będzie
> nieprecyzyjna, bo nie wiadomo o jaki rozmiar chodzi.
> Gdy ktoś skupi się na gatunku, to uzna że jest bardzo
> precyzyjna.

Jeżeli ktoś skupi uwagę na rozmiarze jabłek, to będzie
potrzebował innej definicji, czy też innego kryterium.
Ale to nie znaczy, że wcześniejsza definicja jest
nieprecyzyjna -- ona po prostu nie dotyczy zagadnienia,
które daną osobę interesuje. Słowo "precyzja" jakoś tu
nie pasuje.

> > Przy okazji -- Twój dowód, że nie ma deadlocka, jest niepoprawny
> > również z innego względu, mianowicie takiego, że istnieją programy,
> > w których nie używa się semaforów, a w których mimo to nie występują
> > deadlocki.
> Nie rozumiem. Chyba chciałeś napisać "występują". Czy możesz podać jeden
> kontrprzykład w którym dojdzie do zakleszczenia, jeśli używam mojego
> sposobu, a syncthread traktujemy tak, jakby było objęte semaforami w
> podanej przeze mnie kolejności?

Nie. Celowo napisałem "nie występują". Jeżeli chcemy mieć dowód,
to chcemy, żeby był kompletny. Twoje twierdzenie jest takie:

"jeżeli w programie wszystkie wspólne zasoby są chronione semaforami,
i te semafory są zajmowane zawsze w tej samej kolejności, to w programie
nie dojdzie do deadlocka"

ja nie wnikam teraz w prawdziwość bądź fałszywość tego twierdzenia, choć
intuicyjnie mógłbym się z nim zgodzić (w każdym razie nie potrafię w tej
chwili wymyślić kontprzykładu, ale nie potrafię też wymyślić teraz sobie
rozumowania, które by tego twierdzenia dowodziło)

ja wypowiadam zaś tezę następującą: "mogą istnieć programy, których struktura
jest odmienna od tej, której dotyczy Twoje twierdzenie, a w których mimo
wszystko nie dojdzie do deadlocka"

z tego rozumowania ma wynikać, że predykat "w programie X nie wystąpią
nigdy deadlocki" nie jest równoważny predykatowi "w programie X wszystkie
wspólne zasoby są chronione odpowiednio używanymi semaforami".
A nas interesuje definicja tego pierwszego predykatu.

> > W ramach ciekawostki dopowiem, że Bell Labs stworzyło
> > język Promela i system SPIN do weryfikacji, czy w programie może
> > dojść do zakleszczeń (dowody w tym systemie nie mają jednak natury
> > syntaktycznej, tylko opierają się o konstruowanie modeli. W każdym
> > razie w tym systemie używa się własnie jednej z odmian logiki
> > temporalnej do formułowania twierdzeń o stanach systemu)
> Jak juz pisałem, nie wiem co to jest logika temporalna.

To raczej nie jest dobry powód do chwalenia się.
http://lmgtfy.com/?q=logika+temporalna

> > Być może Twoje twierdzenie rzeczywiście dałoby się uogólnić,
> > generalizując pojęcie semaforu, i w rezultacie uzyskać system
> > dowodzący, że w programie nie dojdzie nigdy do dead-locku,
> > jednak nie jestem pewien, czy ów dowód (albo system) byłby
> > z technicznego punktu widzenia nietrywialny
> Jakby wyglądał formalny dowód to nie mam pojęcia. Ja jakoś
> to sobie po prostu wyobrażam że nie dojdzie do deadlocka i
> w praktyce nigdy nie doszło. Dlatego tak bardzo zależy mi,
> abyś podał jeden kontrprzykład.

Jak napisałem, intuicyjnie Twoje przypuszczenie wydaje mi się
prawdziwe, ale też umiałbym sformułować dowodu.

> > ale trzeba by było jeszcze dopowiedzieć,
> > że owe wątki zapisują również dane do pamięci, bo dopiero wtedy zajdzie
> > potrzeba synchronizacji
> Już wyżej było o tym, nie chciało mi się powtarzać.

Zawsze staram się unikać zmiennych globalnych ;]