작은 검사로 실행 구성
검사 대상은 여러 번 실행되므로 전체 애플리케이션보다 필요한 상호작용을 좁힌 단위 검사 형태가 적합하다. 전용 헤더와 공유 라이브러리를 연결하고 일반 main 대신 정해진 진입점을 사용한다. 지원하는 원자 연산과 동기화 API를 통해 동작을 관찰하므로 임의의 스레드 코드를 그대로 넣는 방식과 다르다.
원자 연산과 실행 경로
부분 순서 축소 등을 이용해 같은 의미의 중복 실행을 줄인다. 추적에 나타난 실행 순서와 값이 관찰되는 메모리 관계는 반드시 같지 않다. 어떤 쓰기에서 값을 읽었는지와 메모리 순서 및 스레드 관계를 함께 살펴야 오류 원인을 이해할 수 있다. 검사에 필요한 단언도 명시한다.
진행 조건과 지원 한계
메모리의 진행성과 공정성 설정이 종료를 기다리는 코드의 분석에 영향을 줄 수 있다. 해당 가정을 실제 대상과 맞춰야 한다. 일부 C플러스플러스 동기화 기능을 제공하지만 스레드 생성은 C11 형태를 지원하는 등 제약이 있다. 지원 범위를 확인하고 탐색 옵션 및 입력을 기록한다. 제한한 작은 모델의 성공을 임의 규모의 모든 실행으로 확대하지 않는다.
관련 문서
GenMC / Loom 동시성 테스트 / Spin 모델 검사기 / Civl 검증기