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

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

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

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

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

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

Используя аннотации, вы можете формулировать договоры, которые неявно выражены определениями функций, между реализациями (вызываемыми объектами) и клиентами (вызывающими объектами), а также задавать инварианты и другие свойства программы, которые впоследствии могут повысить эффективность анализа.

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

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

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

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

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

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

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

Annotation Описание
_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, которые содержат заметки для функций, действующих на эти защищенные объекты блокировки.

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

Общие заметки о доступе к данным

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

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

Заметки Smart Lock и RAII

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

Annotation Описание
_Analysis_assume_smart_lock_acquired_ Сообщает анализатору о том, что была получена смарт-блокировка. Эта заметка принимает в качестве параметра Тип блокировки ссылки.
_Analysis_assume_smart_lock_released_ Сообщает анализатору о том, что была снята смарт-блокировка. Эта заметка принимает в качестве параметра Тип блокировки ссылки.
_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 .

См. также: