스케줄 외의 메모리 의미
동시 코드는 스레드 순서뿐 아니라 원자 연산과 메모리 모델에 따라 관찰 가능한 값이 달라질 수 있다. GenMC는 SC와 TSO 및 RA, RC11, IMM 등 여러 모델을 다룬다. 어떤 모델이 실제 대상과 맞는지 정해야 분석 결과를 적용할 수 있다. 단순히 실행을 반복하는 부하 검사와는 역할이 다르다.
중간 표현과 입력 언어
C 계열은 Clang을, Rust는 rustc를 통해 LLVM 중간 표현으로 연결한다. 분석의 핵심은 공통 표현을 사용하지만 언어별 프런트엔드와 지원 API의 제약은 남는다. Rust 지원은 실험적 구성으로 안내되며 컴파일러가 사용하는 LLVM 주요 버전과 GenMC의 빌드를 맞춰야 한다.
탐색 범위와 재현
동적 부분 순서 축소로 불필요한 중복 실행 탐색을 줄인다. 선택한 검사 목표와 입력 범위가 실제로 확인하는 영역을 결정하므로 전체 서비스를 그대로 완전 검증했다고 해석하지 않는다. 지원되는 동기화 기능과 외부 호출을 확인하고 오류 실행의 메모리 연산을 조사한다. 소스와 컴파일러 및 메모리 모델 설정을 함께 보존한다.