Аннотация поведения блокировки

Статья
04/03/2023

Во избежание ошибок параллелизма в многопоточных программах, всегда выполняйте соответствующую дисциплину блокировок и используйте заметки SAL.

Ошибки параллелизма, как известно, трудно воспроизвести, диагностировать и отладку, так как они не детерминированные. При проектировании текста кода, имеющего более чем несколько потоков, в лучшем случае возникает трудность, и становится непрактичным. Поэтому рекомендуется следовать дисциплине блокировки в многопоточных программах. Например, проработка порядка блокировки при множественном захвате блокировок помогает избежать взаимоблокировок, а приобретение защитной блокировки до получения доступа к общему ресурсу помогает избежать состояния гонок.

К сожалению, простым на первый взгляд правилам блокировки удивительно сложно следовать на практике. Основное ограничение в современных языках программирования и компиляторах заключается в том, что они не поддерживают напрямую спецификацию и анализ требований параллелизма. Программисты должны полагаться на неофициальные комментарии к коду для выражения своих намерений о том, как они используют блокировки.

Заметки SAL параллелизма предназначены для помощи в определении побочных эффектов блокировки, ответственности за блокировку, владения данными, иерархии порядка блокировки и другого ожидаемого поведения блокировки. Выполняя неявные правила явно, заметки SAL параллелизма предоставляют последовательный способ для документирования того, как код использует правила блокировки. Заметки параллелизма также расширяют возможности средств анализа кода для поиска условий гонки, взаимоблокировки, несоответствующих операций синхронизации и других неявных ошибок параллелизма.

Общие рекомендации

С помощью заметок можно указать контракты, которые подразумеваются определениями функций между реализациями (вызывающими) и клиентами (вызывающими). Вы также можете выразить инварианты и другие свойства программы, которые могут улучшить анализ.

SAL поддерживает множество различных типов примитивов блокирования, таких как критические секции, мьютексы, спин-блокировки и другие объекты ресурсов. Многие заметки параллелизма принимают выражение блокировки в качестве параметра. По соглашению блокировка обозначается выражением пути базового объекта блокировки.

Некоторые правила учета владения потоком, которые следует помнить постоянно:

Спин-блокировки являются несчитающими блокировками, у которых есть определенный поток-владелец.
Мьютексы и критические секции являются считающими блокировками, у которых есть определенный поток-владелец.
Семафоры и события считаются блоки, которые не имеют четкого владения потоком.

Блокировка заметок

В следующей таблице перечислены заметки о блокировке.

Номер	Description
`_Acquires_exclusive_lock_(expr)`	Добавляет заметки к функции и указывает, что функция после вызова увеличивает на единицу число монопольных блокировок объекта блокировок с именем `expr`.
`_Acquires_lock_(expr)`	Аннотирует функцию и указывает, что функция после вызова увеличивает на единицу число блокировок объекта блокировок с именем `expr`.
`_Acquires_nonreentrant_lock_(expr)`	Блокировка с именем `expr` получена. Возникает ошибка, если блокировка уже захвачена.
`_Acquires_shared_lock_(expr)`	Аннотирует функцию и указывает, что функция после вызова увеличивает на единицу число общих блокировок объекта блокировок с именем `expr`.
`_Create_lock_level_(name)`	Оператор, который объявляет символ `name` символом уровня блокировки, благодаря чему он может быть использован в аннотациях `_Has_Lock_level_` и `_Lock_level_order_`.
`_Has_lock_kind_(kind)`	Заметит любой объект для уточнения сведений о типе объекта ресурса. Иногда общий тип используется для разных видов ресурсов, а перегруженный тип недостаточно для различения семантических требований между различными ресурсами. Ниже представлен список предварительно определенных параметров `kind`: `_Lock_kind_mutex_` Идентификатор типа блокировки для мьютексов. `_Lock_kind_event_` Идентификатор типа блокировки для событий. `_Lock_kind_semaphore_` Идентификатор типа блокировки для семафоров. `_Lock_kind_spin_lock_` Идентификатор типа блокировки для блокировок спина. `_Lock_kind_critical_section_` Идентификатор типа блокировки для критических разделов.
`_Has_lock_level_(name)`	Аннотирует объект блокировки и присваивает ему уровень блокировки `name`.
`_Lock_level_order_(name1, name2)`	Оператор, предоставляющий порядок блокировки между `name1` и `name2`. Блокировки, имеющие уровень `name1` , должны быть получены перед блокировками, имеющими уровень `name2`.
`_Post_same_lock_(expr1, expr2)`	Заметит функцию и указывает, что в состоянии после записи две блокировки `expr1` и `expr2`обрабатываются так, как если бы они были одинаковыми объектами блокировки.
`_Releases_exclusive_lock_(expr)`	Добавляет заметки к функции и указывает, что функция после вызова уменьшает на единицу число монопольных блокировок объекта блокировок с именем `expr`.
`_Releases_lock_(expr)`	Аннотирует функцию и указывает, что функция после вызова уменьшает на единицу число блокировок объекта блокировок с именем `expr`.
`_Releases_nonreentrant_lock_(expr)`	Блокировка с именем `expr` снята. Сообщается об ошибке, если блокировка в данный момент не проводится.
`_Releases_shared_lock_(expr)`	Аннотирует функцию и указывает, что функция после вызова уменьшает на единицу число общих блокировок объекта блокировок с именем `expr`.
`_Requires_lock_held_(expr)`	Аннотирует функцию и указывает, что перед вызовом функции количество блокировок объекта с именем `expr` не менее единицы.
`_Requires_lock_not_held_(expr)`	Добавляет заметки к функции и указывает, что перед вызовом функции количество блокировок объекта с именем `expr` равно нулю.
`_Requires_no_locks_held_`	Аннотирует функцию и указывает, что количество блокировок на всех объектах блокировки равно нулю.
`_Requires_shared_lock_held_(expr)`	Аннотирует функцию и указывает, что перед вызовом функции количество общих блокировок объекта с именем `expr` не менее единицы.
`_Requires_exclusive_lock_held_(expr)`	Добавляет заметки к функции и указывает, что перед вызовом функции количество монопольных блокировок объекта с именем `expr` не менее единицы.

Встроенные SAL для непредоставленных явно объектов блокировки

Некоторые объекты блокировки не предоставляются реализацией связанных функций блокировки. В следующей таблице перечислены встроенные переменные SAL, которые содержат заметки для функций, действующих на эти защищенные объекты блокировки.

Номер	Description
`_Global_cancel_spin_lock_`	Описывает отмену спин-блокировки.
`_Global_critical_region_`	Описывает критическую область.
`_Global_interlock_`	Описывает блокируемые операции.
`_Global_priority_region_`	Описывает область приоритета.

Заметки общего доступа к данным

В следующей таблице перечисляются аннотации для доступа к разделяемым данным.

Номер	Description
`_Guarded_by_(expr)`	Добавляет заметки к переменной и указывает на то, что при доступе к данной переменной количество блокировок объекта с именем `expr` не менее единицы.
`_Interlocked_`	Заметит переменную и эквивалентна `_Guarded_by_(_Global_interlock_)`.
`_Interlocked_operand_`	Параметр аннотированной функции является целевым операндом одной из различных функций interlocked. Эти операнды должны иметь определенные дополнительные свойства.
`_Write_guarded_by_(expr)`	Добавляет заметки к переменной и указывает на то, что при изменении данной переменной количество блокировок объекта с именем `expr` не менее единицы.

Заметки Smart Lock и RAII

Смарт-блокировки обычно упаковывают собственные блокировки и управляют их временем существования. В следующей таблице перечислены заметки, которые можно использовать с смарт-блокировками и шаблонами кодирования RAII с поддержкой move семантики.

Номер	Description
`_Analysis_assume_smart_lock_acquired_(lock)`	Сообщает анализатору предположить, что получена смарт-блокировка. Эта заметка ожидает тип ссылочной блокировки в качестве параметра.
`_Analysis_assume_smart_lock_released_(lock)`	Указывает анализатору предположить, что смарт-блокировка была выпущена. Эта заметка ожидает тип ссылочной блокировки в качестве параметра.
`_Moves_lock_(target, source)`	`move constructor` Описывает операцию, которая передает состояние блокировки из `source` объекта в `target`объект. Считается `target` вновь созданным объектом, поэтому любое состояние, которое оно было раньше потеряно и заменено состоянием `source` . Он `source` также сбрасывается в чистое состояние без количества блокировок или целевого объекта псевдонимов, но псевдонимы, указывающие на него, остаются неизменными.
`_Replaces_lock_(target, source)`	`move assignment operator` Описывает семантику, в которой выдается целевая блокировка перед передачей состояния из источника. Вы можете рассматривать его как комбинацию `_Moves_lock_(target, source)` , предшествуемую параметру `_Releases_lock_(target)`.
`_Swaps_locks_(left, right)`	Описывает стандартное `swap` поведение, которое предполагает, что объекты `left` и `right` обмен их состоянием. Обмен состоянием включает число блокировок и целевой объект псевдонима, если он присутствует. Псевдонимы, указывающие на `left` объекты, `right` остаются неизменными.
`_Detaches_lock_(detached, lock)`	Описывает сценарий, в котором тип оболочки блокировки позволяет диссоциироваться с его содержащимся ресурсом. Он похож на то, как `std::unique_ptr` работает с внутренним указателем: он позволяет программистам извлекать указатель и оставлять его интеллектуальный контейнер указателя в чистом состоянии. Аналогичная логика поддерживается `std::unique_lock` и может быть реализована в пользовательских оболочках блокировки. Отсоединяемая блокировка сохраняет свое состояние (число блокировок и целевой объект псевдонима, если таковые имеются), а оболочка сбрасывается, чтобы содержать нулевое число блокировок и не целевой объект псевдонимов, сохраняя собственные псевдонимы. Нет никаких операций по подсчетам блокировок (освобождение и получение). Эта заметка ведет себя точно так же, как `_Moves_lock_` и за исключением того, что отсоединяемый аргумент должен быть `return` , а не `this`.