1. Introduction

현대 CPU와 컴파일러는 프로그램을 공격적으로 최적화한다. 이런 최적화는 순차적인 프로그램(sequential programs)을 빠르게 만들지만, 병렬 프로그램(parallel program)에서는 놀라운 행동을 관찰하게 만든다. 이런 최적화에서 득을 보기 위해서, C++나 자바같은 메인스트림 언어들은 프로그램이 관찰할 수도 있는 이러한 느슨한 행동(relaxted behaviour)을 명세하는 복잡한 메모리 모델을 채택하고 있다. 하지만, 이런 모델은 곧바로 프로그램을 작성하기 어렵다.

이런 모델이 프로그래머에게 제공하는 기본적인 추론 도구는 데이터 경쟁 없음 정리(data-race-freedom theorems; DRF)이다. 프로그래머는 비원자적 변수에 동시에 접근하는 (동시에 읽는 것은 제외됨) 데이터 경쟁(data races)을 피하기 위해서 쓰레드 사이의 동기화에 쓰이는 모든 변수를 원자적(atomic)이라고 표시해야 한다. 대신, DRF 정리는 어떤 느슨한 행동도 관찰할 수 없음을 보장해준다. 정리하면, DRF 프로그램은 순차적인 의미(sequential semantics)를 갖는다.

프로그램이 데이터 경쟁에서 자유롭지 못할 때, 그런 모델은 프로그램의 행동에 대해서 아주 적은 보장을 해주거나 아니면 아무것도 보장해주지 않는다. 이것은 언어의 구성 요소를 잘못 사용하면 보통 정의되지 않은 행동(undefined behaviour)을 초래하는 불안전한 언어(unsafe languages)를 설명하는데 잘 맞는다. 즉, 데이터 경쟁 역시 하나의 오사용으로 보면, 이것은 꽤 자연스럽다. 반면에, 안전한 언어는 버그가 있는 프로그램일지라도 잘 정의된 의미(well-defined semantics)를 제공하기 위해 최선을 다한다. 이런 의미는 합성적(compositional)일 것으로 기대되는데, 그래야 프로그램이 그 프로그램의 구성 요소 중 일부가 버그를 갖고 있어도 부분을 이해함으로써 전체를 이해할 수 있기 때문이다.

데이터 경쟁에 약한 의미(weak semantics)가 주어지는 것은 이런 합성적 성질을 위태롭게 만든다. 안전한 언어에서는, 만약 f()이 올바른 정답을 리턴하더라도 f() + g()가 틀린 답을 리턴한다면, g에 버그가 있다고 결론지을 수 있다. 데이터 경쟁에 대한 약한 의미는 이런 성질을 위태롭게 하는데, g가 올바르더라도 f 안의 데이터 경쟁에 의해서 틀린 답을 내놓을 수도 있기 때문이다.

이 연구에서는 메모리를 공유하는 병렬 프로그램(shared-memory parallel programs)에 대한 새로운 의미를 제안하여, 데이터 경쟁이 있음에도 강력한 의미를 보장하게 해준다.

• 먼저 지역적 DRF(local DRF) 성질을 도입하여, 데이터 경쟁이 존재하는 상황에서도 동시성 프로그램에 대한 합성적인 추론을 가능하게 해준다.
• 간단한 small-step operational semantics와 함께 메모리 모델을 제안하고, 이 모델이 지역적 DRF를 가지고 있음을 증명하고, 동등한 axiomatic model을 제안한다.
• 이 메모리 모델이 많은 일반적인 컴파일러 최적화를 지원하며, x86과 ARMv8 아키텍쳐 모두에서 안전한 compilation scheme을 제공한다는 것을 보이고, OCaml에서의 효율성의 증거를 보인다.

2. Reasoning beyond data-race freedom

먼저 전역적 DRF(global DRF) 성질인:

데이터 경쟁에서 자유로운 프로그램은 순차적인 의미를 갖는다.

에서, 더 강한 지역적 DRF 성질인:

프로그램의 데이터 경쟁이 없는 모든 부분은 순차적인 의미를 갖는다.

를 제안한다.

전역적 DRF와 지역적 DRF의 차이점을 설명하기 위해서, 순차적인 프로그램과 지역적 DRF가 없어서 예상치못한 결과를 뱉는 멀티 쓰레드 프로그램 몇 가지를 소개할 것이다.

2.1. Bounding data races in space

지역적 DRF로 가기 위한 첫 번째 단계는 데이터 경쟁이 영향을 미치는 공간을 제한해서(bounding data races in space), 하나의 변수에 대한 데이터 경쟁이 다른 변수에 접근하는데 영향을 미치지 않도록 보장하는 것이다.

C++ 메모리 모델은 데이터 경쟁에서 자유로운 프로그램에 대해서만 의미를 주기 때문에, 원칙적으로 C++ 메모리 모델은 이런 성질을 갖지 않는다. 하지만, 어떻게 타당한 구현에서 이런 성질을 갖는 것이 실패하는지는 분명하지 않기 때문에, 예시를 들고 왔다.

Example 1.

b = a + 10

• 가정: a나 b에 다른 쓰레드가 접근하지 않는다.
• 예상 결과: b = a + 10
• 가능한 결과: b != a + 10 (C++)

설명

다음과 같은 멀티 쓰레드 프로그램을 생각해보자. c는 비원자적인 전역 변수이다.

c = a + 10;                         ||
...  some computation ...           ||  c = 1;
b = a + 10;                         ||

여기서 … 부분의 계산이 순수, 즉 사이드 이펙트가 없다고 하자. 컴파일러는 a가 두 번 읽히는 사이에 a가 수정되지 않는다는 것을 알고, a + 10을 굳이 두 번 계산할 필요가 없다는 것을 알고 첫 번째 쓰레드를 다음과 같이 최적화할 수 있다:

t = a + 10 ;
c = t;
... some computation ...
b = t;

… 부분의 계산에서 레지스터가 부족하다면 a + 10의 결과를 저장해둔 임시 변수 t가 레지스터에서 방출될 수 있다. t의 결과는 c에 저장되기 때문에, 똑똑한 레지스터 할당자(register allocator)는 새로운 스택 슬롯을 할당하기 보다는 t를 c로 재활용할 수 있다¹:

t = a + 10;                         ||
c = t;                              ||
...  some computation ...           ||  c = 1;
b = c;                              ||

하지만, 이렇게 최적화된 프로그램에서는, c = a + 10과 c = 1 사이에 데이터 경쟁이 생기고 c가 이상한 값을 가질 수 있다. 프로그래머의 관점으로는, a에 동시 쓰기(concurrent write)가 없었는데도 불구하고 같은 a에서 두 번 읽었는데 서로 다른 값을 관찰하게 된다! 실제로, 두 쓰레드가 c에 동시에쓰는 것이 유일한 데이터 경쟁이고, 첫 번째 쓰레드(의 원본 코드)에서는 c를 읽지 않았다.

변수 하나에 대한 데이터 경쟁이 다른 변수를 읽는 결과에 영향을 미치는 일은 컴파일러 최적화가 경쟁이 있는 C++ 프로그램에 줄 수 있는 최악의 영향은 아니다. Boehm의 연구에서는 다른 예시도 있지만, 이 예시 하나면 데이터 경쟁이 영향을 미치는 공간을 제한하는 일이 중대한 성질임을 보이기에 충분하며, 타당한 C++ 구현은 이 성질이 없다는 것도 알았다.

2.2 Bounding data races in time

C++와는 반대로, 자바 메모리 모델은 데이터 경쟁이 있더라도 허용되는 행동을 제한한다. 특히, 변수를 읽어서 리턴하는 값은 반드시 같은 변수에 쓰여진 무언가여야 하는데, 덕분에 데이터 경쟁이 영향을 미치는 공간이 제한된다.

하지만, 자바의 데이터 경쟁이 영향을 미치는 시간은 제한되어 있지 않다(not bounded in time): 아래의 예시와 같이, 과거에 발생한 데이터 경쟁이 이후의 접근에 영향을 줘서 비순차적인 행동을 가지도록 할 수 있다. 어떤 두 개의 접근이 동시에 발생(happen concurrently)한다는 것은, 메모리 모델에 의해 정의되는 순서를 사용해서 정의되는 이전에 발생(happens-before)을 이용해서 두 쓰레드가 서로 이전에 발생하지 않았다고 정의한다. 그러니까 아무런 동기화 없이 서로 다른 쓰레드에서 발생하는 두 개의 접근이라는 뜻이다.

Example 2.

b = a; c = a;

• 가정: a, b, c에 대해서 동시에 발생하는 접근이 없다.
• 예상 결과: b = c
• 가능한 결과: b != c (C++, 자바)

설명

다음과 같은 프로그램을 생각해보자. flag는 초기값이 false인 원자적 불리언 변수(자바의 volatile)이다.

a = 1;                              || a = 2;
flag = true;                        || f = flag;
                                    || b = a;
                                    || c = a;

f가 true가 되었다고 해보자. 그러면 flag가 volatile이기 때문에 flag에 대한 읽고 쓰기는 서로 동기화되고, 따라서 a에 값을 쓰는 일(a = 1과 a = 2)은 서로 경쟁 상태에 있지만 a에서 값을 읽는 일 이전에 발생하게 된다.

이런 상황에서, 다음과 같은 가정이 성립한다: a에서 값을 읽는 일과 동시에 발생하는 a, b, c에 대한 접근이 없다. 하지만, 자바는 b = 1, c = 2인 결과를 허용하는데, 두 개의 읽기(b = a와 c = a)가 서로 다른 쓰기(a = 1과 a = 2)에서 읽는 것을 서용하기 때문이다. 구체적으로는, 컴파일러가 c = a는 최적화하지 않고 b = a를 b = 2로 최적화하면 발생할 수 있다. 이런 상황은 별칭(aliasing) 때문에 발생할 수 있는데, 만약 첫 번째 읽기 b = a만 a = 2로 쓰여진 곳과 같은 위치라는 것을 정적으로 알는 경우에 그렇다. 자바 8과 9 버전에서 이 행동을 초래하는 구체적인 예시는 부록의 기술 보고서에 있음.

따라서, 자바의 데이터 경쟁은 시간에 얽매이지(bounded in time) 않는데, 메모리 모델이 과거에 일어난 데이터 경쟁으로 인해서 일관되지 않은 값을 리턴하는 것을 읽는 것을 허용하기 때문이다. 놀랍게도, 이런 비순차적인 행동은 미래의 데이터 경쟁 때문에 나타나기도 하는데, 다음 예시를 보자.

Example 3.

class C { int x; } 라는 정의가 이전에 있다고 가정하자.

C c = new C(); c.x = 42; a = c.x;

• 가정: a에 다른 접근은 없다.
• 예상 결과: a = 42
• 가능한 결과: a != 42 (C++, 자바)

설명

여기서, c는 새로 할당되었고 아직 다른 쓰레드가 참조하지 않기 때문에, 과거에 c.x에 데이터 경쟁이 발생할 수 없다는 것을 알 수 있다. 따라서, 이 코드 조각은 프로그램의 나머지 부분에 존재하는 데이터 경쟁과 상관없이 항상 a에 42를 쓴다고 상상할 수 있다.

하지만 실제로 이 이후의 데이터 경쟁 때문에 a가 42가 아닌 다른 값을 갖는 것이 가능하다. 다음 코드를 보면:

C c = new C();                      ||
c.x = 42;                           ||
a = c.x;                            ||
g = c;                              || g.x = 7;

첫 번째 쓰레드가 c.x에서 값을 읽고 g에 값을 쓰는데, 이때 이 두 오브젝트의 위치가 다르기 때문에, 자바의 메모리 모델은 이 순서를 바꾸는 것을 허용한다. 그래서 g = c가 먼저 실행되고, 그 사이 두 번째 쓰레드가 g.x에 7을 쓰고, 다시 첫 번째 쓰레드가 a = c.x로 값을 읽게 되면, a는 42가 아니라 7이 된다.

따라서, 지역적 DRF를 제공한다는 것은 곧 읽기의 순서가 나중에 있을 쓰기와 뒤섞이면 안된다는 것을 뜻하고, 이는 컴파일러 최적화와 느슨한 동작을 허용하는 (weakly-ordered) 하드웨어에서의 컴파일에 제약을 주게 된다. 이 제약으로 인한 성능 비용이 어느 정도인지 나중에 살펴볼 것이다.

2.3 Global and Local DRF

지역적 DRF 성질이란, 데이터 경쟁의 영향이 공간적으로 또 시간적으로 제한되는 것을 말한다. 다른 변수의 데이터 경쟁, 과거의 데이터 경쟁, 또는 미래의 데이터 경쟁이 어떤 변수에 접근하는 일에 영향을 주지 않는 것이다. 특히, 다음과 같은 직관적인 성질이 성립한다:

만약 같은 쓰레드가 어떤 위치 a에서 값을 두 번 읽을 때, 동시에 a에 값을 다른 쓰레드가 없다면, 두 번 읽은 값은 같은 값이다.

섹션 3에서 operational semantics를 소개한 뒤, 섹션 4에서 메모리 모델에 대한 지역적 DRF 정리를 형식적으로(formally) 기술한다. 자세한 증명은 부록에 있다. 지역적 DRF 정리 덕분에 이전에 소개한 예시들이 예상되는 행동을 한다는 것을 증명할 수 있었다.

표준적인 전역적 DRF 정리를 이용하면 앞의 세 가지 예시들이 프로그램 실행 도중의 어떤 시간에 어떤 변수에도 데이터 경쟁이 없다는 아주 강력한 가정 하에서만 예상되는 행동을 한다는 것을 증명할 수 있다. 반면 지역적 DRF는 프로그램의 다른 부분에 데이터 경쟁이 있어도 괜찮다는 더 일반적인 가정 하에 같은 결과를 증명할 수 있게 해준다.

3. A Simple Operational Model