On Thursday, April 2, 2015 at 2:13:08 PM UTC+2, g...@g...com wrote:
> > > 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,
Nie zgodzę się. Aby to pasował do powyższej sytuacji, to
będzie potrzebował dodatkowych wyjaśnień, że chodziło o
definicję gatunku jabłek, a nie rozmiaru :)

> 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"
Zgadza się.

>
> 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)
By trzeba chwilę się zastanowić, a tej chwili nie mam. Jaka
jest definicja deadlocka? Czy taka: do deadlocka dochodzi, gdy wątek
a otworzył semafor A, a wątek b semafor B i jednocześnie wątek a czeka
na semafor B, a wątek b czeka na semafor A? Jest poprawna czy nie?
Jeśli zawsze otwierają semafory w tej samej kolejności, to nie
może dojść do sytuacji, że jeden ma A i czeka na B, a drugi ma
B i czeka na A. Hmmm nie jestem pewny, ale to chyba jest dowód,
przynajmniej na takich definicjach.



> 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"
Mnie wystarczy w codziennej praktyce programistycznej wynikanie, nie
wiem czy muszę mieć równoważność. Zastanówmy się. Jeśli semafory
raz są w kolejności AB a drugi raz w BA i jeśli dwa różne wątki mogą
wykonać kod objęty tymi semaforami, to coś mi się zdaje, że, bez
gwarancji na czas wykonania kodu, może dojść 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.
Nie jestem pewny, ale nabieram przekonania, że nawet jest równoważny.
Oczywiście przy założeniu że nie ma gwarancji na czas wykonania i że kod
objęty semaforami w nieposortowanej kolejności jest wykonywany wielowątkowo.

>
> > > 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
Nie chwalę się :)

>
> > > 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.
Zacznijmy od definicji deadlocka, jeśli ta którą podałem jest
prawdziwa, to chyba mamy dowód.


> > > 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 ;]
;-)

Pozdrawiam