완화된 메모리 모델에서의 비종료성 증명

순차 프로그램에서 비종료성은 재귀 집합(recurrence sets)으로 특징지어집니다. 본 연구는 이러한 재귀 집합 개념을 약한 메모리 모델에서 실행되는 동시성 프로그램으로 확장합니다. 고전적인 재귀 집합이 상태와 전이에 기반한 순차 프로그램의 운영 의미론에서 정의되는 것과 달리, 동시성 프로그램은 실행(executions)에 기반한 공리적 의미론을 가집니다. 이에 따라 새로운 재귀 집합은 확장(extensions)에 대해 실존적으로 닫힌 실행 집합으로 정의됩니다. 동시성 프로그램의 의미론은 메모리 모델뿐만 아니라 스케줄러나 메모리 서브시스템과 같은 환경의 공정성(fairness) 가정에도 영향을 받습니다. 본 연구에서는 이러한 공정성 가정을 고려하여 새로운 재귀 집합을 정형화합니다. 이 재귀 집합이 모든 실용적인 메모리 모델에서 공정한 비종료성을 증명하는 데 건전(sound)하며, 상당수 모델에서는 완전(complete)하다는 것을 보입니다. 이론을 실제에 적용하기 위해, 약한 메모리 모델에서 동시성 프로그램의 공정한 비종료성을 증명하는 새로운 자동화 기법을 개발했습니다. 이 기법의 핵심은 실행 기반 라쏘(lassos)를 통해 재귀 집합을 유한하게 표현하는 것입니다. 라쏘 탐색 알고리즘을 Dartagnan에 구현하여 CPU 및 GPU 메모리 모델에서 실행되는 여러 프로그램에 대해 평가했습니다. 본 연구는 동시성 프로그램의 비종료성 분석을 위한 강력한 이론적, 실용적 프레임워크를 제공합니다. 이는 복잡한 메모리 모델 환경에서 프로그램의 신뢰성을 높이는 데 기여할 수 있습니다.