Udostępnij za pośrednictwem

Dodawanie adnotacji do zachowania blokującego

  • Artykuł

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ż są one nieokreślone. 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_(dst, src) Dodawać adnotacje do funkcji i wskazuje, dst że w stanie post dwa blokady i src, są traktowane tak, jakby były tym samym obiektem blokady, stosując właściwości blokady z src do dst.
_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ć inne specyficzne 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, a wzorce kodowania pozyskiwania zasobów to inicjowanie (RAII) z obsługą move semantyki.

Adnotacja opis
_Analysis_assume_smart_lock_acquired_(lock) Informuje analizatora o założeniu, że został nabyty inteligentny blokada. 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 targetobiektu . 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.

Zobacz też