W ciągu ostatnich 15 lat wielokrotnie czytałem Herlihy i Winga. To bardzo trudna lektura. I to jest niefortunne, ponieważ chociaż wokół krawędzi są pewne subtelności, podstawowy pomysł jest właściwie całkiem rozsądny.
W skrócie: linearyzowalność jest jak serializowanie, ale z dodatkowym wymogiem, aby serializacja szanowała dodatkowe ograniczenia w porządkowaniu między transakcjami. Celem jest umożliwienie ci rygorystycznego uzasadnienia pojedynczej struktury danych atomowych zamiast konieczności jednoczesnego rozumowania całego systemu.
Łatwość uzyskania liniowości jest również łatwa: wystarczy powiązać muteks z obiektem, który chcesz linearyzować. Każda transakcja na tym obiekcie zaczyna się od zablokowania muteksu, a kończy na odblokowaniu muteksu.
Oto definicje, których użyję:
System jest serializowalny, jeśli otrzyma zestaw transakcji na zbiorze danych, każdy wynik wykonania transakcji jest taki sam, jakby transakcje zostały wykonane w jakiejś kolejności sekwencyjnej, a operacje w ramach każdej transakcji są zawarte w ich transakcji w kolejności określone przez kod transakcji.
Możliwość szeregowania uniemożliwia pojawienie się przeplatania operacji między różnymi transakcjami i wymaga, aby wybrane uporządkowanie transakcji spełniało związek przyczynowy (jeśli transakcja A zapisuje wartość x, a transakcja B odczytuje wartość x, którą napisał A, wówczas transakcja A musi poprzedzać transakcję B w wybrane zamówienie szeregowe.) Ale nie mówi nic o jakichkolwiek innych ograniczeniach w porządkowaniu transakcji (w szczególności nie mówi nic o procesach i kolejności, w jakiej procesy postrzegają zdarzenia.)
Istnieje inny pokrewny pomysł, który dodaje ograniczenia dotyczące kolejności wykonywania operacji przez operacje (ale nie mówi o transakcjach tylko o pojedynczych operacjach odczytu / zapisu):
System jest sekwencyjnie spójny, jeśli wynik dowolnego wykonania jest taki sam, jakby operacje wszystkich procesów zostały wykonane w jakiejś kolejności sekwencyjnej, a operacje każdego pojedynczego procesu pojawiają się w tej sekwencji w kolejności określonej przez jego program. ( Lamport, „Jak zrobić komputer wieloprocesorowy, który poprawnie wykonuje programy wieloprocesowe”, IEEE T Comp 28: 9 (690-691), 1979 ).
Definicja spójności sekwencyjnej polega na tym, że akceptujemy tylko zamówienia sekwencyjne, w których dla każdej lokalizacji pamięci (obiektu) indukowana kolejność operacji sekwencyjnych jest zgodna z zasadą, że wartość zwracana przez każdą operację odczytu do lokalizacji xmusi być taka sama, jak wartość zapisana przez bezpośrednio poprzedzająca operacja zapisu do lokalizacji xw kolejności sekwencyjnej.
Linearyzowalność ma dobre intencje (a) połączenie pojęcia transakcji (z serializacji) z koncepcją, że procesy oczekują, że wykonywane przez nich operacje będą wykonywane w kolejności (od spójności sekwencyjnej) oraz (b) zawężenia kryteriów poprawności, aby mówić o każdym z nich obiekt w izolacji, zamiast zmuszać cię do rozumowania całego systemu. (Chciałbym móc powiedzieć, że implementacja mojego obiektu jest poprawna nawet w systemie, w którym istnieją inne obiekty, których nie można linearyzować.) Uważam, że Herlihy i Wing próbowali rygorystycznie zdefiniować monitor .
Część (a) jest „łatwa”: Sekwencyjnym wymogiem podobnym do spójności byłoby, aby transakcje na obiekcie wydawane przez każdy proces pojawiały się w sekwencji wynikowej w kolejności określonej przez program. Wymaganiem podobnym do serializacji byłoby to, że wszystkie transakcje na obiekcie wzajemnie się wykluczają (mogą być serializowane).
Złożoność wynika z celu (b) (możliwość mówienia o każdym obiekcie niezależnie od wszystkich innych).
W systemie z wieloma obiektami możliwe jest, że operacje na obiekcie B nakładają ograniczenia na kolejność, w której, jak wierzymy, operacje zostały wywołane na obiekcie A. Jeśli spojrzymy na całą historię systemu, będziemy ograniczeni do pewnych kolejnych zamówień, i będzie musiał odrzucić innych. Chcieliśmy jednak kryteriów poprawności, które moglibyśmy zastosować w oderwaniu (rozumowanie na podstawie tego, co dzieje się z obiektem A bez odwoływania się do historii globalnego systemu).
Na przykład: załóżmy, że próbuję spierać się o poprawność obiektu A, który jest kolejką, załóżmy, że obiekt B jest lokalizacją pamięci i załóżmy, że mam następujące historie wykonania: Wątek 1: A.enqueue (x), A. dequeue () (zwraca y). Wątek 2: A.enqueue (y), A.dequeue () (zwraca x). Czy istnieje przeplatanie zdarzeń, które pozwoliłyby na poprawne wdrożenie tej kolejki? Tak:
Thread 1 Thread 2
A.enqueue(x) ...
... A.enqueue(y)
... A.dequeue() (returns x)
A.dequeue(y) (returns y) ...
Ale co teraz, jeśli historia (w tym obiekt B ) to: B zaczyna się od wartości 0. Wątek 1: A.enqueue (x), A.dequeue () (zwraca y), B.write (1). Wątek 2: B.read () (zwraca 1) A.enqueue (y), A.dequeue () (zwraca x).
Thread 1 Thread 2
A.enqueue(x) ...
A.dequeue() (returns y) ... (uh oh!)
B.write(1) ...
... B.read() (returns 1)
... A.enqueue(y)
... A.dequeue() (returns x)
Teraz chcielibyśmy, aby nasza definicja „poprawności” mówiła, że ta historia wskazuje, że albo nasza implementacja A jest błędna, albo nasza implementacja B jest błędna, ponieważ nie ma serializacji, która „ma sens” (albo Wątek 2 musi przeczytać wartość z B, która nie została jeszcze napisana lub Wątek 1 musi usunąć wartość z A, która nie została jeszcze zakolejkowana.) Tak więc, podczas gdy nasza pierwotna serializacja transakcji na A wydawała się rozsądna, jeśli nasza implementacja pozwala na historię taką jak druga, wtedy jest ona wyraźnie nieprawidłowa.
Ograniczenia, które dodaje linearyzacja, są więc całkiem rozsądne (i konieczne nawet w przypadku prostych struktur danych, takich jak kolejki FIFO). Są to takie rzeczy: „Twoja implementacja powinna uniemożliwić dequeue () wartość, która nie będzie kolejkowana () do pewnego czasu w przyszłość." Linearyzowalność jest dość łatwa (i naturalna) do osiągnięcia: wystarczy powiązać muteks z obiektem, a każda transakcja rozpoczyna się od zablokowania, a kończy przez odblokowanie. Rozumowanie na temat linearyzowalności zaczyna być trudne, gdy próbujesz zaimplementować swoją atomowość za pomocą nieblokujących lub bezblokujących lub bez czekania technik zamiast prostych muteksów.
Jeśli interesują Cię pewne wskazówki do literatury, znalazłem następujące (chociaż myślę, że dyskusja na temat „czasu rzeczywistego” jest jednym z czerwonych śledztw, które sprawiają, że linearyzacja jest trudniejsza niż powinna.) Https: // stackoverflow.com/questions/4179587/difference-between-linearizability-and-serializability