프로그래밍 언어 및 도구 연구소

Coq Proof Assistant에서 비인터리빙 동시성 모델의 기계화

Coq Proof Assistant에서 동시 계산의 다양한 비인터리빙 모델에 대한 기계화 이론.

동시 프로그램에 대한 추론에 직접 접근하는 방식은 개별 스레드의 원자적 동작에 대한 가능한 모든 인터리빙 세트로 동작을 정의하는 것입니다.그러나 인터리빙에 대한 추론은 가능한 인터리빙의 수가 빠르게 증가하기 때문에 인간과 컴퓨터 모두에게 너무 어려운 것으로 입증되었습니다.

pomset 언어 및 이벤트 구조와 같은 비인터리빙 동시성 모델은 프로그램 동작 세트에 대해 보다 간결한 표현을 제안함으로써 이 문제를 해결하려고 합니다.최근 몇 년 사이에 이완된 메모리 모델, 동시 프로그램의 모델 검사 및 모델 기반 돌연변이 테스트와 같은 비인터리빙 동시성 모델에 대한 관심이 다시 높아졌습니다.

이 프로젝트의 목표는 Coq Proof Assistant에서 비인터리빙 동시성 모델의 기계화된 이론을 개발하는 것입니다.라이브러리는 관심 있는 연구자들이 이러한 모델의 속성을 공식적으로 증명하고 이론의 새로운 응용을 개발하는 데 도움을 줄 것입니다.

참가자

Evgenii Moiseenko