스레드 사이의 실행 순서
같은 코드도 연산이 섞이는 순서에 따라 다른 결과가 나올 수 있다. Lincheck는 검사 로직을 실행하며 이런 순서 차이를 탐색한다. 단순히 여러 번 실행해 우연히 오류가 나타나기를 기다리는 방식과 구분된다. 실행이 끝났을 때 확인해야 할 결과를 단언으로 작성하는 일은 여전히 중요하다.
자료 구조의 계약
동시 자료 구조에서는 검사할 연산을 선언하면 여러 호출 시나리오를 생성해 결과가 요구한 정확성 조건을 따르는지 확인할 수 있다. 기본 조건은 선형화 가능성이다. 호출 결과만 맞는지와 동시 호출을 어떤 순차 실행으로 설명할 수 있는지는 다른 질문이므로 필요한 계약을 고른다.
탐색 범위와 API 변화
스트레스 검사와 경계 있는 모델 검사에는 각각 탐색 범위와 가정이 있다. 통과한 작은 시나리오를 임의 크기와 모든 환경의 보증으로 확대하지 않는다. 3 계열에서는 일반 동시 코드 검사에 초점을 넓히고 패키지 및 배포 그룹도 변경했다. 사용하는 문서와 의존 버전을 맞추고 실패 추적을 현재 구현에서 다시 확인한다.
관련 문서
Jcstress / GenMC / CDSChecker / Loom 동시성 테스트