OCaml 메모리 모델

ref를 읽을 때 어떻게 될까? 싱글 쓰레드 코드에서는 “뭐가 됐든 가장 최근에 쓴 값”을 읽는게 너무 당연하지만, 복잡한 동기화가 필요한 멀티 쓰레드 코드에서는 “가장 최근”에 대한 정확한 정의가 어려워진다.

여기서는 이런 미묘한 부분을 어떻게 피하는지, 그리고 “가장 최근”이 복잡한 개념이 아닌 상황에서 직관적인 동기화 코드를 어떻게 작성하는지를 설명한다. 후자는 세부적인 내용을 살펴봐야 하지만, 대부분은 저수준의 동기화 라이브러리를 작성하거나 컴파일러를 해킹해야 하는 사람에게 유용한 내용이다 (만약 어플리케이션 코드를 짜는데 이런 저수준의 세부 사항에 의존하고 있다면, 뭔가 잘못하고 있는 거다).

Happens-before

ref에서 값을 읽거나 값을 쓰는 것 같은 프로그램의 실행 흐름(trace), 또는 일련의 이벤트를 고려하면 실행 중인 OCaml 프로그램과 메모리 사이의 상호 작용을 이해할 수 있다 (여기서는 ref를 “수정 가능한 메모리 위치”와 같은 의미로 사용한다. 즉, 가변 레코드 필드와 가변 오브젝트 멤버는 전부 ref다). 각각의 이벤트는 소스 코드의 읽기와 쓰기 연산에 대응하지만, 소스 코드의 특정 연산은 실행할 때마다 매번 새로운 이벤트를 생성한다.

싱글 쓰레드 프로그램이 생성하는 이벤트의 순서를 프로그램 순서라고 한다. 멀티 쓰레드 프로그램에서는, 여전히 프로그램 순서를 얘기하긴 하지만, 더 이상 total order가 아니다. 이벤트는 서로 다른 두 쓰레드가 생성하는데, 이 이벤트끼리는 프로그램 순서 상 서로 이전/이후라고 말할 수 없다.

프로그램 순서는 소스 코드 안의 연산이 작성된 순서를 나타내지만, 반드시 그 이벤트가 발생하는 순서를 명시하지는 않는다. 이벤트는 그 순서가 바뀔 수 있고 (reorder), 컴파일러와 CPU에 의해서 합쳐지거나 최적화될 수 있다. 신뢰 가능한 순서는 happens-before라는 relation으로 명시될 수 있다. 만약 이벤트 e1이 이벤트 e2보다 먼저 생긴다면(happens-before), 어떤 쓰레드도 e1 없이 e2만 관측할 수 없다. 이것을 e1가 e2 이후에 발생(happens-after)한다고 한다. 만약 서로가 각각 먼저 생길 수 있다면 (happens-before the other), 이들 이벤트들은 동시에 발생(happen concurrently)한다고 한다. Happens-before 관계는 추이적(transitive; e1 -> e2 이고 e2 -> e3 라면 e1 -> e3)이고 비반사관계(어떤 이벤트도 스스로보다 먼저 발생하지 않는다. 즉 \forall e. ~(e -> e))이다.

동기화를 위한 API는 일반적으로 happens-before 관계를 명시한다. 예를 들면, 뮤텍스는 한 쓰레드의 Lock 연산이 Unlock 연산 이전에 발생(happens-before)하고, Unlock 연산이 그 다음 쓰레드의 Lock 연산 이전에 발생(happens-before)하도록 명시한다. 여기서 happens-before 관계는 refs와 아토믹 참조 Atomic.t로 명시된다.

여기서는 채널과 같은 고수준 동기화에 대해서는 얘기하지 않는다. 하지만, 아토믹과 관련하여 보장되는 내용은 고수준의 동기화를 구현하는데 충분하다.

읽기, 쓰기, 그리고 경쟁 상태

가장 기본적인 happens-before 보장(guarantee)은 특정 ref에 대한 싱글 쓰레드의 접근에 관한 내용이다.

e1과 e2가 프로그램 순서의 이벤트이고 (즉 같은 쓰레드에 의해서 순서대로 실행되고) 같은 ref에 접근하고 둘 다 읽기 연산이 아닐 때, 그러면 e1이 e2에 선행(happens-before)한다.

다음과 같은 프로그램을 생각해보자.

1. let r = ref 0 in
2. let a = !r in
3. r := 1;
4. let b = !r in
5. let c = !r in
...

1, 2, 3 라인은 순서대로 발생한다. 메모리 모델 측면에서 보자면 라인 1에서는 참조를 초기화하기 때문에 “쓰기” 연산으로 취급된다. 라인 3은 라인 4, 5에 선행하지만, 라인 4와 5는 둘 다 읽기 연산이므로 동시에 발생한다.

읽기 이벤트 r이 발생하면, 그 메모리 위치에 대한 어떤 쓰기 이벤트 w에 의해 쓰여진 값을 읽는다. 초기화도 역시 쓰기 연산이다. 이때 어떤 쓰기 이벤트의 값인지는 다음과 같은 규칙에 의해 정해진다.

만약 같은 ref에 대해서 어떤 쓰기 연산 w가 어떤 읽기 연산 r에 선행하고, 다른 모든 쓰기 연산 w'는 w에 선행하거나 r에 후행한다면, r은 w가 쓴 값을 읽는다.

이 규칙은 항상 적용되지는 않는다. w가 없을 수 있다: 예를 들면, r과 동시에 발생하는 쓰기 이벤트가 있을 수 있고, 또는 r에 선행하면서 동시에 발생하는 두 개의 쓰기 이벤트가 있을 수 있다. 이 규칙이 읽기 이벤트에 적용되지 않을 때, 우리는 이를 데이터 경쟁(data race)라고 한다.

프로그램은 아래에서 설명할 아토믹과 같은 동기화를 통해 데이터 경쟁을 피해야 한다. C++ 메모리 모델과는 달리, 이 메모리 모델은 데이터 경쟁이 있는 상태에서도 상대적으로 강한 보장을 준다. 하지만, 프로그램은 여전히 경쟁을 피하기 위해서 노력해야 한다: 이 모델이 보장하는 내용(아래의 “Coherence and data races” 참조)은, 데이터 경쟁이 프로그램을 작성하는 어떤 합리적인 방법이라는 것이 아니라, 데이터 경쟁에 의해 발생하는 피해를 제한하기 위해 존재한다. 예를 들면, OCaml 메모리 모델에서, 특정 ref에 대한 데이터 경쟁은 오직 그 ref에 대한 미래의 읽기 이벤트들이 이상한 결과를 읽도록 할 뿐, 전체 프로그램이 C++처럼 정의되지 않은 동작(Undefined Behaviour; UB)을 일으키도록 하는 것이 아니다.

이 규칙은 하나의 쓰레드에 의해 사용되는 메모리 참조에 대해서 예상 가능한 동작을 보장하는데 충분하다. 위의 예시 프로그램에서, 라인 2의 읽기는 라인 1의 초기화 (쓰기)에 의해 쓰여진 값을 읽을 것이다. 왜냐하면, 다른 쓰기 연산(라인 3)은 라인 2(읽기)에 후행하기 때문이다. 비슷하게, 라인 4와 5의 읽기는 라인 3에서 쓰여진 값을 읽을 것인데, 다른 쓰기 연산(라인 1)이 라인 3(쓰기)에 선행하기 때문이다.

Atomics

위의 규칙이 싱글 쓰레드가 접근하는 ref에 대해서 합리적인 동작을 보장하는 반면, 멀티 쓰레드 환경에서는 잘 동작하지 않는다. 예를 들어, 아래의 관용적인 메시지 전달 코드를 보자. message는 0으로 초기화 된 int ref이고 flag는 false로 초기화된 bool ref 이다.

thread 1:
1. message := 42
2. flag := true

thread 2:
3. let seen = !flag in
4. let value = !message in
5. if seen then print_int value

이 프로그램에는 데이터 경쟁이 있다. 라인 3에서 flag를 읽는 부분이 문제다. 왜냐하면 라인 2에서 값을 쓰는 부분과 동시에 발생하기 때문이다. 라인 4에서 message를 읽는 부분도 비슷하게 라인 1의 쓰기 부분과 경쟁 상태에 있다. 만약 라인 3의 읽기 연산이 라인 2의 쓰기 연산을 읽고, 라인 4의 읽기 연산이 message의 초기화 결과를 읽으면, 이 프로그램은 0을 출력할 수도 있다.

더 구체적으로, 이렇게 되는 이유는 다양하다. 예를 들어, 2번 쓰레드가 message에 먼저 접근한다고 하자.

thread 2:
let old = !message in
let seen = !flag in
let value = !message in
if seen then print_int value

컴파일러는 message를 읽는 두 번쨰 연산을 지우는 최적화를 수행할 수도 있다.

thread 2:
let old = !message in
let seen = !flag in
let value = old in
if seen then print_int value

이제 이 프로그램은 seen = true이지만 value = 0인 상태가 될 수 있다.

심지어 최적화 없이 실행되더라도, weakly ordered 머신인 ARM이나 PowerPC에서 실행된다면 이 프로그램은 0을 출력할 수 있다. 이 머신들은 flag와 message에서 읽고 쓰는 연산의 순서를 지들 마음대로 바꿀 수 있다.

메모리 모델의 관점에서, 이런 (0을 출력하는 것과 같은) 나쁜 동작이 허용되는 이유는 쓰레드 1과 쓰레드 2의 연산들 사이에 happens-before 관계가 없기 때문이다. 필요한 동기화를 제공하기 위해서 아토믹을 써야 한다. 프로그램을 다시 짜서 flag를 Atomic.t로 만들자.

thread 1:
1. message := 42
2. Atomic.set flag true

thread 2:
3. let seen = Atomic.get flag in
4. let value = !message in
5. if seen then print_int value

이 프로그램은 절대로 0을 출력할 수 없다: 아무것도 출력하지 않을 수는 있지만, 출력한다면 그 값은 항상 42이다. 이렇게 되는 이유는 아토믹과 관련한 두 가지 규칙 때문인데, 하나는 다음과 같이 싱글 쓰레드에서의 happens-before를 명시하는 내용이고:

아토믹에 선행하는 프로그램 순서의 모든 것은 아토믹에 선행하고, 아토믹에 후행하는 프로그램 순서의 모든 것은 아토믹에 후행한다.

다른 하나는 쓰레드 사이의 happens-before를 명시하는 내용이다:

같은 아토믹 참조에 대해서 둘 다 읽기가 아닌 모든 두 개의 이벤트에 대해서, 둘 중 하나는 다른 하나에 선행한다.

첫 번째 규칙에 의해서, 라인 1은 라인 2에 선행하고, 라인 3은 라인 4에 선행한다 (싱글 쓰레드). 두 번째 규칙에 의해서, 라인 2와 3 중 하나는 다른 하나에 선행 한다 (멀티 쓰레드). 만약 2가 3에 선행하면, 1은 4에 선행해야 하므로 프로그램은 42를 출력한다. 반대의 경우 (즉 3이 2에 선행하면), 3은 false를 읽게 되고 프로그램은 아무것도 출력하지 않는다.

특정 아토믹 참조에 대한 이벤트는 happens-before에 의해서 전순서를 갖기 때문에, 아토믹에 대한 데이터 경쟁은 발생할 수 없음을 알아두자.

다른 메모리 모델과의 비교

이 모델은 데이터 경쟁이 있을 때의 동작을 명시한다. 이는 C++와는 다르고 자바와는 같다.

이 모델의 아토믹 참조는 자바의 volatile 변수나 C++의 seq_cst 아토믹과 비슷하지만, OCaml 아토믹은 아토믹이 아닌 변수의 순서를 바꾸는 것과 관련해서 더 강한 성질을 갖고 있다. 예를 들어, 다음 프로그램을 보자.

thread 1:
Atomic.set x 1
let a = !y

thread 2:
y := 1
let b = Atomic.get x

OCaml 에서는, x에 접근하는 두 아토믹 중 하나는 다른 하나에 선행한다. 만약 set이 먼저 발생하면 b = 1이 된다. get이 먼저 발생하면 y에 값을 대입하는 연산이 get에 선행하고, 이는 set에 선행하고, 이는 y에서 값을 읽는 연산에 선행하기 때문에, a = 1이 된다. 하지만, 자바와 C++ 모두에서는 a = b = 0이 가능하다.

인과 (Causality)

인과 공리 (Causality axiom)는 다음과 같다:

acyclic(hb | po | rf)

위는 herd7라는 메모리 모델 시뮬레이터 도구의 문법이다. 이 공리는 모든 로드-버퍼링 동작을 금지하여 C++와 자바가 겪는 “갑자기 튀어나온 이상한 값” 문제를 제거한다. hb는 happens-before 관계이고, po는 프로그램 순서이고, rf는 reads-from 관계(r이 w가 쓴 값을 읽으면 w rf r)이다. |는 합(union) 연산이다. acyclic은 관계에 대해 체크하려는 성질 이름으로, 여기서는 싸이클이 없어야 한다는 뜻이다.

hb | po | rf에 싸이클이 없도록 요구하는 것은 C++에서 “갑자기 튀어나온 이상한 값(out-of-thin-air values)” 문제를 해결하기 위해서 제안되었지만, ARM과 PowerPC와 같은 weakly-ordered 머신에서 차후에 오는 쓰기(store) 연산이 이전의 읽기(load) 연산에 의존성을 갖게 되어서 수많은 의미없는 브랜치를 삽입해야 하기 때문에, 성능 문제로 거절되었다. 하지만 OCaml에서는 이런 성능과 관련한 트레이드 오프가 다음 두 가지 이유로 인해 받아들일 수 있는 수준이라고 보여진다.

• OCaml에서 대부분의 읽기(load) 연산은 값이 변하지 않는 위치(immutable locations)에 대한 것이므로, 추가적인 브랜치를 삽입할 필요가 없다.
• 멀티코어 OCaml의 가비지 콜렉터 디자인은 이미 읽기 연산에 대한 배리어에 대해서 브랜치를 갖고 있기 때문에, 필요한 브랜치는 대부분 이미 (이걸로 인해) 존재한다.

Coherence and data races

일관 공리(Coherence axiom)는 다음과 같다:

acyclic(co | rf | fr | (hb & loc))

co는 coherence order로, 주어진 모든 메모리 위치에 대한 쓰기 연산의 전순서이다. fr은 from-reads 관계이고 rf^(-1); co로 정의된다. loc는 같은 위치에 대한 이벤트이다.

이 공리의 뜻은 만약 아토믹이 아닌 위치에 대해서 데이터 경쟁이 있더라도, 경쟁 중인 쓰기 중 하나는 반드시 경쟁을 이기게 되고 해당 메모리 위치의 값은 궁극적으로는 안정화된다는 뜻이다.