-
X-Received: by 10.140.21.145 with SMTP id 17mr708228qgl.1.1427976786859; Thu, 02 Apr
2015 05:13:06 -0700 (PDT)
X-Received: by 10.140.21.145 with SMTP id 17mr708228qgl.1.1427976786859; Thu, 02 Apr
2015 05:13:06 -0700 (PDT)
Path: news-archive.icm.edu.pl!agh.edu.pl!news.agh.edu.pl!newsfeed2.atman.pl!newsfeed.
atman.pl!news.supermedia.pl!news.nask.pl!news.nask.org.pl!news.unit0.net!news.g
lorb.com!l13no735265iga.0!news-out.google.com!q14ni5765ign.0!nntp.google.com!j5
no73597qga.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mai
l
Newsgroups: pl.comp.programming
Date: Thu, 2 Apr 2015 05:13:06 -0700 (PDT)
In-Reply-To: <a...@g...com>
Complaints-To: g...@g...com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=89.71.15.176;
posting-account=f7iIKQoAAAAkDKpUafc-4IXhmRAzdB5r
NNTP-Posting-Host: 89.71.15.176
References: <4...@g...com>
<d...@g...com>
<meti4e$osd$1@srv.chmurka.net>
<f...@g...com>
<mevfpd$gpa$1@srv.chmurka.net>
<e...@g...com>
<mf1tnf$d48$1@srv.chmurka.net>
<d...@g...com>
<e...@g...com>
<f...@g...com>
<b...@g...com>
<4...@g...com>
<f...@g...com>
<8...@g...com>
<b...@g...com>
<c...@g...com>
<2...@g...com>
<b...@g...com>
<6...@g...com>
<b...@g...com>
<7...@g...com>
<9...@g...com>
<b...@g...com>
<2...@g...com>
<a...@g...com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <b...@g...com>
Subject: Re: poprawność algorytmu
From: g...@g...com
Injection-Date: Thu, 02 Apr 2015 12:13:06 +0000
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable
Xref: news-archive.icm.edu.pl pl.comp.programming:207774
[ ukryj nagłówki ]
> > 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 ;]
Następne wpisy z tego wątku
- 02.04.15 17:20 M.M.
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-01 W-wa naklejki wjazd do centrum
- 2024-07-01 ładowarka zmarła
- 2024-07-01 Koder szuka pracy. Koduję w j.: Asembler, C, C++ (z Qt) i D.
- 2024-07-01 Kraków => Kierownik Działu Spedycji Międzynarodowej <=
- 2024-07-01 Białystok => Full Stack Web Developer (.Net Core, Angular6+) <=
- 2024-07-01 Berlin => Technical Rollouter (Radio Systems Software Installation and
- 2024-07-01 Warszawa => Key Account Manager <=
- 2024-07-01 Gdańsk => Programista Full Stack .Net <=
- 2024-07-01 Zabrze => Junior HelpDesk <=
- 2024-07-01 Warszawa => Key Account Manager <=
- 2024-07-01 Bielsko-Biała => Expert Migration Architect (Azure) <=
- 2024-07-01 Mini Netykieta polskich grup dyskusyjnych
- 2024-07-01 Re: Jak wypełnić polecenie francuskiego sądu blokowania niektórych zapytań DNS? Blokując Francję
- 2024-07-01 Re: Powtórne wezwanie na PO-komisję uzdrowi Ziobrę już w 10 dni
- 2024-07-01 CA -- problem z logowaniem