On Tuesday, March 31, 2015 at 12:20:29 PM UTC+2, g...@g...com wrote:
> W dniu sobota, 28 marca 2015 10:54:16 UTC+1 użytkownik M.M. napisał:
> > > >
> > > > Mój (hipotetyczny) klient zamawia najlepszy program do gry w
> > > > szachy o łącznym rozmiarze kodu i danych nie większym niż 1MB. Napisałem
> > > > taki program. Jak mam przeprowadzić dowód, że nie istnieje w
> > > > ramach tego rozmiaru lepszy program?
> > >
> > > To akurat nie jest problem metody dowodowej,
> > Właśnie, tego nie da się udowodnić, a jest to też ważny aspekt
> > programu. A w testach tak się robi, porównuje się kilka
> > różnych algorytmów dla różnych danych.
>
> 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ń.

> (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.

Inny przykład, program do translacji języków naturalnych. Dlaczego
chciałbyś używać gorszy program niż lepszy?

Następny problem: gra w szachy. Dlaczego używać słabszego programu niż
silniejszego? Można mnożyć...

> 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?

>
> > > tylko nieprecyzyjnej
> > > specyfikacji. Co to znaczy,że "w ramach określonego rozmiaru program
> > > jest lepszy od innego programu"?
> > Zakładamy że specyfikacja jest dobra. To jest kwestia jakości
> > użytych algorytmów/heurystyk.
>
> 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.

> 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.



>
> > > 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.

do góry

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ę

> > (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ć)

> 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"

> 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

> > 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.

> > 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.

> > > > 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().
W jaki sposób przetłumaczyłbyś tę sytuację na swój "ogólniony semafor"?

do góry

Użytkownik "M.M." napisał w wiadomości grup
dyskusyjnych:c8c46028-ecf9-454b-bb5d-75458b6ea66f@go
oglegroups.com...

>Inny przykład, program do translacji języków naturalnych. Dlaczego
>chciałbyś używać gorszy program niż lepszy?

Dlaczego uważasz, że dla w/w programów da się ustalić relację liniowego
(pół)porządku?

A praktycznie: program X zwykle daje ładniejszy tekst, ale za to przetwarza
dane w chmurze, wysyłając je na serwer nie-wiadomo-gdzie. Program Y daje
przyzwoitą jakość i przetwarza lokalnie. Który wybierzesz do przetłumaczenia
tekstu przetargu? A który do przetłumaczenia tekstu na publicznie dostępną
stronę WWW?

>Następny problem: gra w szachy. Dlaczego używać słabszego programu niż
>silniejszego? Można mnożyć...

Bo np. silniejszy program zawsze wygrywa, więc nie ma fun-u?
Można dzielić...

>się konkretyzuje. Bez względu na to jak się skonkretyzuje, to ciężko
>dokonać takiego dowodu formalnego.

Problem, IMO, leży w czym innym: dowody formalne zapobiegają tylko niektórym
błędom. A same z siebie mogą być błędne. Więc stwarzają złudną iluzję
bezpieczeństwa.

Ok. Zastąpmy "dowodzenie formalne" przez "pasy bezpieczeństwa". Oczywiście,
pasy ratują życie itd. Ale /pomimo/ pasów zdarzają się śmiertelne wypadki.
Więc np. jazda na podwójnym gazie, 200 km/h w terenie zabudowanym, w gęstej
mgle i pod prąd nie jest bezpieczna nawet jeżeli PASY SĄ ZAPIĘTE. Podobnie
pisanie super-odpowiedzialnych programów przez tylko jednego programistę,
bez testów - NAWET Z UŻYCIEM FORMALNYCH DOWODÓW POPRAWNOŚCI - nie jest moim
zdaniem dobrym pomysłem. I niekoniecznie dlatego że będą błędy.

do góry

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

do góry

On Tuesday, March 31, 2015 at 7:08:24 PM UTC+2, slawek wrote:
> Użytkownik "M.M." napisał w wiadomości grup
> dyskusyjnych:
>
> >Inny przykład, program do translacji języków naturalnych. Dlaczego
> >chciałbyś używać gorszy program niż lepszy?
>
> Dlaczego uważasz, że dla w/w programów da się ustalić relację liniowego
> (pół)porządku?
Da się. Bierzemy N programów, M tekstów, K ludzi. Każda osoba czyta
przetłumaczony tekst i wystawia ocenę od zera do np 10. Sumujemy
punkty. Więc w ogóle można porównywać program do tłumaczenia, a na
podstawie kodu nie można.


> A praktycznie: program X zwykle daje ładniejszy tekst, ale za to przetwarza
> dane w chmurze, wysyłając je na serwer nie-wiadomo-gdzie. Program Y daje
> przyzwoitą jakość i przetwarza lokalnie. Który wybierzesz do przetłumaczenia
> tekstu przetargu? A który do przetłumaczenia tekstu na publicznie dostępną
> stronę WWW?
>
> >Następny problem: gra w szachy. Dlaczego używać słabszego programu niż
> >silniejszego? Można mnożyć...
>
> Bo np. silniejszy program zawsze wygrywa, więc nie ma fun-u?
> Można dzielić...
Jak już odbiegamy, to też nie zawsze. Weźmiemy np. 20 programów i
zrobimy turniej każdy z każdym. Może się okazać, że zwycięzca
turnieju przegrywa z przegranym - ale to tylko na marginesie.

>
> >się konkretyzuje. Bez względu na to jak się skonkretyzuje, to ciężko
> >dokonać takiego dowodu formalnego.
>
> Problem, IMO, leży w czym innym: dowody formalne zapobiegają tylko niektórym
> błędom. A same z siebie mogą być błędne. Więc stwarzają złudną iluzję
> bezpieczeństwa.
>
> Ok. Zastąpmy "dowodzenie formalne" przez "pasy bezpieczeństwa". Oczywiście,
> pasy ratują życie itd. Ale /pomimo/ pasów zdarzają się śmiertelne wypadki.
> Więc np. jazda na podwójnym gazie, 200 km/h w terenie zabudowanym, w gęstej
> mgle i pod prąd nie jest bezpieczna nawet jeżeli PASY SĄ ZAPIĘTE. Podobnie
> pisanie super-odpowiedzialnych programów przez tylko jednego programistę,
> bez testów - NAWET Z UŻYCIEM FORMALNYCH DOWODÓW POPRAWNOŚCI - nie jest moim
> zdaniem dobrym pomysłem. I niekoniecznie dlatego że będą błędy.
Soft do sterowania rakietami podobno
pisało osiem niezależnych zespołów. Wszystkie osiem wersji softu
działało równolegle. Wyjście tych wszystkich wersji trafiało do systemu
głosowania. Nawet jeśli tylko 2 wersje dały dobrą odpowiedź, a
pozostały złą ale różną od siebie, to system jako całość działał.


Pozdrawiam

do góry

W dniu wtorek, 31 marca 2015 19:29:20 UTC+2 użytkownik M.M. napisał:
> >
> > "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.

Generalizowanie to tyle, co uogólnianie, czyli przechodzenie
od przypadku konkretniejszego do ogólniejszego. Stąd, że Twoje
generalizowanie jest nieprecyzyjne, nie wynika, że każde generalizowanie
jest nieprecyzyjne.
Na przykład dodanie funkcji porównującej jako parametru
dla funkcji "sort" jest generalizowaniem, a jest piekielnie
precyzyjne.

> > 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? ;-)

Problem polega na tym, że nie wiem, o co Ci chodziło, bo wyraziłeś
się dość nieprecyzyjnie

> > > 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.

W pewnym zakresie może tak. Ale znajdzie się również taki, w którym
eksperci będą między sobą dywagować, czy Słomczyński, czy Barańczak

> > 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.

Też nie wiem. Prawdopodobnie nie można, tym bardziej, że
nie umiemy nawet uściślić, co to znaczy "lepiej tłumaczyć tekst"

> > 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?

W niektórych przypadkach możemy być może policzyć, jaka jest teoretyczna
granica wydajności, i pokazać, że nasz algorytm ją realizuje (jeżeli
poprze "lepszość" rozumiemy mniejszą złożoność obliczeniową)

Ale niestety Twoje użycie słowa "najlepszy" jest nieprecyzyjne,
bo "najlepszy" może być również w sensie "maintainability" -- że
ma najlepsze komentarze, jest najłatwiej rozszerzalny itd.

> > 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?

Nie rozumiem o co pytasz. W ogólności zależy to od przypadku.

> > > > 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?

Umożliwia synchronizację wątków przed dostępem do pamięci.
Jeśli Cię to bardziej interesuje, polecam kurs z "Heterogenous Parallel
Programming" na Courserze albo książkę "CUDA w przykładach" (wyd. Helion)

> > 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.

Nie. Każdy wątek może bezpiecznie wywołać __syncthreads i nie ma potrzeby
zabezpieczania jej semaforami, zaś (pomijając kwestię marnowania zasobów)
właśnie z tego względu zabezpieczanie semaforami nic w tym przypadku nie
da, a tym bardziej nie ochroni przed deadlockiem.

do góry

Użytkownik napisał w wiadomości grup
dyskusyjnych:fec16715-19e6-4b77-b1e4-ce87326de28b@go
oglegroups.com...

>Z ciekawości zapytam: jakie masz doświadczenie z formalnym dowodzeniem
>twierdzeń?

Z ciekawości zapytam: czy udało się zrobić system klasy A według Orange Book
DoD?

Tu masz link http://csrc.nist.gov/publications/history/dod85.pdf, jakbyś nie
pamiętał o co chodzi, a pamiętasz, prawda?

do góry

Użytkownik "M.M." napisał w wiadomości grup
dyskusyjnych:47d74d19-db68-4988-893e-d37e1e996365@go
oglegroups.com...

>Soft do sterowania rakietami podobno
>pisało osiem niezależnych zespołów. Wszystkie osiem wersji softu
>działało równolegle. Wyjście tych wszystkich wersji trafiało do systemu
>głosowania. Nawet jeśli tylko 2 wersje dały dobrą odpowiedź, a
>pozostały złą ale różną od siebie, to system jako całość działał.

I co zrobisz, jeżeli 1 i 2 dają odpowiedź A, 3 i 4 dają B, a 5 po prostu się
sfajczył?

do góry

W dniu wtorek, 31 marca 2015 20:00:08 UTC+2 użytkownik slawek napisał:
> Użytkownik napisał w wiadomości grup
> dyskusyjnych:fec16715-19e6-4b77-b1e4-ce87326de28b@go
oglegroups.com...
>
> >Z ciekawości zapytam: jakie masz doświadczenie z formalnym dowodzeniem
> >twierdzeń?
>
> Z ciekawości zapytam: czy udało się zrobić system klasy A według Orange Book
> DoD?

Unikanie odpowiedzi na pytanie poprzez zadawanie innego pytania
nie robi na mnie wrażenia. Jeżeli zrobiłeś coś, z czego jesteś
dumny i chcesz się pochwalić, to myślę, że wszyscy chętnie posłuchamy.

Jeżeli idzie o mnie, to nie, nie próbowałem nawet nigdy zrobić systemu
klasy A według Orange Book DoD.

do góry

On Tuesday, March 31, 2015 at 8:10:47 PM UTC+2, slawek wrote:
> Użytkownik "M.M." napisał w wiadomości grup
> dyskusyjnych:47d74d19-db68-4988-893e-d37e1e996365@go
oglegroups.com...
>
> >Soft do sterowania rakietami podobno
> >pisało osiem niezależnych zespołów. Wszystkie osiem wersji softu
> >działało równolegle. Wyjście tych wszystkich wersji trafiało do systemu
> >głosowania. Nawet jeśli tylko 2 wersje dały dobrą odpowiedź, a
> >pozostały złą ale różną od siebie, to system jako całość działał.
>
> I co zrobisz, jeżeli 1 i 2 dają odpowiedź A, 3 i 4 dają B, a 5 po prostu się
> sfajczył?
TO nie przejdzie :) Napisałem o ciut bardziej korzystnej
sytuacji: "złą ale różną".

do góry