유한한 선점(Bounded Preemptions) 하에서의 순차적 일관성(Sequential Consistency) 검증

Gibbons와 Korach는 1997년에 근본적인 문제를 연구했습니다: 멀티스레드(multi-threaded) 프로그램의 관찰된 읽기(reads) 및 쓰기(writes) 시퀀스가 주어졌을 때, 순차적 일관성(sequentially consistent)을 갖는 인터리빙(interleaving)이 존재하는가? 공유 메모리(shared memory) 구현 테스트에 대한 응용 외에도, 이 문제에 대한 절차는 동적 부분 순서 감소(Dynamic Partial-Order-Reduction, DPOR) 알고리즘에서 사용됩니다. 이 문제는 서로 다른 구문론적 파라미터(syntactic parameters)가 제한되더라도 NP-hard인 것으로 알려져 있습니다. 본 논문에서 우리는 요구되는 인터리빙의 종류에 대한 제한 사항을 고려합니다: 최대 π번의 선점(preemptions)을 갖는 순차적 일관성 인터리빙이 존재하는가? 경험적 증거에 따르면 여러 버그가 몇 번의 선점적 전환(preemptive switches) 내에서 나타납니다. 이는 우리가 유한한 선점(bounded preemptions) 하에서 이 문제를 조사하도록 동기를 부여합니다. 우리의 결과는 삼분법(trichotomy)을 보여줍니다: 각 변수에 대해 해당 변수에 쓰는 스레드가 단 하나인 단일 작성자(single-writer) 프로그램 클래스의 경우 이 문제는 다항 시간(polynomial-time) 알고리즘을 가질 수 있습니다; 두 명의 작성자(two-writer) 프로그램의 경우 NP-hard가 되며, 마지막으로 세 명의 작성자(three-writer) 프로그램의 경우 지수 시간 가설(Exponential-Time-Hypothesis, ETH) 하에서 조건부 하한(conditional lower bound)을 얻습니다. 선점(preemptions)의 횟수 π가 제한되지 않을 때, 우리는 이 문제가 W[1]-hard임을 보여주며, 따라서 파라미터 π에 대해 고정 파라미터 계산 가능(fixed-parameter-tractable, FPT)할 가능성이 낮음을 보여줍니다.