스레드와 메모리 관찰
서로 다른 스레드에서 수행한 연산은 메모리 모델에 따라 예상과 다른 값으로 관찰될 수 있다. Nidhugg는 이런 동작을 분석해 오류를 찾는다. 대상 프로그램은 Pthreads를 사용하고 각 스레드는 단독 실행에서 결정적으로 동작한다는 전제를 가진다. 외부 입력이나 숨은 비결정성이 이 가정과 맞는지 검토한다.
모델과 빌드의 연결
SC와 TSO 및 PSO, POWER와 ARM 모델을 지원하지만 사용하는 LLVM 버전에 따라 일부 기능이 제한된다. 공식 안내는 LLVM 15 이상에서 ARM과 POWER 모델을 지원하지 않는다고 설명한다. 빌드가 성공했다는 사실과 필요한 분석 모델이 사용 가능하다는 사실을 구분한다. 대상과 분석 환경의 의미를 맞추어야 한다.
검사 목표와 결과 보존
C와 C플러스플러스 같은 언어의 코드를 중간 표현으로 연결한다. 검사할 프로그램과 입력 및 실행 가정을 좁혀야 결과의 범위를 이해하기 쉽다. 보고된 오류를 조사할 때는 스레드 순서와 메모리 관찰 관계를 함께 살핀다. 소스와 컴파일러 및 선택한 메모리 모델을 보존하고 제한된 검사에서 찾지 못한 오류까지 불가능하다고 단정하지 않는다.