메모리 모델

여러 실행 흐름이 같은 메모리를 함께 쓸 때 무엇이 보이고 무엇이 안 보일 수 있는지를 정해 둔 규약입니다. 프로그램에 적은 순서가 실제로 일어나는 순서와 같다는 보장은 없습니다. 어디까지 어긋나도 되는지의 선을 이 규약이 긋습니다.

상세

여러 사람이 주방 칠판 하나에 주문을 적고 지웁니다. 손이 바빠 적히는 차례가 뒤바뀌어도 칠판은 누가 봐도 같은 것이 보입니다. 메모리는 같은 자리를 같은 순간에 읽어도 흐름마다 다른 값이 읽힐 수 있습니다.

메모리 모델은 여러 실행 흐름이 같은 메모리를 읽고 쓸 때 어떤 읽기가 어떤 쓰기의 값을 볼 수 있는지를 정하는 규약입니다. 프로그램에 적힌 순서를 지키겠다는 약속이 아닙니다. 어긋남의 상한을 긋는 약속입니다. 컴파일러와 프로세서가 어디까지 재배치해도 되는지, 그 상한이 여기서 정해집니다.

Leslie Lamport 는 1979년 논문에서 이 자리를 이렇게 잡았습니다. 프로세서는 프로그램이 지정한 순서와 다른 순서로 연산을 실행할 수 있습니다. 실행 결과가 프로그램에 적힌 순서대로 실행한 것과 같기만 하면 그 실행은 옳다고 봅니다. 이 조건을 만족하는 프로세서를 그는 순차적이라 불렀습니다. 문제는 그런 프로세서 여럿이 공통 메모리에 접근할 때 생깁니다. 각자 자기 프로그램 기준으로만 옳으면 서로가 보는 순서까지 맞는다는 보장이 없습니다.

flowchart TD
    A["프로그램에 적힌 순서"] -->|"재배치가 일어나는 자리"| B["컴파일러와 프로세서가 낸 순서"]
    B -->|"보이는 시점이 갈리는 자리"| C["다른 흐름이 읽는 순서"]

어긋남은 두 자리에서 생깁니다. 하나는 프로그램에 적힌 순서와 실제로 실행되는 순서 사이입니다. 여기서는 컴파일러가 한 번 순서를 옮겨 적습니다. 프로세서가 그 순서를 다시 바꿉니다. 다른 하나는 실행된 순서와 다른 흐름에 보이는 순서 사이입니다. 메모리 모델은 이 두 자리에서 무엇까지 허용되는지를 답합니다. 답이 적혀 있지 않으면 같은 코드가 기계마다 다르게 돕니다.

배경

실행 흐름이 하나뿐이면 순서를 곧이곧대로 지킬 이유가 적습니다. 결과만 같으면 되기 때문입니다. 그래서 컴파일러는 명령의 순서를 바꿔 내보냅니다. 프로세서도 기다리는 시간을 줄이려고 앞뒤 연산의 순서를 바꿔 실행합니다. 흐름이 하나일 때 이 재배치는 밖으로 드러나지 않습니다. 드러날 상대가 없습니다.

흐름이 둘이 되면 사정이 달라집니다. 한 흐름의 중간 상태를 다른 흐름이 읽습니다. 그 순간 재배치가 밖에서 관측됩니다. 어떤 뒤바뀜까지 관측될 수 있는지 아무 데도 적혀 있지 않으면, 프로그램이 맞는지 틀렸는지를 따질 기준 자체가 없습니다. 손에 있는 기계에서 통과했다는 사실은 다음 기계에서도 통과한다는 뜻이 아닙니다.

선을 그어야 할 계층도 하나가 아닙니다. 재배치는 컴파일러가 한 번, 프로세서가 또 한 번 합니다. 하드웨어가 무엇까지 뒤바꾸는지를 알아도, 컴파일러가 소스의 어느 줄을 어디로 옮겨도 되는지는 그것으로 정해지지 않습니다. 그 계층의 답은 언어가 적어야 합니다.

그래서 하드웨어를 만드는 쪽과 언어를 정하는 쪽이 각자 그 선을 문서로 못 박게 됐습니다. 무엇이 보장되고 무엇이 보장되지 않는지를 적은 그 규약을 메모리 모델이라 부릅니다. 프로그램의 정확성은 이 선 위에서만 따질 수 있습니다.

갈래

무엇을 재배치할 수 있게 남겨 두느냐가 축입니다. 한쪽 끝은 어떤 뒤바뀜도 밖에서 관측되지 않게 하는 것입니다. 반대쪽 끝은 인과만 지키면 나머지 순서를 열어 두는 것입니다.

순차 일관성

Lamport 는 공통 메모리에 접근하는 프로세서 여럿으로 이루어진 컴퓨터에 조건 하나를 걸었습니다. 어떤 실행의 결과든 모든 프로세서의 연산을 어떤 하나의 순차 순서로 실행한 것과 같아야 합니다. 그리고 각 프로세서의 연산이 그 순서 안에서 자기 프로그램이 지정한 순서대로 나타나야 합니다. 이 조건을 만족하는 다중프로세서를 그는 순차적으로 일관되다고 불렀습니다.

요구는 둘입니다. 전체 연산을 한 줄로 세울 수 있어야 합니다. 그 줄 안에서 각 프로세서의 연산은 자기 프로그램 순서를 지켜야 합니다. 프로그램을 읽으며 머릿속에 그리는 그림이 대체로 이것입니다.

강한 순서

Intel 소프트웨어 개발자 매뉴얼의 Memory Ordering 절은 메모리 순서를 프로세서가 읽기와 쓰기를 시스템 버스를 거쳐 시스템 메모리로 내보내는 순서라고 적습니다. 같은 문서는 이 아키텍처가 구현에 따라 여러 메모리 순서 모델을 지원한다고 적습니다. Intel386 프로세서는 어떤 상황에서도 명령어 흐름에 나온 순서대로 읽기와 쓰기를 내보냅니다. 같은 문서는 이것을 흔히 강한 순서라 부른다고 적습니다.

전체 저장 순서

P6 이후 계열은 그 선을 조금 늦춥니다. 읽기는 다른 읽기와 재배치되지 않습니다. 쓰기는 앞선 읽기를 앞지르지 못합니다. 쓰기끼리도 재배치되지 않습니다. 다만 비시간적 이동 명령으로 낸 스트리밍 저장과 문자열 연산은 이 금지의 예외입니다. 읽기는 서로 다른 위치를 향한 앞선 쓰기를 앞지를 수 있습니다. 같은 위치를 향한 쓰기는 앞지르지 못합니다. 쓰기끼리의 순서는 그대로 두고 읽기만 앞선 쓰기를 앞지르는 이 꼴을 전체 저장 순서라 부릅니다. 프로세서가 여럿이면 조건이 더 붙습니다. 한 프로세서가 낸 쓰기들은 모든 프로세서에게 같은 순서로 관측됩니다. 서로 다른 프로세서가 낸 쓰기들 사이에는 순서가 정해지지 않습니다.

완화 원자성

언어 계층은 연산마다 필요한 만큼만 순서를 요구하게 열어 둡니다. C++ 표준 초안은 원자 연산에 memory_order 를 붙이고 relaxed · acquire · release · acq_rel · seq_cst 같은 값을 둡니다. relaxed 에서는 어떤 연산도 메모리를 순서 짓지 않습니다. release 를 붙인 저장 연산은 그 메모리 위치에 대해 해제 연산을 수행합니다. acquire 를 붙인 적재 연산은 획득 연산을 수행합니다.

seq_cst 는 거기에 하나를 더 얹습니다. 모든 스레드가 모든 변경을 같은 순서로 관측하는 단일 전체 순서가 존재합니다. 위의 순차 일관성이 언어 계층에 다시 나타난 자리입니다.

예시

이 규약이 실제로 나타나는 자리는 Java 언어 명세, 커널 문서, C++ 표준 초안입니다. 셋을 나란히 두면 같은 문제를 서로 다른 계층에서 어떻게 적어 두는지가 보입니다.

Java 언어 명세

Java 언어 명세(Java Language Specification)의 17.4.5 절은 happens-before 순서를 정의합니다. 한 동작이 다른 동작보다 happens-before 이면 앞의 것은 뒤의 것에 보이고 뒤의 것보다 앞에 순서 지어집니다. 두 동작 x 와 y 에 대해 이 관계를 hb(x, y) 라고 적습니다.

규칙은 이런 꼴입니다. x 와 y 가 같은 스레드의 동작이고 프로그램 순서상 x 가 y 앞에 오면 hb(x, y) 입니다. x 가 뒤따르는 y 와 synchronizes-with 관계이면 역시 hb(x, y) 입니다. hb(x, y) 이고 hb(y, z) 이면 hb(x, z) 입니다. 객체 생성자의 끝에서 그 객체의 종료자 시작으로 가는 happens-before 간선도 있습니다.

Linux 커널 memory-barriers.txt

커널 문서는 CPU(Central Processing Unit, 중앙처리장치)가 프로그램의 인과가 유지되는 것처럼 보이기만 하면 메모리 연산을 자기가 원하는 어떤 순서로도 수행할 수 있다고 적습니다. 서로 독립인 메모리 연산은 사실상 무작위 순서로 수행됩니다.

그래서 순서가 필요한 자리에는 배리어를 넣습니다. 필수 배리어는 mb() · rmb() · wmb() 입니다. SMP(Symmetric Multi-Processing, 대칭 다중 처리) 조건부 배리어는 smp_mb() · smp_rmb() · smp_wmb() 입니다. 주소 의존 배리어는 READ_ONCE() 안에 들어 있습니다. 같은 문서는 아키텍처가 어떤 배리어에 대해 최소 요구보다 더 줄 수는 있어도 그보다 덜 주면 그 아키텍처가 틀린 것이라고 적습니다. 반대로 아키텍처가 도는 방식 때문에 명시적 배리어가 필요 없어져 배리어가 무연산이 되는 경우도 있을 수 있습니다. DEC Alpha 에서는 READ_ONCE() 가 메모리 배리어 명령까지 냅니다.

C++ 표준 초안

C++ 표준 초안은 이 규약 위에서 데이터 경쟁을 정의합니다. 두 표현식 평가가 이럴 때 충돌합니다. 한쪽이 메모리 위치를 수정하거나 객체의 수명을 시작하거나 끝냅니다. 다른 쪽이 같은 메모리 위치나 겹치는 저장 공간을 읽거나 수정합니다.

데이터 경쟁의 조건은 셋입니다. 잠재적으로 동시인 두 충돌 동작이 있습니다. 그중 적어도 하나가 원자적이지 않습니다. 어느 쪽도 다른 쪽보다 happens before 하지 않습니다. 셋이 다 맞으면 그 실행에는 데이터 경쟁이 있습니다. 그런 데이터 경쟁의 결과는 정의되지 않은 동작입니다.

모델이 무엇을 규정하는 물건인지가 여기서 드러납니다. 어떤 값이 나오는지를 정하는 것이 아닙니다. 어떤 프로그램이 애초에 뜻을 가지는지를 정합니다.

메모리 모델

상세

배경

갈래

순차 일관성

강한 순서

전체 저장 순서

완화 원자성

예시

Java 언어 명세

Linux 커널 memory-barriers.txt

C++ 표준 초안

관련 항목

순서를 강제하는 도구

재배치를 일으키고 다스리는 하드웨어 요소

규약이 깨졌을 때 나타나는 문제

이것을 정의하는 표준·문서

이 규약이 조율하는 실행 단위와 자원