🚀 go-pugleaf

piątek, 20 sty, Tomasz Zielonka:
>> Jest to projekt akademicki, robiony w Instytucie Podstaw Informatyki PAN w
>> Sopocie. Kod źródłowy nie jest w tej chwili udostępniany, ale myślę, że nie
>> byłoby z tym problemu.
> Chetnie bym sobie obejrzal.

Postaram się udostępnić źródła w przyszłym tygodniu, dam znać.

>> Sam model matematyczny to hipersieci Petriego. Ma on tę zaletę nad podobnymi
>> formalizmami, że można stosować model checking.
> Slyszalem termin "model checking" wczesniej, ale dopiero teraz
> sprawdzilem, co to jest, i nie jestem pewien, czy rozumiem. Moglbys
> napisac, dlaczego to jest fajne, np. w Waszym zastosowaniu? ;-) Ostatnio
> w mojej pracy coraz czesciej przydaja mi sie takie "akademickie"
> techniki jak np. "partial evaluation", czy "abstract interpretation"
> (jesli dobrze zidentyfikowalem ;-) - moze warto byloby sie i z ta
> zapoznac.

Model checking to algorytm sprawdzania spełnialności formuły logicznej w
systemach ze skończoną liczbą stanów. Najprostszy przykład formuły to np. "w
każdym stanie s zachodzi: s(x) > 0". Naiwna implementacja sprawdzenia
spełnialności tej formuły polegałaby na przejrzeniu wszystkich stanów systemu
i sprawdzeniu, czy ta własność w każdym z nich zachodzi. Jednak istnieją różne
skomplikowane techniki model-checkowania które umożliwiają działanie na
ogromnych systemach, np. o liczbie stanów równej 10^100, co oczywiście nie
jest możliwe przy naiwnych algorytmach.

Inne formuły, które można modelcheckować, to np. "nie istnieje ścieżka
wykonania (ciąg stanów) prowadząca do dead-locku" albo "jeśli s(x) = 0, to w
którymś stanie s' następującym po s zajdzie s'(x) != 0".

Jeżeli chodzi o zastosowania, to model checking jest popularny w
zastosowaniach sprzętowych (bo hardware ma skończoną liczbę stanów i można w
miarę łatwo go opisać w sposób zrozumiały dla algorytmów modelcheckujących), a
nie nadaje się do zwykłych programów (nieskończona lub za duża liczba stanów).

Model checking jest podobny do testowania -- w testowaniu też badamy prawdziwość
jakiejś formuły w danym modelu (systemie), tyle, że dotyczy ona niewielkiego
podzbioru stanów. Model checking jest czymś innym niż specyfikacje formalne,
bo specyfikacja opisuje klasę modeli, a model checking wymaga podania jakiegoś
konkretnego modelu i zbioru formuł, które ten model musi spełniać.

W naszym projekcie model checking jest rzeczą wartościową, bo nasz model
obliczeń mobilnych jest stosunkowo wysokopoziomowy, strukturalny, a przy
takich własnościach niełatwo jest zachować skończoność systemu.

>> Pierwsza wersja naiwnego model checkera została stworzona w Haskellu,
>> jednak w tym wypadku sprawa wydajności okazała się kluczowa, a ciężko
>> robić optymalizacje w leniwym Haskellu czy choćby wnioskować, co się
>> aktualnie oblicza. Sprawa jest dziwna, bo szacując matematycznie ilość
>> potrzebnych obliczeń w pewnym przykładzie nie wychodzi ich dużo, a
>> Haskell oblicza to długo.
> Moze mieliscie space-leak? Najczestsze objawy to duze zuzycie pamieci i
> czas GC dominujacy w czasie dzialania programu.

Nie pamiętam, czy profiler pokazywał jakieś informacje o GC... A powinien?

>> Problemem jest zapewne wielokrotne wykonywanie tych samych obliczeń
>> (dlaczego nie ma prostego sposobu na "function memoization"?!), ale
>> mimo użycia profilera nie udało mi się znaleźć tych kluczowych
>> miejsc...
> Moze poproscie o pomoc na haskell-cafe@haskell.org?

Może powinniśmy. Choć teraz, gdy w planach jest porzucenie tej implementacji,
chyba szkoda na to czasu.

>> Ostatecznie ma być użyty lepszy algorytm modelcheckujący (co nie jest
>> trywialne, bo logika modelu jest niestandardowa), a model checker ma być
>> przepisany na coś imperatywnego (Java...).
> Au! Moze da sie temu jakos zapobiec? ;-)

Oj nie wiem :). Do Javy czy C są zaawansowane biblioteki używane w model
checkingu, do Haskella niby też można je podłączyć (przez jakiś "foreign
interface"), ale przeglądałem artykuł, w którym opisano takie rozwiązanie i
było ono bardzo wolne. A wydajność jest jednak sprawą kluczową... Poza tym
chciałbym mieć kontrolę nad czasem obliczania.

Za to część symulatorowa na pewno pozostanie w Haskellu (co ciekawe nie ma
problemu z wydajnością, mimo, że matematyczna złożoność obliczeń jest grubo
ponad wykładnicza :) ).

>> Gdybym dzisiaj miał decydować o języku implementacji, byłbym za jakimś MLem,
>> bo miałbym tę samą ekspresywność, a język jest bardziej praktyczny (i chyba
>> nawet są jakieś MLe kompilowane do bajtkodu JVM...). Aha, pisząc w Haskellu
>> dosięgła nas następująca zmora: okazało się, że żeby zrobić "coś", trzeba
>> wprowadzić monadę, co wymagałoby przepisania praktycznie całego programu
>> (oczywiście ze zmianą wszystkich typów funkcji włącznie)...
> No coz, zdaza sie. Nigdy nie mialem az tak bolesnego przypadku - moze
> dlatego, ze dosyc szybko zaczynam uzywac monad, tzn. kiedy widze, ze to
> moze ulatwic, a nie dopiero wtedy, kiedy jest juz konieczne.

Moze po prostu mamy za małe doświadczenie w Haskellu.

> PS. Duze masz/macie doswiadczenie w uzywaniu Haskella? Przyznaje,
>     ze mi osiagniecie stanu pozwalajacego wygodnie rozwiazywac
>     typowe praktyczne problemy zajelo chyba ze dwa lata, ale
>     wiem, ze niektorym przychodzi to szybciej.

Ja nie mam za dużego praktycznego doświadczenia. Ten projekt to największa
rzecz, jaką robiłem w języku funkcyjnym. Choć z językami funkcyjnymi zetknąłem
się jeszcze w liceum (dzięki grupom dyskusyjnym, a ściślej - Qrczakowi), a
przez okres studiów nie tracę z nimi kontaktu (nie ma to jak metody numeryczne
w Haskellu :) ). Myślę, że pomogła mi matematyka na studiach (podobny sposób
myślenia o problemie) i takie książki, jak "Struktura i interpretacja
programów komputerowych". Tak więc pisanie symulatora i model checkera było
całkiem przyjemne :).