완화된 메모리 모델에서의 비종료성 증명
순차 프로그램에서 비종료성은 재귀 집합(recurrence sets)으로 특징지어집니다. 본 연구는 이러한 재귀 집합 개념을 약한 메모리 모델에서 실행되는 동시성 프로그램으로 확장합니다. 고전적인 재귀 집합이 상태와 전이에 기반한 순차 프로그램의 운영 의미론에서 정의되는 것과 달리, 동시성 프로그램은 실행(executions)에 기반한 공리적 의미론을 가집니다. 이에 따라 새로운 재귀 집합은 확장(extensions)에 대해 실존적으로 닫힌 실행 집합으로 정의됩니다. 동시성 프로그램의 의미론은 메모리 모델뿐만 아니라 스케줄러나 메…