-
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
- Grok zaczął nadużywać wulgaryzmów i wprost obrażać niektóre znane osoby
- Can you activate BMW 48V 10Ah Li-Ion battery, connecting to CAN-USB laptop interface ?
- We Wrocławiu ruszyła Odra 5, pierwszy w Polsce komputer kwantowy z nadprzewodzącymi kubitami
- Ada-Europe - AEiC 2025 early registration deadline imminent
- John Carmack twierdzi, że gdyby gry były optymalizowane, to wystarczyły by stare kompy
- Ada-Europe Int.Conf. Reliable Software Technologies, AEiC 2025
- Linuks od wer. 6.15 przestanie wspierać procesory 486 i będzie wymagać min. Pentium
- ,,Polski przemysł jest w stanie agonalnym" - podkreślił dobitnie, wskazując na brak zamówień.
- Rewolucja w debugowaniu!!! SI analizuje zrzuty pamięci systemu M$ Windows!!!
- Brednie w wiki - hasło Dehomag
- Perfidne ataki krakerów z KRLD na skrypciarzy JS i Pajton
- Instytut IDEAS może zacząć działać: "Ma to być unikalny w europejskiej skali ośrodek badań nad sztuczną inteligencją."
- Instytut IDEAS może zacząć działać: "Ma to być unikalny w europejskiej skali ośrodek badań nad sztuczną inteligencją."
- Instytut IDEAS może zacząć działać: "Ma to być unikalny w europejskiej skali ośrodek badań nad sztuczną inteligencją."
- U nas propagują modę na SI, a w Chinach naukowcy SI po kolei umierają w wieku 40-50lat
Najnowsze wątki
- 2025-07-20 Absurdalny zakaz fotografowania będzie nowelizowany
- 2025-07-20 Takie tam...
- 2025-07-20 https://newsgrouper.org/pl.soc.prawo blokuje posty: 154 posts blocked.
- 2025-07-20 Bateria 9V 6F22, alkaliczna v cynkowa, samorozładowanie, bateria wysokiej trwałości do miernika
- 2025-07-20 Tani zakup z ali?
- 2025-07-19 Wrocław => Konsultant wdrożeniowy (systemy controlingowe) <=
- 2025-07-19 Chiny => Koordynator Produkcji / Przedstawiciel ds. rozwoju produktu <
- 2025-07-19 Środa Wielkopolska => SAP FI/CO Internal Consultant <=
- 2025-07-19 China => Production Coordinator / Representant Product Dev <=
- 2025-07-19 Warszawa => Specjalista wsparcia IT - analiza techniczna sprzętu IT <
- 2025-07-19 Warszawa => Strategic Account Manager <=
- 2025-07-19 Warszawa => Key Account Manager IT <=
- 2025-07-19 Skazany za zabójstwo a ofiara żyje
- 2025-07-19 Zakrzewo => SAP HCM Consultant <=
- 2025-07-19 Poznań => Konsultant SAP HCM <=