-
Data: 2015-04-02 17:20:09
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 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
Najnowsze wątki z tej grupy
- Do czego nadaje się QDockWidget z bibl. Qt?
- Bibl. Qt jest sztucznie ograniczona - jest nieprzydatna do celów komercyjnych
- Co sciaga kretynow
- AEiC 2024 - Ada-Europe conference - Deadlines Approaching
- Jakie są dobre zasady programowania programów opartych na wtyczkach?
- sprawdzanie słów kluczowych dot. zła
- Re: W czym sie teraz pisze programy??
- Re: (PDF) Surgical Pathology of Non-neoplastic Gastrointestinal Diseases by Lizhi Zhang
- CfC 28th Ada-Europe Int. Conf. Reliable Software Technologies
- Młodzi programiści i tajna policja
- Ada 2022 Language Reference Manual to be Published by Springer
- Press Release - AEiC 2023, Ada-Europe Reliable Softw. Technol.
- Ada-Europe - AEiC 2023 early registration deadline approaching
- Ada-Europe Int.Conf. Reliable Software Technologies, AEiC 2023
- Ile cykli zajmuje mnożenie liczb 64-bitowych?
Najnowsze wątki
- 2024-07-10 Nadchodzi nowa opłata od posiadania aut spalinowych
- 2024-07-10 Droga dwukierunkowa
- 2024-07-10 Elektryki są fajne
- 2024-07-10 Elektryki są fajne :(
- 2024-07-09 USB -> jack
- 2024-07-10 Kompakt WC z montażem
- 2024-07-10 Gorąco za oknem, to napisałem piosenkę o grupowiczach
- 2024-07-09 Naprawa klimy przenośnej - czy to opłacalne?
- 2024-07-10 Białystok => Technical Leader (Java Background) <=
- 2024-07-10 Białystok => Senior Rust Software Engineer <=
- 2024-07-10 Warszawa => Spedytor Międzynarodowy <=
- 2024-07-10 Warszawa => Spedytor międzynarodowy <=
- 2024-07-10 Warszawa => Technical Lead ( (Java Background)) <=
- 2024-07-10 Warszawa => Projektant/Programista React Native <=
- 2024-07-10 Gdańsk => Head of International Freight Forwarding Department <=