약한 메모리 검증 및 강건성을 위한 MSO 프레임워크

메모리 모델 (Memory models)은 컴파일러 및 아키텍처 최적화로 인해 발생하는 약한 동작 (weak behaviors)을 고려하는 병렬 프로그램 실행의 형식적 명세입니다. 메모리 모델의 수와 복잡성이 증가함에 따라, 통일된 처리를 허용하는 적절한 메타 이론 (metatheory) 내에서 모델들을 공리화함으로써 전체 모델 클래스에 걸쳐 균일한 검증을 수행하려는 노력이 이어져 왔습니다. 본 연구에서는 다양한 인기 약한 메모리 모델의 트리의 너비 (treewidth) 및 MSO 표현 가능성 (MSO-expressibility)에 관한 결과를 증명함으로써, 약한 메모리를 위한 메타 이론으로서 단항 이차 논리 (Monadic Second-Order logic, MSO)를 형식적으로 연구합니다. 이러한 조합은 우리가 여러 검증 문제를 통일적으로 다룰 수 있게 해줍니다. 요약하자면, 우리의 결과는 다음과 같습니다. 첫째, 순차적 일관성 ($\mathsf{SC}$) 하에서의 실행은 유계된 트리의 너비 (bounded treewidth)를 갖는 반면, 총 저장 순서 ($\mathsf{TSO}$) 하에서의 실행은 그렇지 않음을 증명합니다. 둘째, Release/Acquire 및 전체 RC20을 포함한 광범위한 모델들은 MSO 공리화가 가능하지만, Strong Release/Acquire 및 $\mathsf{TSO}$와 같은 다른 모델들은 SETH 하에서 이차 시간이 필요한 직교 벡터 (Orthogonal Vectors) 문제를 선형 시간 내에 해결할 수 없는 한 MSO 공리화가 불가능함을 증명합니다. 마지막으로, 최근의 거친 강건성 기준 (coarse robustness criteria)에 관한 연구를 확장하여 reads-from 강건성 (reads-from robustness)이라는 개념을 도입합니다. 우리의 트리의 너비 경계(상한 및 하한 모두)가 MSO 공리화 가능한 모든 모델 $\mathsf{MM}$에 대해 광범위한 알고리즘적 함의를 가짐을 보여줍니다. 즉, 모든 프로그램 $\mathsf{P}$에 대해, $\mathsf{MM}$ 하에서 $\mathsf{P}$를 검증하거나 $\mathsf{P}$가 $\mathsf{MM}$에 대해 reads-from 강건하지 않다고 보고하는 알고리즘이 존재합니다. 전반적으로, 우리의 결과는 약한 메모리 검증 및 강건성을 위한 풍부하고 다재다능한 이론적 프레임워크를 구축합니다.