OxCaml에서의 데이터 레이스 프리덤 (Data race freedom)

2026년 5월 7일 얼마 전 저는 이 블로그가 실시간으로 편집 가능한 OCaml 노트북을 임베드할 수 있도록 x-ocaml을 연결했습니다. 해당 포스트는 순정(vanilla) OCaml 5 toplevel을 사용했습니다. 오늘날 여러분의 브라우저에서 실행되는 toplevel은 컴파일러의 Jane Street 포크인 OxCaml로 구축되었습니다. 이는 우리가 스레드(thread)를 생성하지 않고도 작은 병렬 프로그램이 데이터 레이스(data-race)로부터 자유롭다는 것을 대화형으로 증명할 수 있음을 의미합니다.

아래 예시들은 최근 진행한 OxCaml에 관한 CS6868 강의(유인물)를 거쳐, OxCaml 팀의 훌륭한 'Intro to Parallelism (Part 1)' 튜토리얼을 각색한 것입니다. 해당 튜토리얼은 정석적인 참조 자료이며 전체를 읽어볼 가치가 있습니다. 이 포스트는 컴파일 타임(compile time)에 데이터 레이스를 배제하는 두 가지 새로운 모드 축(mode axes)과, 오해하기 쉬운 이식성(portability)에 관한 한 가지 미묘한 차이에 초점을 맞추어 그 핵심을 더 짧은 형태로 담아내고자 합니다.

짧은 여담: OCaml에서의 데이터 레이스는 덜 무섭습니다

본론으로 들어가기 전에, 왜 우리가 OCaml에서 데이터 레이스를 아예 배제하려고 하는지에 대해 잠시 짚고 넘어갈 가치가 있습니다. C, C++, 또는 unsafe Rust에서 데이터 레이스는 재앙적입니다. 표준은 여러분의 프로그램이 애초에 정의된 의미를 갖지 않는다는 근거 하에, 컴파일러가 조용한 메모리 오염(memory corruption)을 포함하여 무엇이든 할 수 있도록 허용합니다. OCaml은 훨씬 더 온건합니다. OCaml의 메모리 모델(memory model)은 레이스가 있는 프로그램이라 할지라도 타입 안전성(type safety)과 메모리 안전성(memory safety)을 보존함을 보장합니다. 레이스가 발생하는 프로그램은 도메인(domains) 간에 약한 일관성(weakly-consistent)을 가진 값을 관찰할 수는 있지만, 크래시(crash)가 발생하거나, 초기화되지 않은 메모리를 읽거나, 타입 시스템의 불변성(invariants)을 위반하지는 않습니다.

따라서 OCaml에서의 레이스(race)는 런타임의 실수(footgun)가 아니라 논리적 버그(logic bug)입니다. 그렇다면 왜 굳이 정적(statically)으로 이를 잡아내려 할까요? 프로그램이 데이터 레이스 프리(data-race free) 상태가 되면 **순차적 일관성 (sequential consistency)**을 얻을 수 있기 때문입니다. 즉, 관찰된 모든 동작은 각 도메인(domain)의 고유한 연산들이 프로그램 순서(program order)대로 실행되면서, 서로 다른 도메인들의 연산들이 어떻게 교차(interleaving)되는지로 설명될 수 있습니다. 여전히 동시성 추론(concurrent reasoning)이 필요하긴 합니다. 가능한 교차 방식이 많기 때문입니다. 하지만 이는 동시성 코드(concurrent code)가 가질 수 있는 가장 단순한 모델이며, 등식 추론(equational reasoning), 귀납법(induction), 그리고 일반적인 프로그램 논리 도구들을 각각의 교차 방식에 그대로 적용할 수 있습니다. 레이스 프리덤(race freedom)을 포기하면 이를 잃게 됩니다. 관찰된 동작을 정당화하기 위해 스레드 내부 (intra-thread) 재정렬(reordering)까지 허용해야 하며, 이 경우 단일 도메인의 연산이 다른 도메인들에게 프로그램 순서와 다르게 실행되는 것처럼 보일 수 있습니다. 순차적 일관성이 진정한 보상이며, 레이스 프리덤은 그것을 얻기 위해 지불하는 대가입니다.

Hello, OxCaml

여러분의 브라우저가 정말로 OxCaml 토플(toplevel)을 실행하고 있는지 빠르게 확인해 봅시다. @ local 어노테이션(annotation)은 OxCaml 전용 구문입니다. 순정(stock) OCaml 파서(parser)에서는 파싱조차 되지 않을 것입니다.

레이스가 발생하는 gensym

우리가 계속해서 다시 보게 될 예시입니다. 캡처된 카운터(counter)를 증가시켜 고유한 ID를 배정하는 심볼 생성기(symbol generator)입니다. 순차적으로 실행하면 잘 작동하며, 셀(cell)은 두 개의 ID를 출력합니다. 마지막 줄은 gensym을 다른 도메인으로 보내려고 시도하며, 바로 이 지점에서 타입 체커(type checker)가 우리를 막아섭니다.

이를 두 개의 도메인에서 병렬로 실행한다면, 데이터 레이스의 네 가지 구성 요소 레시피를 모두 충족하게 됩니다. 두 개의 도메인, 공유된 count, 양쪽 모두의 쓰기 작업, 그리고 count가 원자적(atomic)이지 않은 일반 ref라는 점입니다. 순정 OCaml 5에서는 컴파일러가 이 클로저(closure)를 다른 도메인으로 보내는 것을 기꺼이 허용할 것입니다. 하지만 OxCaml은 실행이 시작되기도 전에 이를 거부합니다. 에러 메시지는 바닐라(vanilla) OCaml의 어휘에는 없는 두 가지 개념인 비이식적 (nonportable) 과 이식적 (portable) 을 언급합니다. 이것들은 무엇을 의미할까요?

데이터 레이스 프리덤을 위한 두 가지 새로운 모드

OxCaml은 값의 타입과는 직교(orthogonal)하며, 해당 값이 어떻게 사용될 수 있는지를 설명하는 어노테이션(annotations)인 여러 모드를 통해 OCaml의 타입 시스템을 확장합니다. 저는 이미 이 블로그에 그중 두 가지에 대해 글을 쓴 적이 있습니다. 값이 최대 하나의 참조만을 갖는지 추적하는 uniqueness(유일성), 그리고 값이 얼마나 자주 사용될 수 있는지를 추적하는 linearity(선형성)가 그것입니다. 오늘 포스트는 다른 한 쌍, 즉 컴파일 타임에 데이터 레이스 (data races)를 배제하는 두 가지 모드에 대해 다룹니다.

contention (경합)—uncontended / contended: 여러 도메인 (domains)이 동시에 값에 접근할 수 있는지 여부를 추적합니다. contended 값은 지금 이 순간 다른 도메인의 손에 있을 수 있으므로, 타입 시스템은 해당 값으로 할 수 있는 작업을 제한합니다.

portability (이식성)—portable / nonportable: 값이 도메인 경계를 안전하게 넘어갈 수 있는지 여부를 추적합니다. 다른 도메인으로 전송되는 클로저 (closures)는 반드시 portable 해야 합니다.

이 한 쌍만으로도 gensym 레이스를 잡아내기에 충분합니다. 각 제한 사항을 개별적으로 살펴본 후, 다시 클로저로 돌아와 보겠습니다.

Contention은 가변 쓰기 (mutable writes)를 거부합니다

contended 값은 지금 이 순간 다른 도메인에 의해 변이 (mutated)될 수 있습니다. 따라서 OxCaml은 해당 값의 가변 필드 (mutable fields)를 읽거나 쓰는 것을 거부합니다:

마지막 줄의 에러 메시지는 정확히 해당 규칙을 명시합니다: “이 값은 contended 상태이지만, 가변 필드 mood가 쓰여지고 있으므로 uncontended 상태일 것으로 예상됩니다.” contended 값의 가변 필드를 읽는 것조차 거부됩니다. 다른 도메인이 동일한 순간에 쓰기 작업을 수행 중일 수 있기 때문입니다.

Portability는 캡처된 참조 (captured refs)를 거부합니다

Portability는 클로저에 관한 것입니다. @ portable 클로저는 컴파일러가 다른 도메인으로 보내기에 안전하다고 검증한 클로저이지만, 한 가지 결정적인 제약이 있습니다. 클로저가 인클로징 스코프 (enclosing scope)로부터 *캡처 (captures)*하는 모든 값은 클로저 본문 내부에서 contended로 취급됩니다. 아무것도 변이하지 않는 순수 함수 (pure function)는 contention 규칙이 반대할 요소가 없으므로 당연히 portable 합니다:

ref를 캡처하는 것 자체는 괜찮습니다. 규칙을 위반하는 것은 캡처된 ref를 *변이 (mutating)*하는 것입니다:

에러 메시지를 주의 깊게 읽어보세요. counter가 왜 이식 가능 (portable) 하지 않은지 정확한 이유를 알려줍니다. 클로저 (closure) 가 @ portable 이므로, 캡처된 r 은 본문 내부에서 contended 로 취급됩니다. 하지만 incr r 은 변이 (mutation) 이며, ref를 통해 쓰는 작업은 그것이 uncontended 여야 합니다. 이 두 규칙이 충돌하는 것입니다. 이제 원래의 gensym 거절 사유가 이해될 것입니다. 그것도 정확히 똑같은 일을 수행합니다 — 캡처된 count 를 변이합니다.

함정, 그리고 실제 규칙

마지막 두 셀을 함께 읽다 보면 잘못된 교훈을 얻기 쉽습니다. 즉, 함수를 다른 도메인으로 보낼 수 있게 안전하게 만들려면 부수 효과 (side effects) 를 포기해야 한다는 생각입니다. 그것은 너무나 제한적일 것입니다.

실제 규칙은 더 좁으며, 그 차이는 매우 중요합니다.

이식성 (Portability) 은 클로저가 자신을 둘러싼 스코프 (enclosing scope) 에서 무엇을 캡처하는지를 제한합니다. 캡처된 값들은 contended 가 됩니다 — 이것이 규칙이며, gensym 이 거절된 이유입니다. 하지만 클로저의 매개변수 (parameters) 는 캡처가 아닙니다. 그것들은 매 호출마다 새롭게 전달되므로, 타입이 명시하는 어떤 모드로도 전달될 수 있습니다 — @ uncontended 를 포함하여 말이죠. uncontended 인 인자를 제공해야 할 의무는 호출을 수행하는 쪽으로 넘어갑니다. 이는 "부수 효과 없음" 보다 훨씬 약한 요구 사항입니다.

코드에서의 캡처 vs 매개변수

이 차이를 구체화하는 예시입니다. loop 는 @ portable 이며, 그 본문은 int ref 를 변이합니다. 이것이 작동하는 이유는 해당 ref 가 캡처된 것이 아니라, @ uncontended 로 주석이 달린 매개변수 (parameter) 이기 때문입니다:

두 개의 @ portable 주석이 여기서 역할을 하고 있습니다. 내부의 주석은 loop 가 다른 도메인으로 보낼 수 있음을 나타냅니다 — 이것이 핵심이며, a 가 loop 의 캡처가 아닌 매개변수 이기 때문에 작동합니다. 즉, loop 가 결국 병렬적인 어딘가에서 호출될 때, 그 어딘가에서 전달하는 a 가 uncontended 임을 증명해야 합니다. 이식성이 변이를 금지한 것이 아니라, 증명의 책임을 호출 지점 (call site) 으로 넘긴 것입니다. 외부 주석은 factorial_portable 전체도 이식 가능하다는 것을 나타냅니다 — 그것은 새로운 a 를 할당합니다.

매 호출마다 새로운 a를 할당하며 외부의 어떤 것도 캡처하지 않으므로, 함수 전체를 다른 도메인 (domain)으로 보낼 수 있습니다. 컴파일러는 프로그램을 수락하는 과정의 일부로 두 주석 (annotations)을 모두 검증합니다.

공식적인 부연 설명: 기본값과 서브모딩 (submoding)

우리는 마치 @ contended와 @ portable이 흥미로운 모드 (modes)이며, 그것들이 없는 상태는 특별한 것이 아닌 것처럼 작성해 왔습니다. 사실 각 축에는 기본값과 보증이 "얼마나 강력한지"에 대한 방향을 가진 작은 격자 (lattice)가 존재합니다. 유인물에서는 이를 다음과 같이 요약합니다:

축 (Axis)	모드 (Modes, ⊑)	기본값 (Default)
경합 (Contention)	uncontended ⊑ shared ⊑ contended	uncontended
이식성 (Portability)	portable ⊑ nonportable	nonportable

A ⊑ B 관계는 **서브모딩 순서 (submoding order)**입니다. 모드 A의 값은 모드 B가 기대되는 곳 어디에서나 사용될 수 있는데, 이는 A가 더 강력한 보증을 담고 있고 B는 더 느슨한 기대치를 가지기 때문입니다. uncontended 값은 @ contended 파라미터 (parameter)를 만족합니다 (우리는 단지 호출된 함수가 다른 도메인이 해당 값에 접근하도록 허용할 수도 있다고 약속했을 뿐이며, 만약 다른 도메인이 결코 접근하지 않는다면 그 약속은 자명하게 호환됩니다). portable 클로저 (closure)는 @ nonportable 슬롯 (slot)을 만족합니다. 하지만 그 반대는 성립하지 않습니다. 서브모딩은 한 방향으로만 흐릅니다.

기본값은 일반적인 OCaml을 작성할 때 얻게 되는 값입니다. 모든 값은 uncontended 상태로 시작합니다. 즉, 다른 도메인이 이를 가지고 있지 않으므로 읽기와 쓰기가 제한되지 않습니다. 모든 클로저는 nonportable 상태로 시작합니다. 즉, 이를 다른 곳으로 보낼 것이라는 어떠한 주장도 하지 않습니다. 이것이 일반적인 OCaml 코드가 OxCaml 하에서도 타입 검사 (type-checking)를 유지하는 이유입니다. 기본값은 각 축의 가장 허용적인 끝단이며, 여러분(또는 병렬 API)이 더 강력한 보증을 요구할 때에만 새로운 제한 사항을 마주하게 됩니다. 이 포스트에서는 경합 체인의 두 끝단인 uncontended와 contended만을 사용하며, 도메인 간의 읽기 전용 접근을 허용하지만 gensym 이야기에는 필요하지 않은 shared는 건너뜁니다.

gensym으로 돌아가기: 해결책

캡처된 값과 파라미터의 구분은 단순한 루프를 해결하기에는 충분하지만, gensym

양상은 다릅니다. 호출 전반에 걸쳐 공유되어야 하는 단일 카운터가 존재하기 때문입니다. 우리는 그 자체가 이식 가능한 (portable) 카운터 타입을 필요로 합니다. 즉, 값이 경합 (contention)과 이식성 (portability) 모드 사이를 교차하더라도, 이를 캡처하는 클로저 (closure)가 이식성을 유지할 수 있는 무언가가 필요합니다. 그것이 바로 OxCaml의 portable 라이브러리에 있는 Portable.Atomic.t입니다. 'a Portable.Atomic.t는 그것이 어디에 위치하든 항상 이식 가능하며 항상 경합이 없는 (uncontended) 상태입니다.

카운터와 gensym을 하나의 모듈로 감싸서 최상위 레벨 (toplevel)이 전체 번들을 이식 가능한 것으로 볼 수 있게 한 다음, 처음에 우리를 곤경에 빠뜨렸던 일을 실제로 수행합니다. 즉, gensym을 새로 생성된 도메인 (domain)으로 전송하는 것입니다. 컴파일러는 이를 수용하며 (Gen이 이식 가능함을 검증합니다), 프로그램은 실행됩니다:

최상위 레벨은 module Gen : sig ... end @@ portable이라고 보고합니다. 모드 추론 (mode inference)이 내부의 모든 값이 이식 가능함을 감지하고 모듈 전체를 이식 가능하게 만들었으므로, Gen.gensym은 이식 가능 모드 (portable mode)에서의 추출 (extraction) 과정에서도 살아남습니다.

왜 위에서 사용했던 factorial_portable과 같은 방식으로 최상위 레벨에서 단순히 let (gensym @ portable) = ... 라고 작성하지 않는지 의문이 들 수도 있습니다. 그것은 최상위 레벨의 특이한 점 때문입니다. 일반적인 let은 암시적인 최상위 모듈 (implicit toplevel module)에 위치하게 되는데, 이 모듈 자체는 기본값인 nonportable 모드에 있습니다. 따라서 나중에 Domain.Safe.spawn이 gensym을 다시 읽어올 때, 클로저가 바인딩 시점에 이식 가능한 것으로 검증되었음에도 불구하고, gensym이 비이식적 (nonportable) 바인딩인 것을 보고 거부하게 됩니다. factorial_portable 셀이 더 단순한 형태를 사용할 수 있었던 이유는 다른 어떤 것도 이식 가능 모드에서 해당 바인딩을 추출하려고 시도하지 않았기 때문입니다. module Gen으로 감싸는 것은 클로저에 자체적인 이식 가능한 홈을 제공하며, 이것이 클로저가 실제로 도메인 경계를 넘을 수 있게 해줍니다. 실제 .ml 파일에서는 컴파일 단위 (compilation unit) 전체가 하나의 모듈이므로 모드 추론이 전체를 이식 가능하다고 표시할 수 있으며, 따라서 이러한 번거로운 과정은 필요하지 않습니다.

(여기서 보이는 Portable.Atomic에 대한 참고 사항: 실제 프로그램에서는 portable opam 라이브러리로부터 open Portable을 통해 가져오게 됩니다. 페이지 용량을 적절하게 유지하기 위해, 이 노트북은 basement만을 제공합니다.)

— 실제 원자적 연산 (atomic operations)을 제공하는 작은 라이브러리 — 이며, 페이지 상단의 숨겨진 설정 셀이 이를 : value mod contended portable이라는 Kind 어노테이션 (kind annotation)으로 감쌉니다. 이 Kind는 이 타입이 두 축을 모두 가로지른다는 것을 컴파일러에게 알려줍니다. 즉, 하나를 캡처하는 클로저 (closure)는 포터블 (portable) 상태를 유지하며, 어떤 도메인 (domain)이라도 이에 접근할 수 있다는 의미입니다. 강의 유인물에서는 단일 원자적 카운터 (atomic counter)보다 더 정교한 상태를 다루기 위한 정답은 **캡슐 (capsules)**이라고 언급합니다. 이는 가변 상태 (mutable state)를 해당 접근 프로토콜과 함께 묶는 구조적인 방법으로, 패키지 전체를 포터블하게 만듭니다.

남은 과제

여기서의 레이스 프리덤 (race-freedom) 보장은 어떠한 테스트 실행과도 무관합니다. 위의 모든 거부 사례는 디스크 상의 OxCaml 바이너리가 거치는 것과 동일한 컴파일 단계에서, 즉 코드가 실행되기도 전에 발생했습니다. 마지막의 spawn은 시연일 뿐 증명이 아닙니다. 컴파일러가 애초에 프로그램을 수락했다는 사실 자체가 레이스가 불가능함을 우리에게 알려줍니다. 두 개의 모드 축 (mode axes), 하나의 Kind 어노테이션, 그리고 "포터블 (portable)"이 무엇을 의미하는지에 대한 명확한 규칙만으로 데이터 레이스 프리덤 (data-race freedom)을 타입 체커 (type checker)가 강제하는 속성으로 만들기에 충분했습니다.

이 내용의 바탕이 된 강의에서는 캡슐 (capsules) (원자적 연산보다 더 정교한 공유 상태를 위한 것)과 Parallel.fork_join2 (구조적 병렬성 (structured parallelism)을 위한 것)에 대해 더 자세히 다룹니다. 이는 다음 포스트의 주제로 남겨두겠습니다.