동시성 구조를 검증하기
스레드가 공유 자료에 접근하거나 GPU 작업이 배리어에서 만나는 동작은 실행 순서에 영향을 받는다. VerCors는 이러한 구조를 명세와 연결해 분석한다. OpenCL 커널의 배리어와 원자 연산, OpenMP 지시문 등 서로 다른 병렬 프로그래밍 형태가 관심 대상이다.
권한과 결과를 함께 표현
어떤 메모리를 읽거나 쓸 수 있는지와 연산이 만족해야 하는 조건을 주석으로 나타낸다. 데이터 경쟁이 없다는 성질과 원하는 계산을 수행한다는 성질은 구분된다. 필요한 계약을 작성하고 각 성질이 실제로 검증됐는지 확인한다.
언어와 환경의 경계
여러 언어를 지원하도록 설계되었지만 각 언어의 모든 기능이 동일하게 처리되는 것은 아니다. 새 검증 기능을 시험하는 PVL이라는 언어도 제공한다. 실행 환경에는 자바가 필요하며 C를 다룰 때는 Clang도 요구된다.
관련 문서
Viper 검증 기반 / Gobra / Relacy / GenMC