명세의 기호 평가
실제 숫자 하나만 실행하는 대신 명령어의 동작을 기호적으로 평가한다. 이 과정에서 레지스터 읽기와 쓰기, 연산 조건 같은 정보를 얻을 수 있다. Sail 명세가 분석 대상 명령어의 의미를 제공한다.
메모리 모델과 결합
isla-axiomatic은 Sail ISA 모델과 cat 언어 부분집합으로 작성한 공리적 메모리 모델을 결합한다. 작은 동시성 실험인 리트머스 테스트에서 어떤 결과가 허용되는지 살펴볼 수 있다. 명령어 의미와 메모리 순서 규칙은 서로 다른 입력이다.
모델 스냅샷 관리
이미 생성된 ISA 중간 표현 스냅샷을 사용하거나 Sail 모델에서 직접 만들 수 있다. 분석을 재현하려면 모델 스냅샷, 초기 상태 설정, 메모리 모델과 테스트를 함께 맞춘다. 같은 도구라도 이 구성들이 달라지면 허용되는 행동이 달라질 수 있다.
관련 문서
Sail 명세 언어 / GenMC / Relacy / Z3