Metody Bezpiecznego Programowania

Studia stacjonarne II stopnia, kierunek informatyka, specjalność Systemy rozproszone
wykłady: śro. 13:30 @ s. 128-BT, lab.: śro. 9:45, 15:10 @ s. lab. 1.6.18-BT

Prowadzący: dr hab. inż. Paweł T. Wojciechowski, prof. PP
Email: Pawel [dot] T [dot] Wojciechowski [at] cs.put.edu.pl
Administrator sieci lab.: labadmin [w] cs.put.edu.pl

Cel przedmiotu

Przez ostatnie dziesięciolecia obowiązywało prawo Moore'a: wprowadzenie kolejnej nowej generacji procesorów sprawiało, że programy mogły działać szybciej. Te czasy minęły. Układy procesorowe nowych generacji będą miały coraz więcej jednostek CPU, ale każda pojedyncza jednostka nie będzie szybsza od tej z poprzedniego roku (zob. np. Our Manycore Future). Aby programy mogły działać szybciej, koniecznością staje się pisanie programów współbieżnych.

Niestety pisanie poprawnych programów współbieżnych jest zwykle znacząco trudniejsze niż pisanie analogicznych programów sekwencyjnych. Ponieważ programy współbieżne wykonywane są w sposób niedeterministyczny, ich testowanie jest trudne, a wykrycie i usunięcie wszystkich błędów w kodzie nie zawsze możliwe.

W ramach przedmiotu omówione zostaną wybrane współczesne metody i języki bezpiecznego programowania (ang. safe programming), ze szczególnym uwzględnieniem programowania funkcyjnego, współbieżnego i rozproszonego. Cechą charakterystyczną tych metod i języków jest gwarancja braku określonej klasy błędów programistycznych.

Celem przedmiotu jest pokazanie fundamentalnych podstaw bezpiecznego programowania oraz mechanizmów (lub budowy) przykładowych systemów, które w możliwe najlepszy sposób ilustrują poszczególne zagadnienia. Przedmiot nie jest kursem programowania lub użycia tych systemów. Zakładana jest znajomość co najmniej jednego (dowolnego) języka programowania oraz podstaw systemów współbieżnych i rozproszonych.

Krótki opis

Przedyskutowane zostaną zarówno tradycyjne metody synchronizacji, korzystające z monitorów i zamków, jak również metody alternatywne, które oparte są na pamięci transakcyjnej. Pamięć transakcyjna może być realizowana programowo dla danego języka programowania, lub sprzętowo przez procesor (zob. np. Intel Haswell).

Obok nowych metod synchronizacji, omówione zostaną także wybrane metody statycznej detekcji błędów programistycznych. Obejmują one abstrakcje wbudowane w język programowania, tj. przede wszystkim systemy typów, na przykładzie języków programowania fukcyjnego, jak również przykładowe metody służące do weryfikacji poprawności programów współbieżnych.

Przedstawione zostaną także alternatywne narzędzia, języki i środowiska, które wspierają bezpieczeństwo (safety) przez wyręczenie programisty z implementowania operacji trudnych. Przykładem są narzędzia do obliczeń równoległych, oraz nowoczesne języki programowania i środowiska, które łączą przetwarzanie wielowątkowe i rozproszone w jeden spójny mechanizm.

Oprócz prezentacji zagadnień praktycznych omówione zostaną podstawy teoretyczne, np. wybrane modele i własności przetwarzania współbieżnego. Przedstawiony zostanie także model pamięci dla języka Java, który specyfikuje poprawność (legalność) kompilatorów i maszyn wirtualnych, uwzględniając optymalizacje kodu oraz wszystkie możliwe do wyrażenia w danym języku programy współbieżne (w tym niepoprawnie zsynchronizowane).

Sylabus

1. Programowanie współbieżne i synchronizacja na przykładzie monitorów w C#/Java: podstawowe operacje monitorów, prawidłowy dostęp do danych współdzielonych, niezmienniki, poprawne wzorce projektowe, błędne praktyki (np. double-check locking),
   
   
2. Programowanie współbieżne i synchronizacja na przykładzie monitorów w C#/Java: zakleszczenie, zagłodzenie, problemy z efektywnością przy konfliktach na zamkach i odwróceniu priorytetów, zaawansowane problemy synchronizacji i optymalizacje (np. unikanie spurious wake-ups i spurious lock conflicts),
   
   
3. Języki funkcyjne: weryfikacja przez silne typowanie, polimorfizm typów, składanie funkcji, częściowe wykonanie (currying), obiekty funkcyjne (closures), referencje i bezpieczne zarządzanie pamięcią, funkcje anonimowe,
   
   
4. Języki funkcyjne: przykładowe typowane struktury danych, konstrukcje agregacyjne (np. map-reduce czyli mapowanie/odwzorowywanie z redukcją, filtrowanie, oraz folding), dopasowanie do wzorca, poprawna rekurencja (tail recursion),
   
   
5. Poprawność współbieżnego dostępu do obiektów współdzielonych: historie sekwencyjne i współbieżne, własność liniowości (linearizability), przykłady: kolejka FIFO i rejestry, formalizacja i własności liniowości (np. lokalność, blokowanie vs. nieblokowanie),
   
   
6. Dynamiczna detekcja błędów w programowaniu współbieżnym na przykładzie Eraser: relacja happens-before i jej ograniczenia, algorytm lockset do detekcji warunków wyścigu, optymalizacje algorytmu uwzględniające inicjalizację zmiennych, dane współdzielone tylko do odczytu oraz read-write locks,
   
   
7. Warunek wyścigu wysokiego rzędu (high-level data race): definicja, algorytm detekcji, poprawność i kompletność algorytmu (false positives - niepotrzebne ostrzeżenia, false negatives - niezauważone błędy),
   
   
8. Pamięć transakcyjna: warunkowe regiony krytyczne (CCR) i inne konstrukcje językowe, niskopoziomowe operacje pamięci transakcyjnej, implementacja CCR przy użyciu tych operacji, struktura stosu, ownership records i deskryptory transakcji, algorytm atomowego zapisu do pamięci transakcyjnej (na przykładach),
   
   
9. Poprawność programowej pamięci transakcyjnej: klasyczne własności i ich ograniczenia w kontekście pamięci transakcyjnej: liniowość, szeregowalność (serializability), globalna atomowość (niepodzielność) i odtwarzalność (recoverability), model pamięci transakcyjnej, opacity jako własność bezpieczeństwa (safety) pamięci transakcyjnej,
   
   
10. Ograniczenia pamięci transakcyjnej i transakcji: problemy przy zamianie zamków na optymistyczne transakcje, silna vs. słaba atomowość a poprawność programów, problem z metodami natywnymi (operacje nieodwracalne), problem z sekwencyjną kompozycją transakcji, porównanie teoretycznej prędkości wykonania transakcji atomowych i sekcji krytycznych, chwilowe osłabianie atomowości,
    
    
11. Model pamięci na przykładzie języka Java: model pamięci jako specyfikacja poprawnej semantyki programów współbieżnych oraz legalnych implementacji kompilatorów i maszyn wirtualnych, słabość vs. siła modelu pamięci, współczesne ograniczenia klasycznego modelu spójności sekwencyjnej, analiza globalna i optymalizacje kodu, model pamięci happens-before oraz jego słabość, model pamięci uwzględniający circular causality, formalizacja modelu, przykłady kontrowersyjnych transformacji kodu programów,
    
    
12. Bezpieczne programowanie równoległe na przykładzie Cilk (ze wsparciem dla C/C++): abstrakcje programistyczne w Cilk, model obliczeń wielowątkowych w oparciu o graf skierowany acykliczny (DAG), miary wykonania na procesorze wielordzeniowym, szeregowanie zachłanne i górne ograniczenia na czas obliczeń,
    
    
13. Bezpieczne programowanie rozproszone w modelu przesyłania komunikatów: model rozproszonych aktorów (Erlang) lub obiektów (NPict), operacje przesyłania komunikatów wbudowane w język programowania, weryfikacja poprawności komunikacji sieciowej przez typy, mobilność procesów (NPict),