Linearyzacja - Linearizability

W kolorze szarym liniowa podhistoria, procesy rozpoczynające się w b nie mają linearyzowanej historii, ponieważ b0 lub b1 mogą zakończyć się w dowolnej kolejności przed wystąpieniem b2.

W programowaniu współbieżnym operacja (lub zestaw operacji) jest linearyzowana, jeśli składa się z uporządkowanej listy zdarzeń wywołania i odpowiedzi ( callbacków ), która może zostać rozszerzona poprzez dodanie zdarzeń odpowiedzi, takich jak:

  1. Rozszerzona lista może być ponownie wyrażona jako historia sekwencyjna (jest możliwa do serializacji ).
  2. Ta sekwencyjna historia jest podzbiorem oryginalnej nierozszerzonej listy.

Nieformalnie oznacza to, że niezmodyfikowana lista zdarzeń może być linearyzowana wtedy i tylko wtedy, gdy jej wywołania były możliwe do serializacji , ale niektóre odpowiedzi harmonogramu serializacji jeszcze nie powróciły.

W systemie współbieżnym procesy mogą jednocześnie uzyskiwać dostęp do współużytkowanego obiektu. Ponieważ wiele procesów uzyskuje dostęp do jednego obiektu, może zaistnieć sytuacja, w której podczas gdy jeden proces uzyskuje dostęp do obiektu, inny proces zmienia jego zawartość. Ten przykład pokazuje potrzebę linearyzacji. W systemie linearyzowalnym, chociaż operacje na wspólnym obiekcie nakładają się na siebie, każda operacja wydaje się zachodzić natychmiast. Linearyzowalność jest silnym warunkiem poprawności, który ogranicza, jakie dane wyjściowe są możliwe, gdy do obiektu uzyskuje dostęp wiele procesów jednocześnie. Jest to właściwość bezpieczeństwa, która zapewnia, że ​​operacje nie kończą się w nieoczekiwany lub nieprzewidywalny sposób. Jeśli system jest linearyzowalny, pozwala to programiście zrozumieć system.

Historia linearyzowalności

Linearyzacja została po raz pierwszy wprowadzona jako model spójności przez Herlihy i Wing w 1987 roku. Obejmowała ona bardziej restrykcyjne definicje atomu, takie jak „operacja atomowa to taka, która nie może być (lub nie jest) przerwana przez współbieżne operacje”, które zwykle są niejasne na temat kiedy operacja jest uważana za początek i koniec.

Obiekt atomowy może być rozumiany natychmiast i całkowicie na podstawie jego sekwencyjnej definicji, jako zestaw operacji przebiegających równolegle, które zawsze wydają się następować jedna po drugiej; nie mogą pojawić się żadne niespójności. W szczególności, linearyzowalność gwarantuje, że niezmienniki systemu są obserwowane i zachowywane przez wszystkie operacje: jeśli wszystkie operacje indywidualnie zachowują niezmiennik, system jako całość będzie.

Definicja linearyzacji

System współbieżny składa się ze zbioru procesów komunikujących się przez współdzielone struktury danych lub obiekty. Linearyzacja jest ważna w tych współbieżnych systemach, w których do obiektów może mieć dostęp wiele procesów jednocześnie, a programista musi być w stanie wnioskować o oczekiwanych wynikach. Wykonanie współbieżnego systemu skutkuje powstaniem historii , uporządkowanej sekwencji wykonanych operacji.

Historia to sekwencja wywołań i reakcji wykonanych z przedmiotu za pomocą zestawu nici lub procesów. Wywołanie można traktować jako początek operacji, a odpowiedź jako sygnalizowany koniec tej operacji. Każde wywołanie funkcji będzie miało następną odpowiedź. Można to wykorzystać do modelowania dowolnego użycia obiektu. Załóżmy na przykład, że dwa wątki, A i B, próbują chwycić blokadę, wycofując się, jeśli jest już zajęta. Byłoby to modelowane jako oba wątki wywołujące operację blokady, a następnie oba wątki otrzymujące odpowiedź, jedną pomyślnie, a drugą nie.

Wywołuje blokadę B wywołuje blokadę Otrzymuje odpowiedź „nieudana” B otrzymuje odpowiedź „udany”

Sekwencyjny historia jest taka, w której wszystkie wywołania mają natychmiastowe reagowanie; to znaczy, że inwokacja i odpowiedź są uważane za zachodzące natychmiast. Historia sekwencyjna powinna być trywialna do rozumowania, ponieważ nie ma rzeczywistej współbieżności; poprzedni przykład nie był sekwencyjny, a zatem trudno go uzasadnić. Tu właśnie pojawia się linearyzacja.

Historię można linearyzować, jeśli istnieje liniowa kolejność zakończonych operacji taka, że:

  1. Dla każdej zakończonej operacji w , operacja zwraca ten sam wynik w wykonaniu , co operacja zwrócona , gdyby każda operacja została zakończona jeden po drugim w kolejności .
  2. Jeśli operacja op 1 zakończy się (otrzyma odpowiedź) przed rozpoczęciem operacji op 2 (wywoła), to operacja op 1 poprzedza operację 2 w .

Innymi słowy:

  • jego wezwania i odpowiedzi mogą być uporządkowane tak, aby uzyskać sekwencyjną historię;
  • że sekwencyjna historia jest poprawna zgodnie z sekwencyjną definicją obiektu;
  • jeśli odpowiedź poprzedzała wywołanie w oryginalnej historii, nadal musi poprzedzać je w sekwencyjnym przeorganizowaniu.

(Zauważ, że pierwsze dwa punkty tutaj pasują do serializacji : operacje wydają się zachodzić w pewnej kolejności. Jest to ostatni punkt, który jest unikalny dla linearyzowalności, a zatem jest głównym wkładem Herlihy i Wing.)

Przyjrzyjmy się dwóm sposobom zmiany kolejności w powyższym przykładzie blokowania.

Wywołuje blokadę Otrzymuje odpowiedź „nieudana” B wywołuje blokadę B otrzymuje odpowiedź „udany”

Zmiana kolejności wywołania B poniżej odpowiedzi A daje sekwencyjną historię. Łatwo to zrozumieć, ponieważ wszystkie operacje odbywają się teraz w oczywistej kolejności. Niestety, nie jest on zgodny z sekwencyjną definicją obiektu (nie jest zgodny z semantyką programu): A powinien z powodzeniem uzyskać blokadę, a B powinien był następnie przerwać.

B wywołuje blokadę B otrzymuje odpowiedź „udany” Wywołuje blokadę Otrzymuje odpowiedź „nieudana”

To kolejna poprawna historia sekwencyjna. To także linearyzacja! Zauważ, że definicja linearyzowalności wyklucza zmianę kolejności odpowiedzi poprzedzających wywołania; ponieważ pierwotna historia nie miała odpowiedzi przed inwokacjami, możemy zmienić jej kolejność według własnego uznania. Stąd oryginalna historia jest rzeczywiście linearyzowalna.

Obiekt (w przeciwieństwie do historii) jest linearyzowalny, jeśli można zlinearyzować wszystkie ważne historie jego użytkowania. Zauważ, że jest to o wiele trudniejsze do udowodnienia twierdzenie.

Linearyzowalność a serializowalność

Rozważ następującą historię, ponownie dwóch obiektów wchodzących w interakcję z zamkiem:

Wywołuje blokadę Pomyślnie blokuje B wywołuje odblokowanie B pomyślnie odblokowuje Wywołuje odblokowanie Pomyślnie odblokowuje

Ta historia nie jest ważna, ponieważ istnieje punkt, w którym zarówno A, jak i B trzymają zamek; co więcej, nie można go zmienić na prawidłową historię sekwencyjną bez naruszenia reguły porządkowania. Dlatego nie jest linearyzowalny. Jednak w ramach serializacji operacja odblokowania B może zostać przeniesiona przed oryginalną blokadę A, która jest prawidłową historią (zakładając, że obiekt rozpoczyna historię w stanie zablokowanym):

B wywołuje odblokowanie B pomyślnie odblokowuje Wywołuje blokadę Pomyślnie blokuje Wywołuje odblokowanie Pomyślnie odblokowuje

Ta zmiana kolejności jest sensowna pod warunkiem, że nie ma alternatywnych sposobów komunikacji między A i B. Linearyzacja jest lepsza, gdy rozważa się poszczególne obiekty oddzielnie, ponieważ ograniczenia dotyczące zmiany kolejności zapewniają, że wiele obiektów linearyzowalnych, traktowanych jako całość, nadal można linearyzować.

Punkty linearyzacji

Ta definicja linearyzowalności jest równoważna z następującą:

  • Wszystkie wywołania funkcji mają punkt linearyzacji w pewnym momencie między ich wywołaniem a odpowiedzią.
  • Wydaje się, że wszystkie funkcje pojawiają się natychmiast w ich punkcie linearyzacji, zachowując się zgodnie z definicją sekwencyjną.

Ta alternatywa jest zwykle znacznie łatwiejsza do udowodnienia. O wiele łatwiej jest też rozumować jako użytkownik, głównie ze względu na jego intuicyjność. Ta właściwość pojawiania się natychmiast lub niepodzielnie prowadzi do używania terminu atomowy jako alternatywy dla dłuższego „linearyzowalnego”.

W poniższych przykładach punkt linearyzacji licznika zbudowanego na zasadzie porównania i zamiany jest punktem linearyzacji pierwszej (i jedynej) udanej aktualizacji porównania i zamiany. Licznik zbudowany przy użyciu blokowania można uznać za linearyzujący w dowolnym momencie, gdy blokady są utrzymywane, ponieważ wszelkie potencjalnie sprzeczne operacje są wykluczone z uruchamiania w tym okresie.

Pierwotne instrukcje atomowe

Procesory mają instrukcje , które mogą być wykorzystane do realizacji blokowania i blokada telefonu i algorytmy poczekamy darmo . Możliwość tymczasowego wstrzymania przerwań , zapewniająca, że ​​aktualnie uruchomiony proces nie może być przełączany kontekstowo , wystarcza również na uniprocesorze . Instrukcje te są używane bezpośrednio przez twórców kompilatorów i systemów operacyjnych, ale są również abstrakcyjne i udostępniane jako kody bajtowe i funkcje biblioteczne w językach wyższego poziomu:

Większość procesorów zawiera operacje przechowywania, które nie są atomowe w odniesieniu do pamięci. Należą do nich magazyny wielu słów i operacje na ciągach. Jeśli przerwanie o wysokim priorytecie wystąpi, gdy część pamięci zostanie zakończona, operacja musi zostać zakończona po zwróceniu poziomu przerwania. Procedura przetwarzająca przerwanie nie może modyfikować zmienianej pamięci. Ważne jest, aby wziąć to pod uwagę podczas pisania podprogramów przerwań.

Gdy istnieje wiele instrukcji, które muszą być wykonane bez przerw, używana jest instrukcja CPU, która tymczasowo wyłącza przerwania. Musi to być ograniczone tylko do kilku instrukcji, a przerwania muszą być ponownie włączone, aby uniknąć nieakceptowalnego czasu odpowiedzi na przerwania lub nawet utraty przerwań. Ten mechanizm nie jest wystarczający w środowisku wieloprocesorowym, ponieważ każdy procesor może ingerować w proces niezależnie od tego, czy występują przerwania, czy nie. Co więcej, w obecności potoku instrukcji nieprzerywalne operacje stanowią zagrożenie dla bezpieczeństwa, ponieważ mogą potencjalnie zostać połączone w nieskończoną pętlę, tworząc atak typu „odmowa usługi” , jak w przypadku błędu komy Cyrixa .

Standard C i SUSv3 zapewniają sig_atomic_tproste odczyty i zapisy atomowe; nie ma gwarancji, że inkrementacja lub dekrementacja będzie niepodzielna. Bardziej złożone operacje atomowe są dostępne w C11 , który zapewnia stdatomic.h. Kompilatory używają funkcji sprzętowych lub bardziej złożonych metod do implementacji operacji; przykładem jest libatomic GCC.

Zestaw instrukcji ARM zapewnia LDREXi STREXinstrukcje, które mogą być wykorzystane do realizacji atomowego dostępu do pamięci przy użyciu ekskluzywnych monitory zaimplementowane w procesorze śledzenie dostępów pamięci dla konkretnego adresu. Jeśli jednak nastąpi przełączenie kontekstu między wywołaniami LDREXi STREX, dokumentacja zauważa, że STREXzakończy się niepowodzeniem, wskazując, że operacja powinna zostać ponowiona.

Operacje atomowe wysokiego poziomu

Najłatwiejszym sposobem osiągnięcia linearyzowalności jest uruchamianie grup operacji pierwotnych w sekcji krytycznej . Ściśle, niezależne operacje można następnie ostrożnie zezwolić na nakładanie się ich krytycznych sekcji, pod warunkiem, że nie narusza to linearyzowalności. Takie podejście musi zrównoważyć koszt dużej liczby blokad z korzyściami zwiększonej równoległości.

Innym podejściem, preferowanym przez naukowców (ale jeszcze nie szeroko stosowanym w branży oprogramowania), jest zaprojektowanie linearyzowalnego obiektu przy użyciu natywnych prymitywów atomowych dostarczanych przez sprzęt. Ma to potencjał maksymalizacji dostępnej równoległości i minimalizacji kosztów synchronizacji, ale wymaga matematycznych dowodów, które pokazują, że obiekty zachowują się poprawnie.

Obiecującą hybrydą tych dwóch jest zapewnienie abstrakcji pamięci transakcyjnej . Podobnie jak w przypadku sekcji krytycznych, użytkownik zaznacza kod sekwencyjny, który musi być uruchamiany w oderwaniu od innych wątków. Implementacja zapewnia następnie wykonanie kodu niepodzielnie. Ten styl abstrakcji jest powszechny podczas interakcji z bazami danych; na przykład podczas korzystania ze Spring Framework , adnotacja metody za pomocą @Transactional zapewni, że wszystkie zawarte interakcje z bazą danych wystąpią w pojedynczej transakcji bazy danych . Pamięć transakcyjna idzie o krok dalej, zapewniając, że wszystkie interakcje pamięci zachodzą atomowo. Podobnie jak w przypadku transakcji bazodanowych, pojawiają się problemy dotyczące składu transakcji, zwłaszcza transakcji bazodanowych i w pamięci.

Częstym tematem podczas projektowania obiektów linearyzowalnych jest zapewnienie interfejsu typu wszystko albo nic: albo operacja kończy się pomyślnie, albo kończy się niepowodzeniem i nic nie robi. ( Bazy danych ACID odnoszą się do tej zasady jako niepodzielności .) Jeśli operacja nie powiedzie się (zwykle z powodu współbieżnych operacji), użytkownik musi ponowić próbę, zwykle wykonując inną operację. Na przykład:

  • Funkcja Porównaj i zamień zapisuje nową wartość w lokalizacji tylko wtedy, gdy jej zawartość pasuje do dostarczonej starej wartości. Jest to powszechnie używane w sekwencji odczyt-modyfikacja-CAS: użytkownik odczytuje lokalizację, oblicza nową wartość do zapisania i zapisuje ją za pomocą CAS (porównaj i zamień); jeśli wartość zmienia się jednocześnie, CAS nie powiedzie się, a użytkownik spróbuje ponownie.
  • Load-link/store-conditional koduje ten wzorzec w bardziej bezpośredni sposób: użytkownik odczytuje lokalizację za pomocą load-link, oblicza nową wartość do zapisania i zapisuje ją za pomocą store-conditional; jeśli wartość zmieniła się jednocześnie, SC (warunkowe przechowywanie) zakończy się niepowodzeniem i użytkownik spróbuje ponownie.
  • W transakcji bazy danych , jeśli transakcja nie może zostać zakończona z powodu współbieżnej operacji (np. w przypadku zakleszczenia ), transakcja zostanie przerwana i użytkownik będzie musiał spróbować ponownie.

Przykłady linearyzacji

Liczniki

Aby zademonstrować moc i konieczność linearyzowalności, rozważymy prosty licznik, który mogą się zwiększać w różnych procesach.

Chcielibyśmy zaimplementować obiekt licznika, do którego dostęp ma wiele procesów. Wiele popularnych systemów wykorzystuje liczniki do śledzenia, ile razy wystąpiło zdarzenie.

Do obiektu licznika można uzyskać dostęp przez wiele procesów i ma dwie dostępne operacje.

  1. Przyrost - dodaje 1 do wartości zapisanej w liczniku, zwraca potwierdzenie
  2. Odczyt - zwraca bieżącą wartość zapisaną w liczniku bez jej zmiany.

Spróbujemy zaimplementować ten obiekt licznika za pomocą wspólnych rejestrów

Nasza pierwsza próba, którą zobaczymy, jest nielinearyzowana, ma następującą implementację z wykorzystaniem jednego wspólnego rejestru wśród procesów.

Nieatomowe

Naiwna, nieatomowa implementacja:

Przyrost:

  1. Odczytaj wartość w rejestrze R
  2. Dodaj jeden do wartości
  3. Zapisuje nową wartość z powrotem do rejestru R

Czytać:

Odczytaj rejestr R

Ta prosta implementacja nie podlega linearyzacji, jak pokazano w poniższym przykładzie.

Wyobraź sobie, że dwa procesy uzyskują dostęp do obiektu pojedynczego licznika, który ma wartość 0:

  1. Pierwszy proces odczytuje wartość w rejestrze jako 0.
  2. Pierwszy proces dodaje jeden do wartości, wartość licznika powinna wynosić 1, ale zanim zakończy zapisywanie nowej wartości z powrotem do rejestru, może zostać zawieszony, podczas gdy drugi proces jest uruchomiony:
  3. Drugi proces odczytuje wartość w rejestrze, która wciąż jest równa 0;
  4. Drugi proces dodaje jeden do wartości;
  5. drugi proces zapisuje nową wartość do rejestru, rejestr ma teraz wartość 1.

Drugi proces został zakończony, a pierwszy proces kontynuuje działanie od miejsca, w którym został przerwany:

  1. Pierwszy proces zapisuje 1 do rejestru, nie wiedząc, że drugi proces zaktualizował już wartość w rejestrze do 1.

W powyższym przykładzie dwa procesy wywołały polecenie inkrementacji, jednak wartość obiektu wzrosła tylko z 0 do 1, zamiast 2, jak powinno. Jedna z operacji przyrostowych została utracona w wyniku braku linearyzacji systemu.

Powyższy przykład pokazuje potrzebę dokładnego przemyślenia implementacji struktur danych oraz tego, jak linearyzacja może wpłynąć na poprawność systemu.

Atomowy

Aby zaimplementować obiekt licznika linearyzowalnego lub licznika atomowego, zmodyfikujemy naszą poprzednią implementację tak, aby każdy proces P i używał własnego rejestru R i

Każdy proces inkrementuje i odczytuje zgodnie z następującym algorytmem:

Przyrost:

  1. Odczytaj wartość w rejestrze R i .
  2. Dodaj jeden do wartości.
  3. Zapisz nową wartość z powrotem do R i

Czytać:

  1. Odczytaj rejestry R 1, R 2, ... R n .
  2. Zwróć sumę wszystkich rejestrów.

Ta implementacja rozwiązuje problem z naszą oryginalną implementacją. W tym systemie operacje przyrostowe są linearyzowane na etapie zapisu. Punkt linearyzacji operacji inkrementacji występuje wtedy, gdy ta operacja zapisuje nową wartość w swoim rejestrze R i. Operacje odczytu są linearyzowane do punktu w systemie, gdy wartość zwracana przez odczyt jest równa sumie wszystkich wartości przechowywanych w każdym rejestrze Ri .

To trywialny przykład. W rzeczywistym systemie operacje mogą być bardziej złożone, a wprowadzone błędy niezwykle subtelne. Na przykład odczyt 64-bitowej wartości z pamięci może być faktycznie zaimplementowany jako dwa sekwencyjne odczyty dwóch 32-bitowych lokalizacji pamięci. Jeśli proces odczytał tylko pierwsze 32 bity, a przed odczytaniem kolejnych 32 bitów wartość w pamięci zostanie zmieniona, nie będzie miał ani wartości oryginalnej, ani nowej wartości, ale wartość pomieszaną.

Ponadto konkretna kolejność, w jakiej przebiegają procesy, może zmieniać wyniki, co utrudnia wykrycie, odtworzenie i debugowanie takiego błędu .

Porównaj i zamień

Większość systemów zapewnia atomową instrukcję porównania i zamiany, która odczytuje z lokalizacji pamięci, porównuje wartość z „oczekiwaną” podaną przez użytkownika i zapisuje „nową” wartość, jeśli obie pasują, zwracając, czy aktualizacja się powiodła . Możemy to wykorzystać do naprawienia algorytmu licznika nieatomowego w następujący sposób:

  1. Odczytaj wartość w komórce pamięci;
  2. dodaj jeden do wartości;
  3. użyj funkcji porównania i zamiany, aby zapisać z powrotem zwiększoną wartość;
  4. spróbuj ponownie, jeśli wartość odczytana przez funkcję porównania i zamiany nie pasuje do wartości, którą pierwotnie odczytaliśmy.

Ponieważ porównanie i zamiana następuje (lub wydaje się występować) natychmiast, jeśli inny proces zaktualizuje lokalizację, gdy jesteśmy w toku, porównanie i zamiana na pewno się nie powiedzie.

Pobieranie i zwiększanie

Wiele systemów zapewnia atomową instrukcję pobierania i zwiększania, która odczytuje z lokalizacji pamięci, bezwarunkowo zapisuje nową wartość (stara wartość plus jeden) i zwraca starą wartość. Możemy to wykorzystać do naprawienia algorytmu licznika nieatomowego w następujący sposób:

  1. Użyj funkcji pobierania i zwiększania, aby odczytać starą wartość i zapisać z powrotem zwiększoną wartość.

Korzystanie z funkcji pobierania i zwiększania jest zawsze lepsze (wymaga mniejszej liczby odwołań do pamięci) w przypadku niektórych algorytmów — takich jak pokazany tutaj — niż porównywanie i zamienianie, chociaż Herlihy wcześniej udowodniła, że ​​porównywanie i zamienianie jest lepsze w przypadku niektórych innych algorytmów, które nie można w ogóle zaimplementować przy użyciu tylko funkcji pobierania i zwiększania. Tak więc projekty procesorów z zarówno pobieraniem i zwiększaniem, jak i porównywaniem i zamianą (lub równoważnymi instrukcjami) mogą być lepszym wyborem niż te z tylko jednym lub drugim.

Zamykający

Innym podejściem jest przekształcenie naiwnego algorytmu w sekcję krytyczną , zapobiegającą zakłócaniu go przez inne wątki za pomocą blokady . Po raz kolejny naprawiam algorytm licznika nieatomowego:

  1. Uzyskaj blokadę, wykluczając inne wątki z uruchamiania sekcji krytycznej (kroki 2–4) w tym samym czasie;
  2. odczytać wartość w komórce pamięci;
  3. dodaj jeden do wartości;
  4. zapisz zwiększoną wartość z powrotem do komórki pamięci;
  5. zwolnić blokadę.

Ta strategia działa zgodnie z oczekiwaniami; blokada uniemożliwia innym wątkom aktualizowanie wartości, dopóki nie zostanie zwolniona. Jednak w porównaniu z bezpośrednim użyciem operacji atomowych może to ucierpieć ze względu na znaczne obciążenie z powodu rywalizacji o blokadę. Aby poprawić wydajność programu, dobrym pomysłem może być zatem zastąpienie prostych sekcji krytycznych operacjami atomowymi w celu synchronizacji bez blokowania (tak jak właśnie zrobiliśmy dla licznika z funkcją porównywania i zamiany oraz pobierania i zwiększania), zamiast na odwrót, ale niestety nie gwarantuje się znaczącej poprawy, a algorytmy bez blokad mogą łatwo stać się zbyt skomplikowane, aby były warte wysiłku.

Zobacz też

Bibliografia

Dalsza lektura