자연적 축약(Natural Reductions)의 건전성 확인 복잡도에 대하여 (확장판)

인터리빙(interleavings)의 대표적인 부분 집합인 축약(reductions)의 검증은 매개변수화된 병행 프로그램(parameterized concurrent programs)의 정당성 증명을 단순화합니다. 본 논문에서는 우리가 자연적 축약(natural reductions)이라고 부르는 표현력이 풍부한 구문적 축약 클래스를 소개합니다. 자연적 축약은 매개변수화된 프로그램의 스레드 템플릿(thread template)에 원자적 블록(atomic blocks)과 전역 랑데부 지점(global rendezvous points)을 도입함으로써 지정됩니다. 우리는 주어진 (준)가환 관계(semi-commutativity relation)에 대해 주어진 자연적 축약이 건전한지(sound) 결정하는 문제를 연구합니다. 스레드 간의 동기화(synchronization)가 없는 경우에는 건전하고 완전한 다항 시간(polynomial-time) 알고리즘을 제시합니다. 동기화가 고려되는 경우에는 문제에 대한 일반적인 하한(lower bound)을 제공하며(동기화 메커니즘에 대해 매개변수화됨), 잠금(locking)과 같은 단순한 메커니즘에 대해서도 이 문제가 이미 coNP-hard임을 보여줍니다.