다음을 통해 공유


잠금 동작에 주석 지정

다중 스레드 프로그램에서 동시성 버그를 방지하려면 항상 적절한 잠금 규칙을 따르고 SAL 주석을 사용합니다.

동시성 버그는 비결정적이므로 재현, 진단 및 디버그하기가 매우 어렵습니다. 스레드 인터리빙에 대한 추론은 가장 어렵고, 스레드가 여러 개 있는 코드 본문을 디자인할 때는 실용적이지 않습니다. 따라서 다중 스레드 프로그램에서는 잠금 규칙을 따르는 것이 좋습니다. 예를 들어 여러 잠금을 획득한 동안 잠금 순서를 따르면 교착 상태를 방지하는 데 도움이 되고, 공유 리소스에 엑세스하기 전에 적절한 보호 잠금을 획득하면 경합 상태를 방지하는 데 도움이 됩니다.

하지만 겉보기에 간단해 보이는 잠금 규칙이 실제로는 따르기가 매우 어려울 수 있습니다. 오늘날의 프로그래밍 언어 및 컴파일러의 근본적인 제한 사항은 동시성 요구 사항의 사양 및 분석을 직접 지원하지 않는다는 것입니다. 프로그래머는 잠금을 사용하는 방법에 대한 의도를 표현하기 위해 비공식적인 코드 주석에 의존해야 합니다.

동시성 SAL 주석은 잠금 부작용, 잠금 책임, 데이터 보호, 잠금 순서 계층 구조 및 예상되는 기타 잠금 동작을 지정할 수 있도록 설계되었습니다. 암시적 규칙을 명시적으로 지정함으로써 SAL 동시성 주석은 코드에서 잠금 규칙을 사용하는 방법을 문서화할 수 있는 일관된 방법을 제공합니다. 또한 동시성 주석은 경합 상태, 교착 상태, 일치하지 않는 동기화 작업 및 다른 미묘한 동시성 오류를 찾기 위한 코드 분석 도구의 기능을 향상시킵니다.

일반 지침

주석을 사용하여 구현(호출자)과 클라이언트(호출자) 간의 함수 정의에 의해 암시되는 계약을 명시할 수 있습니다. 또한 분석을 더욱 개선할 수 있는 프로그램의 고정 및 기타 속성을 표현할 수도 있습니다.

SAL은 임계 영역, 뮤텍스, 스핀 잠금 및 기타 리소스 개체와 같은 다양한 종류의 잠금 기본 형식을 지원합니다. 많은 동시성 주석이 잠금 식을 매개 변수로 사용합니다. 규칙에 따라 잠금은 내부 잠금 개체의 경로 식으로 표시됩니다.

다음과 같은 스레드 소유권 규칙에 유의해야 합니다.

  • 스핀 잠금은 분명한 스레드 소유권이 있는 계산되지 않는 잠금입니다.

  • 뮤텍스와 임계 영역은 분명한 스레드 소유권이 있는 계산되는 잠금입니다.

  • 세마포 및 이벤트는 명확한 스레드 소유권이 없는 잠금으로 계산됩니다.

주석 잠금

다음 표에서는 잠금 주석을 보여 줍니다.

주석 설명
_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_
뮤텍스에 대한 잠금 종류 ID

_Lock_kind_event_
이벤트에 대한 잠금 종류 ID

_Lock_kind_semaphore_
세마포에 대한 잠금 종류 ID

_Lock_kind_spin_lock_
스핀 잠금에 대한 잠금 종류 ID

_Lock_kind_critical_section_
임계 영역에 대한 잠금 종류 ID
_Has_lock_level_(name) 잠금 개체에 주석을 추가하고 name 잠금 수준을 부여합니다.
_Lock_level_order_(name1, name2) name1name2 간의 잠금 순서를 제공하는 문입니다. 수준이 있는 잠금은 수준이 name1 name2있는 잠금 전에 획득해야 합니다.
_Post_same_lock_(dst, src) 함수에 주석을 달고 사후 상태에서 두 잠금 dst src이 잠금 속성을 src dst적용하여 동일한 잠금 개체인 것처럼 처리됨을 나타냅니다.
_Releases_exclusive_lock_(expr) 함수에 주석을 달고 사후 상태에서 함수가 expr로 명명된 잠금 개체의 단독 잠금 수를 하나 감소시킴을 나타냅니다.
_Releases_lock_(expr) 함수에 주석을 추가하고 사후 상태에서 함수가 expr로 명명된 잠금 개체의 잠금 수를 하나 감소시킴을 나타냅니다.
_Releases_nonreentrant_lock_(expr) expr로 명명된 잠금이 해제됩니다. 잠금이 현재 유지되지 않은 경우 오류가 보고됩니다.
_Releases_shared_lock_(expr) 함수에 주석을 추가하고 사후 상태에서 함수가 expr로 명명된 잠금 개체의 공유 잠금 수를 하나 감소시킴을 나타냅니다.
_Requires_lock_held_(expr) 함수에 주석을 달고 사전 상태에서 expr로 명명된 개체의 잠금 수가 1개 이상임을 나타냅니다.
_Requires_lock_not_held_(expr) 함수에 주석을 달고 사전 상태에서 expr로 명명된 개체의 잠금 수가 0개임을 나타냅니다.
_Requires_no_locks_held_ 함수에 주석을 추가하고 검사기에 알려진 모든 잠금의 잠금 수가 0개임을 나타냅니다.
_Requires_shared_lock_held_(expr) 함수에 주석을 추가하고 사전 상태에서 expr로 명명된 개체의 공유 잠금 수가 1개 이상임을 나타냅니다.
_Requires_exclusive_lock_held_(expr) 함수에 주석을 추가하고 사전 상태에서 expr로 명명된 개체의 단독 잠금 수가 1개 이상임을 나타냅니다.

노출되지 않은 잠금 개체에 대한 SAL 내장 함수

특정 잠금 개체는 연결된 잠금 함수의 구현에 의해 노출되지 않습니다. 다음 표에서는 이러한 노출되지 않는 잠금 개체에서 작동하는 함수에 주석을 사용하도록 설정하는 SAL 내장 변수를 보여 줍니다.

주석 설명
_Global_cancel_spin_lock_ 취소 스핀 잠금을 설명합니다.
_Global_critical_region_ 임계 영역을 설명합니다.
_Global_interlock_ 연동 작업을 설명합니다.
_Global_priority_region_ 우선 순위 영역을 설명합니다.

공유 데이터 액세스 주석

다음 표에서는 공유 데이터 액세스에 대한 주석을 보여 줍니다.

주석 설명
_Guarded_by_(expr) 변수에 주석을 추가하고 변수가 엑세스될 때마다 expr로 명명된 잠금 개체의 잠금 수가 1개 이상임을 나타냅니다.
_Interlocked_ 변수에 주석을 추가하며 _Guarded_by_(_Global_interlock_)와 동일합니다.
_Interlocked_operand_ 주석이 추가된 함수 매개 변수는 다양한 연동 함수 중 하나의 대상 피연산자입니다. 이러한 피연산자는 다른 특정 속성이 있어야 합니다.
_Write_guarded_by_(expr) 변수에 주석을 추가하고 변수가 수정될 때마다 expr로 명명된 잠금 개체의 잠금 수가 1개 이상임을 나타냅니다.

스마트 잠금 및 RAII 주석

스마트 잠금은 일반적으로 네이티브 잠금을 래핑하고 수명을 관리합니다. 다음 표에서는 의미 체계를 지원하는 move 스마트 잠금 및 RAII(리소스 획득 초기화) 코딩 패턴과 함께 사용할 수 있는 주석을 나열합니다.

주석 설명
_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 원본에서 상태를 전송하기 전에 대상 잠금이 해제되는 의미 체계를 설명합니다. 앞에 _Releases_lock_(target)오는 조합으로 _Moves_lock_(target, source) 간주할 수 있습니다.
_Swaps_locks_(left, right) 개체 left 를 가정하고 right 상태를 교환하는 표준 swap 동작을 설명합니다. 교환된 상태에는 잠금 수 및 별칭 대상(있는 경우)이 포함됩니다. 개체와 right 개체를 가리키는 별칭은 left 변경되지 않은 상태로 유지됩니다.
_Detaches_lock_(detached, lock) 잠금 래퍼 형식이 포함된 리소스와의 분리를 허용하는 시나리오를 설명합니다. 내부 포인터의 작동 방식 std::unique_ptr 과 유사합니다. 프로그래머가 포인터를 추출하고 스마트 포인터 컨테이너를 깨끗한 상태로 둘 수 있습니다. 유사한 논리는 사용자 지정 잠금 래퍼에서 지원 std::unique_lock 되며 구현할 수 있습니다. 분리된 잠금은 해당 상태(잠금 개수 및 별칭 대상(있는 경우)를 유지하며, 래퍼는 자체 별칭을 유지하면서 잠금 횟수가 0이고 별칭 대상은 없도록 다시 설정됩니다. 잠금 수(해제 및 획득)에 대한 작업은 없습니다. 이 주석은 분리된 인수가 아니라thisreturn 점을 제외하고 정확하게 _Moves_lock_ 동작합니다.

참고 항목