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

요약

본 논문은 매개변수화된 병행 프로그램의 정당성 증명을 단순화하기 위해 '자연적 축약(natural reductions)'이라는 새로운 구문적 축약 클래스를 제안합니다. 연구팀은 주어진 (준)가환 관계에 대해 이러한 축약이 건전한지 결정하는 복잡도를 분석하였으며, 동기화 유무에 따른 알고리즘의 효율성과 복잡도 하한을 제시합니다.

핵심 포인트

• 원자적 블록과 전역 랑데부 지점을 포함하는 '자연적 축약' 개념 도입
• 스레드 간 동기화가 없는 경우 건전하고 완전한 다항 시간 알고리즘 존재 확인
• 동기화 메커니즘이 포함될 경우 문제의 복잡도가 급격히 증가함을 증명
• 잠금(locking) 메커니즘을 포함한 일반적인 경우의 문제가 coNP-hard임을 입증