Jest to znakomity, znany na całym świecie podręcznik dotyczący
programowania współbieżnego i rozproszonego.
Autor rozpoczyna wykład od przedstawienia klasycznych problemów
współbieżności i podstawowych mechanizmów synchronizacyjnych procesów. Potem
przechodzi do omówienia problemu wzajemnego wykluczania i zagadnień związanych z
weryfikacją programów współbieżnych. Opisuje algorytm piekarniany i mechanizmy
synchronizacyjne w modelu ze wspólną pamięcią i w modelu bez wspólnej pamięci oraz
klasyczne algorytmy rozproszone i systemy czasu rzeczywistego . Każdy rozdział kończy
się zestawem ćwiczeń do samodzielnego rozwiązania.
Podręcznik ten jest przeznaczony dla studentów informatyki na wszystkich uczelniach
wyższych, programistów i projektantów systemów informatycznych.
Spis treści:
Przedmowa
Rozdział 1. Co to jest programowanie współbieżne?
1.1. Wprowadzenie
1.2. Współbieżność jako abstrakcja równoległości Wielozadaniowość
1.3. Terminologia współbieżności
1.4. Komputery zwielokrotnione
1.5. Zadania programowania współbieżnego
Rozdział 2. Abstrakcja programowania współbieżnego
2.1. Rola abstrakcji
2.2. Wykonanie współbieżne jako przeplot instrukcji
atomowych
2.3. Uzasadnienie przyjętej abstrakcji
2.4. Dowolny przeplot
2.5. Instrukcje atomowe
2.6. Poprawność
2.7. Uczciwość
2.8. Rozkazy maszynowe"4
2.9. Zmienne ulotne i
nieatomowe"4
2.10. Symulator współbieżności
BACIL
2.11. Współbieżność w języku
AdaL
2.12. Współbieżność w języku
JavaL
2.13. Współbieżność w języku PromelaL
2.14. Dodatek: diagram stanów pewnej zagadki
Rozdział 3. Probierń wzajemnego wykluczania
3.1. Wprowadzenie
3.2. Sformułowanie problemu
3.3. Pierwsza próba
3.4. Dowodzenie poprawności za pomocą diagramów
stanów
3.5. Poprawność pierwszej próby
3.6. Druga próba
3.7. Trzecia próba
3.8. Czwarta próba
3.9. Algorytm Dekkera
3.10. Złożone instrukcje atomowe
Rozdział 4. Weryfikacja poprawności programów współbieżnych
4.1. Specyfikacja własności poprawności w języku
logiki
4.2. Indukcyjne dowody niezmienników
4.3. Podstawowe pojęcia logiki temporalnej
4.4. Zaawansowane pojęcia logiki temporalnej^
4.5. Dedukcyjny dowód poprawności algorytmu DekkeraA
4.6. Weryfikacja przez model
4.7. Język modelowania Promela w systemie SpinL
4.8. Weryfikacja warunków poprawności w systemie SpinL
4.9. Wybór techniki weryfikacji^
Rozdział 5. Złożone algorytmy rozwiązywania problemu wzajemnego
wykluczania
5.1. Algorytm piekarniany
5.2. Algorytm piekarniany dla wielu procesów
5.3. Mniej restrykcyjne modele współbieżności
5.4. Algorytmy szybkie
5.5. Implementacje w języku PromelaL
Rozdział 6. Semafory
6.1. Stany procesu
6.2. Definicja typu semaforowego
6.3. Problem wzajemnego wykluczania dla dwóch procesów
6.4. Niezmienniki semaforów
6.5. Problem wzajemnego wykluczania dla N
procesów
6.6. Problemy wymagające synchronizacji kolejności wykonywania
6.7. Problem producenta-konsumenta
6.8. Definicje semaforów
6.9. Problem pięciu filozofów
6.10. Symulacja Barza semaforów ogólnych'4
6.11. Algorytm Uddinga bez zagłodzeń"4
6.12. Semafory w BACIL
6.13. Semafory w języku Ada^
6.14. Semafory w języku ,TavaL
6.15. Semafory w języku PromelaL
Rozdział 7. Monitory
7.1. Wprowadzenie
7.2. Deklaracja i użycie monitorów
7.3. Zmienne warunkowe
7.4. Problem producenta-konsumenta
7.5. Wymaganie natychmiastowego wznowienia
wykonania
7.6. Problem czytelników i pisarzy
7.7. Poprawność algorytmu czytelników i pisarzy^4
7.8. Monitorowe rozwiązanie problemu pięciu filozofów
7.9. Monitory w symulatorze BACI
7.10. Obiekty chronione
7.11. Monitory w języku Jaya^1
7.12. Symulacja monitorów w Promeli7'
Rozdział 8. Kanały
8.1. Modele komunikacji
8.2. Kanały
8.3. Równoległe mnożenie macierzy
8.4. Rozwiązanie problemu pięciu filozofów za pomocą
kanałów
8.5. Kanały w języku PromelaL
8.6. Randki
8.7. Zdalne wywołania procedur"4
Rozdział 9. Przestrzenie
9.1. Model współbieżności stosowany w języku Linda
9.2. Wyrażalność modelu w języku Linda
9.3. Parametry formalne
9.4. Wzorzec nadzorca-robotnik
9.5. Implementacje przestrzeni krotekL
Rozdział 10. Algorytmy rozproszone
10.1. Model systemu rozproszonego
10.2. Implementacje
10.3. Wzajemne wykluczanie rozproszone
10.4. Poprawność algorytmu Ricarta-Agrawali
10.5. Algorytm RA w języku PromelaL
10.6. Algorytmy przekazywania żetonu
10.7. Żetony w drzewach
wirtualnych^1
Rozdział 11. Własności globalne
11.1. Rozproszone zakończenie wykonania
11.2. Algorytm Dijkstry-Scholtena
11.3. Algorytmy windykacyjne
11.4. Migawki
Rozdział 12. Uzgadnianie
12.1. Wprowadzenie
12.2. Sformułowanie problemu
12.3. Algorytm jednorundowy
12.4. Algorytm bizantyjskich generałów
12.5. Załamania
12.6. Drzewa wiedzy
12.7. Awarie bizantyjskie z trzema generałami
12.8. Awarie bizantyjskie z czterema generałami
12.9. Algorytm rozpływowy
12.10. Algorytm króla
12.11. Brak rozwiązania w przypadku trzech
generałów^1
Rozdział 13. Systemy czasu rzeczywistego
13.1. Wprowadzenie
13.2. Definicje
13.4. Niezawodność i powtarzalność
13.5. Systemy synchroniczne
13.6. Systemy asynchroniczne
13.7. Systemy sterowane przerwaniami
13.8. Odwrócenie i dziedziczenie priorytetów
13.9. Specyfikacja sondy Mars Pathfmder w systemie Spin-6
13.10. Algorytm Simpsona"4
13.11. Profil RavenscarL
13.12. UPPAALL
13.13. Algorytmy szeregowania dla systemów czasu rzeczywistego
Dodatek A. Pseudokod
Dodatek B. Podstawowe pojęcia logiki matematycznej
B.l. Rachunek zdań
B.2. Indukcja
B.3. Metody dowodzenia
B.4. Poprawność programów sekwencyjnych
Dodatek C. Problemy programowania współbieżnego
Dodatek D. Narzędzia programistyczne
D.l. Symulatory BACI oraz jBACI
D.2. Systemy Spin oraz jSpin
D.3. System DAJ
Dodatek E. Dalsza lektura
Bibliografia
Skorowidz
332 strony, oprawa miękka
