Wpisz system wydajności

Czy istnieją systemy (statyczne), które próbują sformalizować charakterystykę wydajności programów? Nie mogę znaleźć takich prób.

Ponieważ systemy typów są (jednym z) najpotężniejszych narzędzi w arsenale programisty do wypowiadania się na temat programów, a ponieważ istnieje wiele przypadków, w których wydajność ma krytyczne znaczenie, nie wydaje się, aby wyobrażenie o próbach podjęcia utwórz system typów, który będzie próbował sformułować przynajmniej niektóre informacje na temat cech pamięci i czasu działania programów.

language-design

— Klaas van Schelven
źródło

Co powiedziałby Twój typ systemu na temat wydajności if condition then expensive_operation else cheap_operation?

— sick

Wiem, że pojawiły się zmiany w stosowaniu interpretacji abstrakcyjnej do automatycznego wnioskowania o złożoności kodu w najgorszym przypadku (i terminacji). Możesz być tym zainteresowany ...

— Bakuriu

Nie w pełni powiązane, ale nadal: kernelnewbies.org/FAQ/LikelyUnlikely W kompilatorze jądra Linux / gcc prawdopodobnie / mało prawdopodobne są makra optymalizujące określone ścieżki. Np.if (likely(operation_went_fine)) { // Do something } else if (unlikely(error_occured)) { // Do something else }

— AmazingDreams,

Przychodzą mi na myśl zmienne i rejestrujące słowa kluczowe w C.

— mattnz

Odpowiedzi:

Można sobie wyobrazić system typów na tyle zaawansowany, aby był powiązany z WCET lub złożonością programu. Następnie problemem jest stworzenie analizatora typu dźwięku (lub kontrolera) - tj. Reguł pisania - aby było to możliwe, i zaimplementowanie go na tyle skutecznie, aby uczynić je dość użytecznym.

Większość systemów typów jest na tyle prosta, że można je szybko obliczyć w praktyce (przynajmniej dla rozsądnego zestawu programów, które ludzki programista mógłby ręcznie napisać).

Niektóre akademickie języki programowania (np. AGDA ) mają bardzo wyrafinowane systemy typu, które są pełne Turinga, więc ich kompilator może zająć dużo czasu (być może nieskończonej).

(Jeśli dobrze rozumiem, praca doktora Jérémie Salvucciego na LIP6 w Paryżu jest dość związana z twoim pytaniem; wysłałem mu wiadomość e-mail na ten temat; możesz poszukać regionów i typów ...).

Bądź jednak świadomy twierdzenia Rice'a i problemu Haltinga . Systemy typów mogą nie zawsze być srebrną kulą, jaką możesz chcieć (patrz stara książka bez srebrnej kuli ).

— Basile Starynkevitch
źródło

WCET to „Najgorszy czas wykonania sprawy” w tym kontekście (na wypadek, gdyby ktoś inny niż ja się zastanawiał)

— Klaas van Schelven

Zależnie pisane języki, takie jak Agda, Coq, Epigram, Guru, Isabelle itp. „Rozwiązują” problem zatrzymania, twierdzenie Rice'a i przyjaciół, nie będąc kompletnym Turingiem. Albo przez konstrukcję (tzn. Po prostu nie jest możliwe napisanie nieskończonej pętli / nie kończącej się rekurencji), wymagając, aby wszystkie programy były napisane w taki sposób, aby moduł sprawdzania zakończenia mógł udowodnić zakończenie, lub wymagając od programisty przedstawienia dowód na zakończenie sprawdzane maszynowo.

— Jörg W Mittag

Wydaje się, że niezwykle możliwe jest stworzenie systemu typów, który kategoryzuje charakterystykę wydajnościową typów(np. „szybki / wolny dla dostępu szeregowego,„ szybki / wolny dla dostępu losowego ”,„ efektywna / nieefektywna pamięć ”). Te cechy mogą być abstrakcyjnymi typami umieszczonymi w hierarchii w taki sposób, że odziedziczą po nich bardziej konkretne typy. Jednak wydajność każdego programu używającego tych typów zależy od sposobu, w jaki są one faktycznie używane / uzyskiwane. Aby system typów mógł wydawać oświadczenia o samym programie, użycie (dostępu do) tych typów musiałoby być reprezentowane jako typy Oznaczałoby to rezygnację z korzystania z wbudowanych struktur kontrolnych (np. Pętli for / while) i zamiast tego stosowanie typów, które je implementują. Stąd hierarchia mogłaby mieć abstrakcyjny typ dostępu szeregowego i listę potomną dostępu szeregowego, drzewo szeregowy rodzaje dostępu i tak dalej.Efektywność użytkowania może być co najmniej częściowo wyrażona przez połączenie i zastosowanie tych typów względem siebie.

W funkcjonalnym języku, takim jak Haskell - który i tak prawie nie ma struktur kontrolnych - wydaje mi się to dość praktyczne i wykonalne. W Javie, jednak takie System A wydaje się znacznie mniej osiągalne (nie tak dużo z realizacji począwszy od wykonalności / wiarygodności wyniku).

Haskell już pozwala nam definitywnie stwierdzić, ile programów jest czyste i zapewnia sposoby ograniczania określonych działań w zapieczętowanych skrzynkach. Ponieważ równoległość / współbieżność w Haskell jest zaimplementowana przez system typów , można argumentować, że jest już częścią drogi (do tego, czego chcesz). W przeciwieństwie do tego, imperatywne języki (nawet te o typie statycznym, takie jak Java) oferują koderowi wiele, wiele sposobów na obalenie każdej próby tego.

— itsbruce
źródło