W dniu czwartek, 2 kwietnia 2015 08:14:46 UTC+2 użytkownik M.M. napisał:

> > > > Nie mam aż tyle czasu, myślalem że rzucisz kilka zalet.
> > > Zalet synchronizacji wątków przed dostępem do pamięci?
> >
> > Tak sobie myślę, że chyba niezbyt ładnie się zachowałem,
> Podając linki do literatury? To akurat bardzo w porządku.

Raczej miałem na myśli ton, w jakim zadałem powyższe pytanie.
Strasznie mnie smuci to, że dyskusje na tej grupie są często
mało merytoryczne i sprowadzają się do udowadniania sobie
nawzajem, kto jest mądrzejszy, albo do obrażania siebie nawzajem.

> Mnie
> się nie chciało już tłumaczyć, że słowo "precyzja" zmienia
> znaczenie zależnie od kontekstu. Nie chce mi się precyzyjnie
> tłumaczyć za każdym razem jak używam każdego słowa.

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?

> > pisząc to, co napisałem powyżej, bo mogłoby to zostać
> > odebrane jako pogardliwe, a nie chciałbym, żeby tak było.
> > Przepraszam. (Z żalem przyznam, że to chyba "dyskusje"
> > z niektórymi osobami na tej grupie tak mnie zdegenerowały,
> > choć oczywiście nie ma się co obwiniać, a trzeba pracować
> > nad tym, żeby było lepiej)
> Nie ma nic pogardliwego w podaniu linku do literatury.

W podaniu linku do literatury oczywiście nie ma,
ale jest coś niedobrego w podchodzeniu do dyskusji
w kategoriach tego, kto ma rację, a nie tego, jak
się rzeczy mają. (W każdym razie mam wrażenie, że
na tej grupie roi się od osób, które czują się na
tyle wielkie, że niczym wyrocznia w Delfach są
zwolnione z konieczności uzasadniania swoich stwierdzeń)

> > To jest trochę (bardzo?) OT,
> Nie jest OT, rozmawiamy od dowodzeniu poprawności równoległego programu.

Tak, ale temat programowania współbieżnego jest dość przepastny.
W każdym razie bardzo daleki od tego, o co pytał OP (jednak trzeba
przyznać, że nie udzielił dostatecznie dużo informacji, żeby móc
uzyskać sensowną pomoc)

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. 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)

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

> > Gorzej jeżeli mamy kilka etapów obliczeń: może być tak, że
> > fragment pamięci, do którego zapis wykona kilka wątków
> > na jednym etapie, będzie potem użyty do obliczeń na innym
> > etapie. Żeby jednak mogło się tak stać, musimy się upewnić,
> > że wszystkie wątki skończyły już zapis -- i do tego właśnie
> > używa się __syncthreads()
> Ja bym to inaczej uzasadnił, choć nigdy nie używałem takiej metody.
> Mamy np. trzy wątki. W pierwszym etapie watek pierwszy dostaje dane spod
> adresów 0,1,2, drugi spod: 3,4,5, trzeci spod: 6,7,8. W drugim etapie
> wątek pierwszy dostaje dane 0,3,6; drugi 1,4,7; w trzecim 2,5,8.
> Wtedy istotnie muszą wszystkie wątki czekać pomiędzy etapami.

Tak, to jest dobry przykład, ale trzeba by było jeszcze dopowiedzieć,
że owe wątki zapisują również dane do pamięci, bo dopiero wtedy zajdzie
potrzeba synchronizacji

do góry

On Thursday, April 2, 2015 at 10:56:13 AM UTC+2, g...@g...com wrote:
> W dniu czwartek, 2 kwietnia 2015 08:14:46 UTC+2 użytkownik M.M. napisał:
>
> > > > > Nie mam aż tyle czasu, myślalem że rzucisz kilka zalet.
> > > > Zalet synchronizacji wątków przed dostępem do pamięci?
> > >
> > > Tak sobie myślę, że chyba niezbyt ładnie się zachowałem,
> > Podając linki do literatury? To akurat bardzo w porządku.
>
> Raczej miałem na myśli ton, w jakim zadałem powyższe pytanie.
> Strasznie mnie smuci to, że dyskusje na tej grupie są często
> mało merytoryczne i sprowadzają się do udowadniania sobie
> nawzajem, kto jest mądrzejszy, albo do obrażania siebie nawzajem.
Nie rozumiem o jaki ton chodzi, ale nieważne.

>
> > Mnie
> > się nie chciało już tłumaczyć, że słowo "precyzja" zmienia
> > znaczenie zależnie od kontekstu. Nie chce mi się precyzyjnie
> > tłumaczyć za każdym razem jak używam każdego słowa.
>
> 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.

> > > pisząc to, co napisałem powyżej, bo mogłoby to zostać
> > > odebrane jako pogardliwe, a nie chciałbym, żeby tak było.
> > > Przepraszam. (Z żalem przyznam, że to chyba "dyskusje"
> > > z niektórymi osobami na tej grupie tak mnie zdegenerowały,
> > > choć oczywiście nie ma się co obwiniać, a trzeba pracować
> > > nad tym, żeby było lepiej)
> > Nie ma nic pogardliwego w podaniu linku do literatury.
>
> W podaniu linku do literatury oczywiście nie ma,
> ale jest coś niedobrego w podchodzeniu do dyskusji
> w kategoriach tego, kto ma rację, a nie tego, jak
> się rzeczy mają. (W każdym razie mam wrażenie, że
> na tej grupie roi się od osób, które czują się na
> tyle wielkie, że niczym wyrocznia w Delfach są
> zwolnione z konieczności uzasadniania swoich stwierdzeń)
>
> > > To jest trochę (bardzo?) OT,
> > Nie jest OT, rozmawiamy od dowodzeniu poprawności równoległego programu.
>
> Tak, ale temat programowania współbieżnego jest dość przepastny.
> W każdym razie bardzo daleki od tego, o co pytał OP (jednak trzeba
> przyznać, że nie udzielił dostatecznie dużo informacji, żeby móc
> uzyskać sensowną pomoc)
>
> 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?


> 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.


> 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.

>
> > > Gorzej jeżeli mamy kilka etapów obliczeń: może być tak, że
> > > fragment pamięci, do którego zapis wykona kilka wątków
> > > na jednym etapie, będzie potem użyty do obliczeń na innym
> > > etapie. Żeby jednak mogło się tak stać, musimy się upewnić,
> > > że wszystkie wątki skończyły już zapis -- i do tego właśnie
> > > używa się __syncthreads()
> > Ja bym to inaczej uzasadnił, choć nigdy nie używałem takiej metody.
> > Mamy np. trzy wątki. W pierwszym etapie watek pierwszy dostaje dane spod
> > adresów 0,1,2, drugi spod: 3,4,5, trzeci spod: 6,7,8. W drugim etapie
> > wątek pierwszy dostaje dane 0,3,6; drugi 1,4,7; w trzecim 2,5,8.
> > Wtedy istotnie muszą wszystkie wątki czekać pomiędzy etapami.
>
> Tak, to jest dobry przykład,
W skrócie: dane muszą być "przemieszane" pomiędzy wątkami i etapami.

> 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ć.

Pozdrawiam

do góry

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

do góry

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

do góry