eGospodarka.pl
eGospodarka.pl poleca

eGospodarka.plGrupypl.comp.programmingpoprawność algorytmu › Re: poprawność algorytmu
  • Data: 2015-04-02 12:54:35
    Temat: Re: poprawność algorytmu
    Od: "M.M." <m...@g...com> szukaj wiadomości tego autora
    [ pokaż wszystkie nagłówki ]

    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

Podziel się

Poleć ten post znajomemu poleć

Wydrukuj ten post drukuj


Następne wpisy z tego wątku

Najnowsze wątki z tej grupy


Najnowsze wątki

Szukaj w grupach

Eksperci egospodarka.pl

1 1 1

Wpisz nazwę miasta, dla którego chcesz znaleźć jednostkę ZUS.

Wzory dokumentów

Bezpłatne wzory dokumentów i formularzy.
Wyszukaj i pobierz za darmo: