On Tuesday, March 31, 2015 at 7:49:55 PM UTC+2, g...@g...com wrote:
> 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.
Poczekaj bo się robią jakieś jaja z tej rozmowy:) Wątek ten dotyczy (nie)przydatności
formalnego dowodu na poprawność programu w
praktyce programistycznej/biznesowej. Potem ja wtrąciłem, że
wymagania są różne, np. klient chce najlepszy program. Jak słuszne
zauważyłeś, nie precyzowałem co oznacza najlepszy. Piłem do tego,
że jeśli już tak ściśle i formalnie chcemy dowodzić, to należało
by również dowieść, że program istotnie jest najlepszy. Więc moje
generalizowanie obejmuje zbiór kryteriów według których
w praktyce programistycznej ocenia się programy. Co widzisz
nieprecyzyjnego w takim generalizowaniu? Albo jakie kryteria
uznajesz (we wcześniejszym poście) za łatwe. Mój klient np.
chce, aby program zarobił jak najwięcej pieniędzy i wymagał
jak najmniejszego personelu do jego administracji. Takie
stawia wymagania. A czy mu dostarczę program do grania na
giełdzie, czy serwis do ogłoszeń matrymonialnych to sprawa
drugorzędna.


> Na przykład dodanie funkcji porównującej jako parametru
> dla funkcji "sort" jest generalizowaniem, a jest piekielnie
> precyzyjne.
Dlaczego można precyzyjne generalizować po tejże funkcji, a po
spotykanych kryteriach oceny programu nie można?

>
> > > 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
Myślałem że jak tylko odrzucisz przypadki nonsensowne, to będzie
precyzyjnie.

>
> > > > 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
TO też da się rozwiązać, można uznać za takie same, jeśli eksperci od
razu nie są jednoznaczni - ale nie ma sensu brnąć dalej.

>
> > > 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"
No więc właśnie. Co z tego, że nawet jeśli są jakieś znikome
szanse na udowodnienie poprawności programu, to zwykle nie ma
żadnych szans, czy program, choć jest poprawny, to realizuje
zamierzony cel.


> > > 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ą)
Nie wiem czy jest to możliwe. Dla mnożenia macierzy kwadratowych wszyscy
byli przekonani że dolna granica to N^3 - a okazało się że nie.


> 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.
Oczywiście że może. Przecież to jest bardzo często spotykany
wymóg. Ja np. mam sprzeczne wymogi: program ma być wydajny, ma
obsługiwać bardzo dużą ilość użytkowników na tanim sprzęcie i
jednocześnie ma być bardzo podatny na zmiany, żeby szybko go
rozbudowywać.



> > > 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.
Pytam o to, jakie miałeś na myśli przypadki, gdy pisałeś, że
może dowód być łatwy.

>
> > > > > 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.
Po to jest prawie każda synchronizacja, a jeśli słowo pamięć
zmienimy na zasób, to chyba dosłownie każda.

> Jeśli Cię to bardziej interesuje, polecam kurs z "Heterogenous Parallel
> Programming" na Courserze albo książkę "CUDA w przykładach" (wyd. Helion)
Nie mam aż tyle czasu, myślalem że rzucisz kilka zalet.

>
> > > 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,
Nie pisałem że trzeba ją zabezpieczać semaformai, tylko że trzeba ją
traktować jakby była zabezpieczona według takiego schematu.

> 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.
Nie wiem totalnie o co chodzi. Semafory nigdy nie chronią przed deadlockiem,
chroni właściwa metoda używania semaforów.

Pozdrawiam