-
X-Received: by 10.140.23.163 with SMTP id 32mr566867qgp.13.1427822959032; Tue, 31 Mar
2015 10:29:19 -0700 (PDT)
X-Received: by 10.140.23.163 with SMTP id 32mr566867qgp.13.1427822959032; Tue, 31 Mar
2015 10:29:19 -0700 (PDT)
Path: news-archive.icm.edu.pl!news.icm.edu.pl!newsfeed.pionier.net.pl!news.glorb.com!
h15no2621642igd.0!news-out.google.com!f74ni4qge.0!nntp.google.com!q107no916296q
gd.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: pl.comp.programming
Date: Tue, 31 Mar 2015 10:29:18 -0700 (PDT)
In-Reply-To: <2...@g...com>
Complaints-To: g...@g...com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=178.36.122.220;
posting-account=xjvq9QoAAAATMPC2X3btlHd_LkaJo_rj
NNTP-Posting-Host: 178.36.122.220
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>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <b...@g...com>
Subject: Re: poprawność algorytmu
From: "M.M." <m...@g...com>
Injection-Date: Tue, 31 Mar 2015 17:29:19 +0000
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable
Xref: news-archive.icm.edu.pl pl.comp.programming:207723
[ ukryj nagłówki ]On Tuesday, March 31, 2015 at 4:39:21 PM UTC+2, g...@g...com wrote:
> W dniu wtorek, 31 marca 2015 14:48:38 UTC+2 użytkownik M.M. napisał:
> > >
> > > To, że "nie istnieje w ramach określonego rozmiaru >>lepszy<< program"
> > > jest "ważnym aspektem programu"? Dla kogo jest to ważne?
> > Uprościłem pewien aspekt złożoności do 'rozmiaru' - miałem bardzo
> > podobną sytuację w praktyce. Ale ok, nie ciągnijmy.
> >
> > > Klienta interesuje, żeby program działał zadowalająco dobrze, a nie to, żeby
> > > "w ramach określonego rozmiaru programu nie istniał jakiś lepszy".
> > Nie zgodzę się, klient może chcieć aby program działał jak najlepiej
> > to możliwe - w ramach jakiś ograniczeń.
>
> "Najlepiej jak to możliwe" -- to też nieprecyzyjne określenie.
> Można je rozumieć jako "najlepiej jak komputer potrafi", albo
> "najlepiej jak programista potrafi". To ostatnie jest zresztą
> zazwyczaj twardym limitem, chyba że klient znajdzie lepszego
> programistę
No oczywiście że jest nieprecyzyjne. Jest nieprecyzyjne jak każde
generalizowanie.
>
> > > (W każdym razie ja nie spotkałem nigdy klienta o tak osobliwych
> > > zainteresowaniach. Ale nawet gdybym spotkał, pewnie po prostu nie
> > > uwierzyłbym własnym uszom)
> > Dlaczego byś nie uwierzył? Program wspomaga decyzje. Od decyzji zależy
> > (w jakimś stopniu) generowanie zysków. Co w tym dziwnego, że chcemy
> > aby taki program działał jak najlepiej.
>
> Powiedzieć, że coś "działa jak najlepiej", to coś innego, niż
> powiedzieć, że "nie istnieje w ramach pewnych ograniczeń lepszy program"
> (nie jest nawet jasne, co się tutaj rozumie w kwestii "istnienia programu"
> -- czy chodzi o jakiś program dostępny na rynku, czy taki, który
> ktoś potencjalnie mógłby napisać)
Przypuszczasz, że chodziło mi o dowód formalny (na podstawie kodu
źródłowego) na istnienie lepszego programu na rynku? ;-)
> > Inny przykład, program do translacji języków naturalnych. Dlaczego
> > chciałbyś używać gorszy program niż lepszy?
>
> Ja nie wiem, co to znaczy w tym kontekście "gorszy", a co "lepszy"
A ja wiem że wiesz, potrafisz odróżnić tekst dobrze przetłumaczony od
źle przetłumaczonego.
> > Następny problem: gra w szachy. Dlaczego używać słabszego programu niż
> > silniejszego? Można mnożyć...
>
> Zgaduję teraz, że pisząc o "program do gry w szachy" masz na myśli
> "program grający w szachy"? Jeśli tak, to ok -- rozumiem, co to znaczy
> "lepszy", a co "gorszy" (choć oczywiście jest to tylko częściowy
> porządek)
>
> > > Nie widzę też, w jaki sposób testy miałyby tu być pomocne.
> > Bierzesz wiele danych wejściowych, porównujesz jakość odpowiedzi i
> > oceniasz. A jak na podstawie kodu udowodnić, że jeden program lepiej
> > translatuje, albo lepiej gra w szachy, od drugiego?
>
> Oczywiście, kiedy masz już pewne kryterium jakości, to możesz się
> pokusić o przeprowadzenie formalnego dowodu w odniesieniu do tego
> kryterium
Nie wiem jak można udowodnić na podstawie źródeł dwóch
programów, który program lepiej tłumaczy tekst.
>
> > > To, co piszesz, nic nie wyjaśnia.
> > > Powiedzenie, że coś jest najlepsze, jest po prostu powiedzeniem
> > > nieprecyzyjnym.
> > Wiadomo że jest nieprecyzyjnym. W każdym przypadku co innego
> > oznacza najlepszy. W każdym przypadku chodzi o inną jakość algorytmów czy
> > heurystyk. Obojętnie o jaką jakość chodzi, to trudno dowieść jej
> > formalnie na podstawie kodu.
>
> Przeciwnie. Dla pewnych kryteriów przeprowadzenie formalnych dowodów
> będzie prostsze, dla innych trudniejsze, a dla jeszcze innych niemożliwe.
Różnych programów o rozmiarze N bajtów mamy 256^N. Mamy definicję
dopuszczalnych danych wejściowych, być może wraz z rozkładem
prawdopodobieństwa. Mamy precyzyjnie określone co oznacza najlepszy.
Jak udowodnić, że wśród 256^N nie istnieje żaden lepszy program
od naszego?
> > > Co to znaczy "najlepsze"? Że przynosi najwięcej
> > > pieniędzy? Że ma najwięcej użytkowników? Że najbardziej podoba
> > > się klientowi?
> > Tak, dobre przykłady.
> >
> > > Jeżeli podajesz jawnie złą specyfikację, to potem nie możesz mówić
> > > "zakładamy, że specyfikacja jest dobra", bo nie jest.
> > Można tak mówić, ponieważ to generalne określenie w każdym przypadku
> > się konkretyzuje. Bez względu na to jak się skonkretyzuje, to ciężko
> > dokonać takiego dowodu formalnego.
>
> Nieprawda. To, jak się coś skonkretyzuje (oraz co się skonkretyzuje),
> ma kluczowe znaczenie dla łatwości/trudności przeprowadzenia dowodu.
Może czegoś nie wiem, dla jakich kryteriów dowód będzie łatwy w
przeprowadzeniu?
> > > > > Zresztą cechy użytkowe nie są czymś, co dowodzi się formalnie
> > > > > (bo są subiektywne). Formalnie chcemy dowodzić raczej pewnych
> > > > > inwariantów -- że na przykład w programie wielowątkowym nie dojdzie
> > > > > do sytuacji dead-locku (klasyczne zastosowane logik temporalnych),
> > > > Nie słyszałem o logice temporalnej. Może się mylę, ale to się
> > > > wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
> > > > wszystkie pary kodu, który może wykonać się równolegle, były
> > > > opatrzone semaforami w tej samej kolejności w sensie wykonania i
> > > > w odwrotnej kolejności (też w sensie wykonania).
> > >
> > > Mylisz się z pewnością, choćby dlatego, że semafor nie jest jedynym
> > > mechanizmem synchronizującym używanym w programach wielowątkowych.
> > Jeśli odebrałeś moje słowa dosłownie, to mam prośbę. Najpierw uogólnij
> > sobie mój 'semafor' na inne mechanizmy synchronizowania, a potem
> > przeanalizuj czy się mylę. Potem pogadamy dalej.
>
> Na przykład w API CUDA dla GPU nVidii masz polecenie __syncthreads(), które
> działa w taki sposób, że wszystkie wątki czekają, aż ostatni wątek wywoła
> owo polecenie. Deadlocka otrzymamy w każdym przypadku, gdy którykolwiek
> z wątków w danej jednostce uruchomieniowej nie wywoła polecenia __syncthreads().
Nigdy nie używałem tego polecenia. Czy jest konieczne używanie?
Co ono usprawnia? Nigdy nie pisałem tak programu, aby jeden
wątek (dosłownie) czekał na inny wątek. W moich programach wątki
czekają aż wejście do pewnych instrukcji będzie dozwolone. Nigdy nie
wiem czy one czekają aż ostatni dojdzie do bariery, czy wejdzie
najpierw trzeci, czy najpierw pierwszy. Zawsze chcę aby weszły
do instrukcji jak najszybciej z powodu wydajności, nie wiem dlaczego
mam czekać na ostatni.
> W jaki sposób przetłumaczyłbyś tę sytuację na swój "ogólniony semafor"?
Nie wiem, w taki sposób nie programowalem nigdy. Na pewno wszystkie
wątki muszą dojść do tej instrukcji. A żeby doszły, to nie mogą się
wcześniej zablokować i syncthreads musi być wspólną instrukcją....
Chyba mam sposób. Jeśli używam N semaforów s1, s2, ... sN, to zakładam, że
każde synthreads jest objęte:
s1
s2
sn
syncthreds
sn
s2
s1
Potem używam wszędzie w tej samej kolejności od s1 do sn.
Pozdrawiam
Następne wpisy z tego wątku
- 31.03.15 19:43 M.M.
- 31.03.15 19:49 g...@g...com
- 31.03.15 19:59 slawek
- 31.03.15 20:10 slawek
- 31.03.15 20:34 g...@g...com
- 31.03.15 21:01 M.M.
- 31.03.15 23:04 slawek
- 31.03.15 23:25 g...@g...com
- 31.03.15 23:32 Andrzej Jarzabek
- 31.03.15 23:59 slawek
- 01.04.15 00:08 g...@g...com
- 01.04.15 08:46 firr
- 01.04.15 09:01 firr
- 01.04.15 11:57 M.M.
- 01.04.15 12:03 M.M.
Najnowsze wątki z tej grupy
- TCL - problem z escape ostatniego \ w nawiasach {}
- Nauka i Praca Programisty C++ w III Rzeczy (pospolitej)
- testy-wyd-sort - Podsumowanie
- Tworzenie Programów Nieuprzywilejowanych Opartych Na Wtyczkach
- 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
Najnowsze wątki
- 2024-11-08 Warszawa => Head of International Freight Forwarding Department <=
- 2024-11-08 Warszawa => Key Account Manager <=
- 2024-11-08 Szczecin => Key Account Manager (ERP) <=
- 2024-11-08 Białystok => Full Stack web developer (obszar .Net Core, Angular6+) <
- 2024-11-08 Wrocław => Senior PHP Symfony Developer <=
- 2024-11-08 Warszawa => QA Engineer <=
- 2024-11-08 Warszawa => QA Inżynier <=
- 2024-11-08 Warszawa => Key Account Manager <=
- 2024-11-08 Gdańsk => Software .Net Developer <=
- 2024-11-08 Akumulator Hyundai
- 2024-11-08 Warszawa => Manager/Specialist e-commerce (B2C) <=
- 2024-11-08 Gdańsk => Specjalista ds. Sprzedaży <=
- 2024-11-08 Gdańsk => Kierownik Działu Spedycji Międzynarodowej <=
- 2024-11-08 znaj podstawe
- 2024-11-08 Chrzanów => Specjalista ds. public relations <=