접근 조건을 선언하기
어떤 변수가 어떤 잠금으로 보호되는지, 함수를 호출하려면 어떤 잠금이 필요한지 표시할 수 있다. 분석기는 코드의 잠금 상태와 선언한 조건을 비교한다. 같은 타입의 잠금이라도 서로 다른 객체에 속한다면 별개의 조건으로 취급될 수 있다.
함수 경계의 계약
호출하는 쪽이 지켜야 할 잠금 조건은 명시적으로 선언해야 한다. 함수 사이의 모든 실행 경로를 자동으로 추론하는 분석은 아니다. 잠금과 해제의 불균형이나 보호 조건을 만족하지 않는 접근을 검토하는 데 활용한다.
실행 검사와의 차이
정적 검사이므로 런타임 계측 비용을 추가하지 않는다. 대신 주석과 분석 모델이 실제 규칙을 정확히 반영해야 한다. 경고가 없다고 모든 경쟁 상태와 교착 상태가 사라졌다는 뜻은 아니며 동적 검사와 실제 동시 실행 테스트도 함께 고려한다.