Dodawanie adnotacji do zachowania blokującego

Artykuł
10/12/2023

Aby uniknąć błędów współbieżności w programie wielowątkowym, zawsze postępuj zgodnie z odpowiednią dyscypliną blokującą i używaj adnotacji SAL.

Błędy współbieżności są notorycznie trudne do odtworzenia, diagnozowania i debugowania, ponieważ nie są deterministyczne. Rozumowanie dotyczące przeplatania wątków jest w najlepszym razie trudne i staje się niepraktyczne podczas projektowania treści kodu, który ma więcej niż kilka wątków. W związku z tym dobrym rozwiązaniem jest przestrzeganie dyscypliny blokującej w programach wielowątkowe. Na przykład przestrzeganie porządku blokady podczas uzyskiwania wielu blokad pomaga uniknąć zakleszczenia, a uzyskanie odpowiedniej blokady ochrony przed uzyskaniem dostępu do udostępnionego zasobu pomaga zapobiec warunkom wyścigu.

Niestety, pozornie proste zasady blokowania mogą być zaskakująco trudne do zastosowania w praktyce. Podstawowym ograniczeniem w dzisiejszych językach programowania i kompilatorach jest to, że nie obsługują one bezpośrednio specyfikacji i analizy wymagań współbieżności. Programiści muszą polegać na nieformalnych komentarzach kodu, aby wyrazić swoje intencje dotyczące sposobu korzystania z blokad.

Adnotacje SAL współbieżności zostały zaprojektowane w celu ułatwienia określania skutków ubocznych blokowania, blokowania odpowiedzialności, ochrony danych, hierarchii kolejności blokady i innych oczekiwanych zachowań blokowania. Dzięki jawności niejawnych reguł adnotacje współbieżności SAL zapewniają spójny sposób dokumentowania sposobu korzystania z reguł blokowania w kodzie. Adnotacje współbieżności zwiększają również możliwości narzędzi do analizy kodu w celu znajdowania warunków wyścigu, zakleszczeń, niezgodnych operacji synchronizacji i innych subtelnych błędów współbieżności.

Ogólne wskazówki

Używając adnotacji, można określić kontrakty, które są implikowane przez definicje funkcji między implementacjami (wywoływanymi) i klientami (wywołującymi). Można również wyrazić niezmienne i inne właściwości programu, które mogą dodatkowo poprawić analizę.

Sal obsługuje wiele różnych rodzajów blokowania elementów pierwotnych — na przykład sekcje krytyczne, muteksy, blokady spin i inne obiekty zasobów. Wiele adnotacji współbieżności bierze wyrażenie blokady jako parametr. Zgodnie z konwencją blokada jest oznaczona wyrażeniem ścieżki bazowego obiektu blokady.

Niektóre reguły własności wątków, które należy wziąć pod uwagę:

Blokady spin są nierozliczone blokady, które mają wyraźną własność wątku.
Sekcje mutexes i krytyczne są zliczane blokady, które mają wyraźną własność wątku.
Semaphores i zdarzenia są zliczane blokady, które nie mają wyraźnej własności wątku.

Blokowanie adnotacji

W poniższej tabeli wymieniono adnotacje blokujące.

Adnotacja	opis
`_Acquires_exclusive_lock_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie post funkcja zwiększa się o jedną wyłączną liczbę blokad obiektu blokady o nazwie przez `expr`.
`_Acquires_lock_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie post funkcja zwiększa się o jedną liczbę blokad obiektu blokady o nazwie przez `expr`.
`_Acquires_nonreentrant_lock_(expr)`	Uzyskana jest blokada o nazwie by `expr` . Jeśli blokada jest już przechowywana, zgłaszany jest błąd.
`_Acquires_shared_lock_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie post funkcja zwiększa się o jedną współdzieloną liczbę blokad obiektu blokady o nazwie przez `expr`.
`_Create_lock_level_(name)`	Instrukcja, która deklaruje symbol `name` jako poziom blokady, dzięki czemu może być używana w adnotacjach `_Has_Lock_level_` i `_Lock_level_order_`.
`_Has_lock_kind_(kind)`	Dodawać adnotacje do dowolnego obiektu, aby uściślić informacje o typie obiektu zasobu. Czasami typ wspólny jest używany dla różnych rodzajów zasobów, a przeciążony typ nie jest wystarczający do odróżnienia wymagań semantycznych między różnymi zasobami. Oto lista wstępnie zdefiniowanych `kind` parametrów: `_Lock_kind_mutex_` Identyfikator typu blokady dla mutexes. `_Lock_kind_event_` Identyfikator typu blokady dla zdarzeń. `_Lock_kind_semaphore_` Identyfikator typu blokady dla semaforów. `_Lock_kind_spin_lock_` Identyfikator typu blokady dla blokad spin. `_Lock_kind_critical_section_` Identyfikator typu blokady dla sekcji krytycznych.
`_Has_lock_level_(name)`	Dodaje adnotację do obiektu blokady i nadaje mu poziom blokady .`name`
`_Lock_level_order_(name1, name2)`	Instrukcja, która daje kolejność blokady między `name1` i `name2`. Blokady, które mają poziom `name1` , należy uzyskać przed blokadami, które mają poziom `name2`.
`_Post_same_lock_(expr1, expr2)`	Dodawać adnotacje do funkcji i wskazuje, `expr1` że w stanie post dwa blokady i `expr2`, są traktowane tak, jakby były tym samym obiektem blokady.
`_Releases_exclusive_lock_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie post funkcja dekrementuje jedną wyłączną liczbę blokad obiektu blokady o nazwie przez `expr`.
`_Releases_lock_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie post funkcja dekrementuje jedną liczbę blokad obiektu blokady o nazwie przez `expr`.
`_Releases_nonreentrant_lock_(expr)`	Blokada o nazwie by `expr` została zwolniona. Jeśli blokada nie jest obecnie przechowywana, zgłaszany jest błąd.
`_Releases_shared_lock_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie post funkcja dekrementuje przez jedną współdzieloną liczbę blokad obiektu blokady o nazwie przez `expr`.
`_Requires_lock_held_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie wstępnym liczba blokad obiektu, który jest nazwany przez `expr` , jest co najmniej jeden.
`_Requires_lock_not_held_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie wstępnym liczba blokad obiektu o nazwie `expr` by wynosi zero.
`_Requires_no_locks_held_`	Dodawać adnotacje do funkcji i wskazuje, że liczba blokad wszystkich blokad, które są znane kontrolerowi, są zerowe.
`_Requires_shared_lock_held_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie wstępnym liczba udostępnionych blokad obiektu, który jest nazwany przez `expr` , jest co najmniej jeden.
`_Requires_exclusive_lock_held_(expr)`	Dodawać adnotacje do funkcji i wskazuje, że w stanie wstępnym liczba wyłącznych blokad obiektu, który jest nazwany przez `expr` , jest co najmniej jeden.

Funkcje wewnętrzne SAL dla obiektów nieeksponowanych blokujących

Niektóre obiekty blokady nie są widoczne przez implementację skojarzonych funkcji blokowania. W poniższej tabeli wymieniono zmienne wewnętrzne SAL, które umożliwiają adnotacje na funkcjach działających na tych nieeksponowanych obiektach blokady.

Adnotacja	opis
`_Global_cancel_spin_lock_`	Opisuje blokadę anulowania spin.
`_Global_critical_region_`	Opisuje region krytyczny.
`_Global_interlock_`	Opisuje operacje połączone.
`_Global_priority_region_`	Opisuje region priorytetu.

Adnotacje dostępu do danych udostępnionych

W poniższej tabeli wymieniono adnotacje dotyczące dostępu do danych udostępnionych.

Adnotacja	opis
`_Guarded_by_(expr)`	Donotuje zmienną i wskazuje, że za każdym razem, gdy jest uzyskiwany dostęp do zmiennej, liczba blokad obiektu blokady o nazwie by `expr` jest co najmniej jedna.
`_Interlocked_`	Dodawanie adnotacji do zmiennej i jest równoważne .`_Guarded_by_(_Global_interlock_)`
`_Interlocked_operand_`	Parametr funkcji z adnotacjami jest docelowym operandem jednego z różnych funkcji połączonych. Te operandy muszą mieć określone dodatkowe właściwości.
`_Write_guarded_by_(expr)`	Donotuje zmienną i wskazuje, że za każdym razem, gdy zmienna zostanie zmodyfikowana, liczba blokad obiektu blokady o nazwie by `expr` jest co najmniej jedna.

Inteligentne blokady i adnotacje RAII

Inteligentne blokady zwykle opakowują natywne blokady i zarządzają ich okresem istnienia. W poniższej tabeli wymieniono adnotacje, których można używać z inteligentnymi blokadami i wzorcami kodowania RAII z obsługą move semantyki.

Adnotacja	opis
`_Analysis_assume_smart_lock_acquired_(lock)`	Informuje analizatora, aby zakładał, że nabyto inteligentną blokadę. Ta adnotacja oczekuje typu blokady odwołania jako parametru.
`_Analysis_assume_smart_lock_released_(lock)`	Informuje analizatora o założeniu, że blokada inteligentna została zwolniona. Ta adnotacja oczekuje typu blokady odwołania jako parametru.
`_Moves_lock_(target, source)`	Opisuje operację `move constructor` , która transferuje stan blokady z `source` obiektu do `target`obiektu . Obiekt `target` jest uważany za nowo skonstruowany obiekt, więc każdy stan, który miał wcześniej, zostanie utracony i zastąpiony przez `source` stan. Element `source` jest również resetowany do stanu czystego bez liczników blokad ani elementu docelowego aliasu, ale aliasy wskazujące, że pozostają niezmienione.
`_Replaces_lock_(target, source)`	Opisuje `move assignment operator` semantyka, w której blokada docelowa jest zwalniana przed przeniesieniem stanu ze źródła. Można go traktować jako kombinację `_Moves_lock_(target, source)` poprzedzoną elementem `_Releases_lock_(target)`.
`_Swaps_locks_(left, right)`	Opisuje standardowe `swap` zachowanie, które zakłada, że obiekty `left` i `right` wymieniają ich stan. Wymiana stanu obejmuje liczbę blokad i element docelowy aliasu, jeśli istnieje. Aliasy wskazujące `left` obiekty i `right` pozostają niezmienione.
`_Detaches_lock_(detached, lock)`	Opisuje scenariusz, w którym typ otoki blokady umożliwia skojarzenie z zawartym zasobem. Podobnie jak `std::unique_ptr` w przypadku jego wewnętrznego wskaźnika: umożliwia programistom wyodrębnianie wskaźnika i pozostawienie kontenera inteligentnego wskaźnika w czystym stanie. Podobna logika jest obsługiwana przez `std::unique_lock` i może być implementowana w niestandardowych otoki blokad. Odłączona blokada zachowuje swój stan (liczba blokad i element docelowy aliasu, jeśli istnieje), podczas gdy otoka jest resetowana tak, aby zawierała zerową liczbę blokad i bez elementu docelowego aliasu, zachowując przy tym własne aliasy. Nie ma operacji na liczbach blokad (zwalnianie i uzyskiwanie). Ta adnotacja zachowuje się dokładnie tak samo, jak `_Moves_lock_` tylko, że odłączony argument powinien być `return` zamiast `this`.

Udostępnij przez