Chapter 11

RVWMO 메모리 모델

하트 0이 x = 1을 쓰고 이어서 y = 1을 썼다. 하트 1이 y에서 1을 읽었다면 x도 당연히 1일까? RISC-V에서는 아니다. 서로 다른 주소에 대한 메모리 접근은 다른 하트가 보기에 순서가 바뀔 수 있다. 어떤 순서 바뀜이 허용되고 어떤 것은 금지되는지를 정한 규칙이 메모리 일관성 모델이고, RISC-V의 모델 이름이 RVWMO(RISC-V Weak Memory Ordering)다. 이 장에서는 저장 버퍼에서 시작해 RVWMO의 정의, FENCE, 리트머스 테스트, 그리고 C/C++ 원자 연산이 어떻게 번역되는지까지 따라간다.

저장 버퍼·캐시·비순차 실행 때문에 다른 하트가 순서 바뀐 결과를 볼 수 있음을 설명한다.
순차 일관성(SC), TSO, RVWMO가 허용하는 재배치를 비교한다.
프로그램 순서, 전역 메모리 순서, 보존 프로그램 순서(PPO)를 구별한다.
PPO 13개 규칙을 네 무리(주소 겹침·명시적 동기화·구문 의존성·파이프라인 의존성)로 정리한다.
Load Value·Atomicity·Progress 세 공리를 안다.
FENCE의 fm·pred·succ 필드를 인코딩하고 fence.tso의 뜻을 안다.
MP·SB·LB·2+2W 리트머스 테스트의 결과를 모델별로 예측하고 C/C++ 매핑을 읽는다.

RVWMO v2.0 Explanatory Material Ztso v1.0 FENCE (RV32I)

왜 메모리 모델이 필요한가

하트 하나만 보면 모든 것이 프로그램 순서대로 일어나는 것처럼 보인다. 그런데 하드웨어 내부는 그렇지 않다. 성능을 위해 거의 모든 코어가 다음과 같은 장치를 쓴다.

저장 버퍼(store buffer) — store는 캐시에 바로 쓰지 않고 버퍼에 넣어 둔 뒤 나중에 내보낸다. 그동안 뒤의 load는 기다리지 않고 먼저 메모리로 간다.
비순차 실행 — 주소가 먼저 계산된 load부터 실행한다. 캐시 미스가 난 load 뒤의 load가 먼저 값을 받아 올 수 있다.
캐시와 연결망 — 여러 코어의 쓰기가 서로 다른 경로로 퍼져 나가 도착 순서가 달라질 수 있다.

내 하트 안에서는 이런 재배치가 감춰진다(내가 쓴 값은 내가 곧바로 다시 읽을 수 있다). 하지만 다른 하트는 그 효과를 다른 순서로 볼 수 있다.

그림 11-1. 저장 버퍼가 만드는 재배치. 금색 점(store)은 버퍼에 들어가 한참 기다리고, 파란 점(load)은 그 사이 곧장 메모리에 가서 값을 읽어 온다. 하트 0 자신은 이 차이를 느끼지 못하지만, 메모리를 함께 보는 다른 하트에게는 순서가 바뀐 것으로 보인다.

이 효과가 실제로 어떤 결과를 낳는지 아래 애니메이션에서 단계별로 확인해 보자. 두 하트가 각자 자기 변수에 1을 쓰고 상대 변수를 읽는다. 사람이 생각하는 “한 번에 하나씩” 실행이라면 둘 다 0을 읽는 일은 불가능하다. 적어도 한쪽의 쓰기가 먼저 끝났을 테니까.

ANIMATION

저장 버퍼가 만드는 r1 = r2 = 0

각 하트의 store와 load 사이

진행

단계0 / 6

r1 (하트 0)?

r2 (하트 1)?

메모리 x, y0, 0

“아무것도 없음”에서 끝까지 진행하면 r1 = r2 = 0이 나온다. 두 load가 모두 상대의 store가 버퍼에 갇혀 있는 동안 메모리를 읽었기 때문이다. “fence rw,rw”로 바꾸면 FENCE가 앞선 store를 먼저 내보내야 통과할 수 있어서 결과가 1, 1로 바뀐다.

SC, TSO, 그리고 RVWMO

메모리 모델은 “다른 하트가 볼 수 있는 결과의 집합”을 정한다. 강한 모델일수록 프로그래머가 생각하기 쉽고, 약한 모델일수록 하드웨어가 빨라질 여지가 크다.

그림 11-2. 세 모델의 직관적 모형. SC는 스위치 하나가 하트들을 번갈아 메모리에 연결한다. TSO는 하트마다 FIFO 저장 버퍼가 있다. RVWMO는 하트마다 자기 접근의 순서를 (규칙이 허락하는 한) 섞을 수 있지만, 모든 하트가 하나의 전역 메모리 순서에 동의한다는 점(multi-copy atomicity)은 지킨다.

서로 다른 주소에 대한 재배치	SC	TSO / Ztso	RVWMO
store → 뒤의 load	금지	허용 (저장 버퍼)	허용
store → 뒤의 store	금지	금지	허용
load → 뒤의 load	금지	금지	허용
load → 뒤의 store	금지	금지	허용 (의존성 없을 때)
자기 store 값을 먼저 읽기 (전달)	—	허용	허용

규격 원문에서

“Under RVWMO, code running on a single hart appears to execute in order from the perspective of other memory instructions in the same hart, but memory instructions from another hart may observe the memory instructions from the first hart being executed in a different order.”

RVWMO Memory Consistency Model, Version 2.0 — 그래서 여러 하트가 함께 쓰는 코드는 FENCE나 원자 명령으로 순서를 명시해야 한다.

RVWMO의 뼈대: 프로그램 순서, 전역 메모리 순서, PPO

RVWMO는 세 가지 순서로 정의된다.

프로그램 순서(program order) — 한 하트의 동적 명령 흐름에서 메모리 연산이 놓인 순서. 단순한 순차 프로세서가 실행할 순서다.
전역 메모리 순서(global memory order) — 모든 하트의 메모리 연산을 한 줄로 세운 전체 순서. 실행마다 하나씩 있다.
보존 프로그램 순서(preserved program order, PPO) — 프로그램 순서 가운데 전역 메모리 순서가 반드시 지켜야 하는 부분 집합.

그림 11-3. 전역 메모리 순서 만들기. 하트 0의 (a)·(b)는 서로 다른 주소에 쓰는 store이고, 하트 1의 (c)·(d)도 서로 다른 주소를 읽는다. 어느 쌍도 PPO로 묶여 있지 않으므로 RVWMO는 (b)→(c)→(d)→(a) 같은 전역 순서를 허용한다. 그 결과 하트 1은 y의 새 값과 x의 옛 값을 함께 본다.

RVWMO의 정의는 한 문장으로 요약된다. “PPO를 지키고 세 공리(Load Value, Atomicity, Progress)를 만족하는 전역 메모리 순서가 하나라도 존재하는 실행은 합법이다.” 그러니 PPO에 무엇이 들어 있는지가 곧 “무엇이 재배치되지 않는가”의 목록이다.

보존 프로그램 순서(PPO) 13가지 규칙

메모리 연산 a가 프로그램 순서상 b보다 앞에 있고, 둘 다 일반 메인 메모리(I/O 영역이 아님)에 접근하며, 아래 중 하나라도 성립하면 a는 전역 메모리 순서에서도 반드시 b보다 앞에 온다. AMO는 load이자 store라는 점에 주의하자.

무리	규칙	조건 (a가 프로그램 순서상 b보다 앞)
주소 겹침	1	b가 store이고, a와 b가 겹치는 주소에 접근한다
	2	a·b가 모두 load이고, 둘 다 읽는 바이트 x가 있으며, 둘 사이에 x로의 store가 없고, a·b가 x에 대해 서로 다른 메모리 연산이 쓴 값을 돌려준다
	3	a가 AMO 또는 SC로 생긴 연산이고, b가 load이며, b가 a가 쓴 값을 돌려준다
명시적 동기화	4	a를 b 앞에 두는 FENCE가 있다
	5	a에 acquire 표시가 있다
	6	b에 release 표시가 있다
	7	a와 b 모두 RCsc 표시가 있다
	8	a가 b와 짝(paired)이다 (LR과 짝인 SC)
구문 의존성	9	b가 a에 주소 의존성을 가진다
	10	b가 a에 데이터 의존성을 가진다
	11	b가 store이고, a에 제어 의존성을 가진다
파이프라인 의존성	12	b가 load이고, 둘 사이의 어떤 store m이 a에 주소·데이터 의존성을 가지며, b가 m이 쓴 값을 돌려준다
파이프라인 의존성	13	b가 store이고, 둘 사이의 어떤 명령 m이 a에 주소 의존성을 가진다

규칙 5–7의 표시(annotation)는 원자 명령의 aq/rl 비트(10장)나 Zalasr 명령이 붙인다. aq나 rl이 붙은 AMO·LR·SC는 RCsc 표시를 갖는다. 규칙 12·13은 실제 파이프라인이 투기적으로 값을 전달하거나 주소를 모르는 store를 지나쳐 갈 수 없다는 현실을 모델에 반영한 것이다.

그림 11-4. 세 가지 구문 의존성. 의존성은 값이 아니라 레지스터 이름을 따라 정의된다(syntactic). 그래서 xor t0, a0, a0처럼 결과가 늘 0인 계산을 거쳐도 의존성은 남는다. 제어 의존성은 store에만 순서를 준다. 분기 예측으로 뒤의 load를 미리 실행하는 것은 막지 않는다.

세 공리: Load Value, Atomicity, Progress

PPO를 지키는 전역 메모리 순서가 있다고 해서 아무 값이나 읽을 수 있는 것은 아니다. load가 무엇을 돌려주는지, LR/SC가 언제 원자적인지, 연산이 영원히 미뤄질 수 있는지를 세 공리가 정한다.

공리	내용 (요약)
Load Value	load의 각 바이트는, 그 바이트를 쓰는 store 가운데 ① 전역 메모리 순서상 load보다 앞선 것과 ② 프로그램 순서상 load보다 앞선 것을 모두 모아, 그중 전역 메모리 순서가 가장 늦은 store의 값을 돌려준다.
Atomicity	짝을 이룬 LR(r)과 SC(w)에서, r이 store s의 값을 읽었다면 s는 w보다 앞서고, s와 w 사이에 다른 하트가 그 바이트에 쓴 store가 끼어들 수 없다.
Progress	어떤 메모리 연산도 무한히 많은 다른 연산 뒤로 밀릴 수 없다. (쓴 값은 결국 다른 하트에게 보인다)

그림 11-5. Load Value 공리의 “프로그램 순서상 앞선 store” 조항. (b)는 전역 순서에서 (a)보다 앞에 놓였지만 (a)의 값 1을 읽을 수 있다. 저장 버퍼에서 값을 가져오는 저장 버퍼 전달(store forwarding)을 허용하기 위한 조항이다. Ztso 규격도 “TSO에서 저장 버퍼 전달을 허용하는 것도 Load Value 공리”라고 설명한다.

RVWMO는 multi-copy atomic이다

전역 메모리 순서가 하나라는 것은, 어떤 store가 한 다른 하트에게 보였다면 모든 다른 하트에게도 같은 순서로 보인다는 뜻이다(자기 하트의 저장 버퍼 전달만 예외). Power나 옛 Arm처럼 하트마다 다른 순서로 store를 볼 수 있는 non-multi-copy-atomic 모델보다 추론하기 쉽다. 규격 부록에는 이 모델을 Alloy·Herd 형식으로 쓴 공리적 정의와, 동등한 동작(operational) 모델이 함께 실려 있다.

FENCE: 순서를 명시하는 명령

PPO 규칙 4가 말하는 FENCE는 기본 정수 ISA(5장)의 일부다. FENCE 앞의 선행 집합(predecessor set)에 속한 연산을, 뒤의 후행 집합(successor set)에 속한 연산보다 먼저 일어난 것으로 모든 하트와 외부 장치가 보게 만든다. 집합은 네 종류를 조합한다: 장치 입력(I), 장치 출력(O), 메모리 읽기(R), 메모리 쓰기(W).

그림 11-6. FENCE 인코딩. 비트 27–24가 선행 집합(I·O·R·W), 23–20이 후행 집합이다. rs1·rd는 앞으로 더 세밀한 FENCE를 위해 남겨 두었다. 예약된 설정은 기본 구현이 fm = 0000인 일반 FENCE로 취급한다.

FENCE	막는 재배치	대표 용도
`fence rw,rw`	앞의 모든 읽기·쓰기 → 뒤의 모든 읽기·쓰기	전체 장벽, C++ `seq_cst` 펜스, Linux `smp_mb()`
`fence r,rw`	앞의 읽기 → 뒤의 모든 접근	acquire (load 뒤에 둔다)
`fence rw,w`	앞의 모든 접근 → 뒤의 쓰기	release (store 앞에 둔다)
`fence w,w`	쓰기 → 쓰기	Linux `smp_wmb()`, 데이터 쓴 뒤 플래그 쓰기
`fence r,r`	읽기 → 읽기	Linux `smp_rmb()`, 플래그 읽은 뒤 데이터 읽기
`fence.tso`	앞의 읽기 → 뒤의 모든 접근, 앞의 쓰기 → 뒤의 쓰기 (쓰기 → 읽기만 빼고)	C++ `acq_rel` 펜스, TSO 코드 이식
`fence iorw,iorw`	I/O 포함 전부	Linux `mb()`, 장치 드라이버

SIMULATOR

FENCE 만들기

선행 집합 pred (비트 27–24)

후행 집합 succ (비트 23–20)

fence rw,rw 0x0330000f

fm (비트 31–28)

미리 정한 설정

비트를 눌러 집합을 바꾸면 아래 그림의 화살표(“앞의 이 연산은 뒤의 이 연산보다 먼저 보인다”)가 바뀐다. fence.tso를 고르면 쓰기→읽기 화살표만 빠지는 것을 확인하자. pause는 pred = W, succ = 0인 FENCE로, 아무 순서도 강제하지 않는 HINT 인코딩을 Zihintpause가 빌려 쓴 것이다.

리트머스 테스트로 모델 시험하기

메모리 모델은 리트머스 테스트(litmus test)라는 아주 짧은 다중 하트 프로그램으로 이야기한다. 각 테스트에는 “이 결과가 나올 수 있는가?”라는 질문이 하나 붙는다. 규격 부록(Explanatory Material)도 수십 개의 리트머스 테스트로 RVWMO의 미묘한 부분을 설명한다. 가장 유명한 네 가지를 보자. 모든 변수는 0에서 시작한다.

그림 11-7. 네 가지 고전 리트머스 테스트(FENCE 없음). 세로 화살표는 프로그램 순서, MP의 빨간 점선은 “y의 새 값을 읽었는데 x는 옛 값”이라는 문제의 관계다. 아래 줄은 각 결과가 모델별로 허용(✓)되는지를 보여 준다.

EXPLORER

리트머스 테스트 탐색기

하트 0의 두 연산 사이 하트 1의 두 연산 사이

증거 실행

테스트

증거를 보여 줄 모델

관심 결과—

SC—

TSO—

RVWMO—

MP에서 하트 0에 fence w,w만 넣으면 아직 허용, 하트 1에도 fence r,r을 넣어야 금지된다. 하트 1에 주소 의존성을 넣어도 막히지만 제어 의존성은 load를 묶지 못한다. SB에서는 fence.tso로는 부족하고 fence rw,rw(또는 fence w,r)가 두 하트 모두에 필요하다.

이 탐색기가 하는 일과 하지 않는 일

SC는 모든 끼워 넣기를, TSO는 하트별 FIFO 저장 버퍼 동작 모델(전달 포함, W를 pred에·R을 succ에 가진 FENCE만 버퍼를 비우게 함)을 전부 탐색한다. RVWMO는 각 하트의 두 연산이 PPO 규칙 1, 4–6, 9–11로 묶이는지 판단한 뒤, 그 제약을 지키는 모든 전역 메모리 순서를 나열하고 Load Value 공리로 load 값을 정한다. 이 네 테스트에는 같은 주소 load 쌍, AMO, LR/SC가 없어서 규칙 2·3·7·8·12·13과 Atomicity 공리가 관여하지 않는다. 더 복잡한 프로그램은 규격 부록이 소개하는 herd·rmem 같은 공식 도구로 확인해야 한다.

언어 원자 연산의 번역과 Ztso

프로그래머는 보통 FENCE를 직접 쓰지 않는다. C/C++의 std::atomic이나 Linux 커널의 동기화 함수가 메모리 모델을 감싸 준다. 규격 부록은 이 연산들을 RISC-V 명령으로 바꾸는 권장 매핑을 표로 싣고 있다. 아래는 그중 C/C++ 표(Table 16)의 핵심이다.

C/C++ 구문	RVWMO 매핑
`atomic_load(relaxed)`	`l{b\|h\|w\|d}`
`atomic_load(acquire)`	`l{b\|h\|w\|d}; fence r,rw`
`atomic_load(seq_cst)`	`fence rw,rw; l{b\|h\|w\|d}; fence r,rw`
`atomic_store(relaxed)`	`s{b\|h\|w\|d}`
`atomic_store(release)`	`fence rw,w; s{b\|h\|w\|d}`
`atomic_store(seq_cst)`	`fence rw,w; s{b\|h\|w\|d}`
`atomic_thread_fence(acquire)`	`fence r,rw`
`atomic_thread_fence(release)`	`fence rw,w`
`atomic_thread_fence(acq_rel)`	`fence.tso`
`atomic_thread_fence(seq_cst)`	`fence rw,rw`
`atomic_<op>(acquire / release / acq_rel / seq_cst)`	`amo<op>.{w\|d}.aq / .rl / .aqrl / .aqrl`
`atomic_<op>(seq_cst)`, LR/SC로	`loop: lr.{w\|d}.aqrl; <op>; sc.{w\|d}.rl; bnez loop`

그림 11-8. FENCE로 만든 acquire와 release. 빨간 화살표가 막히는 방향이다. Zalasr가 있으면 이 두 쌍은 각각 lw.aq 하나, sw.rl 하나로 줄어든다(규격 부록 Table 17이 이 “native load-acquire/store-release” 매핑을 제시한다).

섞어 쓸 때의 함정

부록의 LR/SC 매핑 표에는 별표 주석이 붙어 있다. load-acquire/store-release 명령을 쓰는 매핑(Table 17)에서 seq_cst RMW의 LR은 lr.aq로 충분해 보이지만, 기존 FENCE 기반 매핑(Table 16)으로 컴파일한 코드와 함께 돌아가려면 lr.{w|d}.aqrl이어야 한다. 매핑은 프로그램 전체가 같은 약속을 따라야 안전하다.

Ztso: TSO를 약속하는 확장

x86이나 SPARC용 코드는 TSO를 가정하고 FENCE 없이 쓰인 경우가 많다. Ztso(v1.0)는 새 명령 없이 “이 구현은 RVTSO를 따른다”는 약속만 추가한다. 규격의 정의는 RVWMO에서의 차이로 주어진다.

모든 load는 acquire-RCpc 표시가 있는 것처럼 동작한다.
모든 store는 release-RCpc 표시가 있는 것처럼 동작한다.
모든 AMO는 acquire-RCsc와 release-RCsc 표시가 모두 있는 것처럼 동작한다.

이 때문에 PPO 규칙 4–7을 뺀 나머지는 모두 중복이 되고, PW와 SR을 모두 갖지 않은(메모리) FENCE도 중복이 된다. 남는 재배치는 store → 뒤의 load 하나뿐이다. V 확장의 벡터 메모리 명령도 명령 단위로는 RVTSO를 따르지만, 한 명령 안의 원소 접근 순서까지 강해지지는 않는다.

규격 원문에서

“In spite of the fact that Ztso adds no new instructions to the ISA, code written assuming RVTSO will not run correctly on implementations not supporting Ztso.”

"Ztso" Extension for Total Store Ordering, Version 1.0 — 그래서 Ztso 전용으로 컴파일한 바이너리는 그 사실을 표시해, Ztso가 없는 플랫폼이 실행을 거부할 수 있게 해야 한다.

핵심 정리

저장 버퍼·비순차 실행·캐시 때문에 다른 하트는 내 메모리 접근을 다른 순서로 볼 수 있다. 메모리 모델은 허용되는 결과의 집합을 정한다.
RISC-V 기본 모델 RVWMO(v2.0)는 서로 다른 주소에 대한 네 종류(W→R, W→W, R→R, R→W) 재배치를 모두 허용하는 약한 모델이지만, 전역 메모리 순서가 하나인 multi-copy atomic 모델이다.
실행은 PPO를 지키고 Load Value·Atomicity·Progress 공리를 만족하는 전역 메모리 순서가 있으면 합법이다.
PPO 13규칙은 주소 겹침(1–3), 명시적 동기화(4–8: FENCE, acquire, release, RCsc, LR/SC 짝), 구문 의존성(9–11: 주소, 데이터, store로의 제어), 파이프라인 의존성(12–13)으로 나뉜다.
FENCE는 fm[31:28], pred[27:24] = PI PO PR PW, succ[23:20] = SI SO SR SW로 인코딩한다. fence.tso(fm = 1000, RW,RW)는 쓰기→읽기만 빼고 순서를 정한다.
MP·LB·2+2W의 문제 결과는 RVWMO에서만, SB의 0/0은 TSO와 RVWMO 모두에서 허용된다. MP는 fence w,w + fence r,r, SB는 양쪽 fence rw,rw로 막는다.
C/C++ acquire load는 l; fence r,rw, release store는 fence rw,w; s로 번역한다. Ztso는 모든 load·store에 RCpc acquire/release를 부여해 TSO를 약속한다.

확인 퀴즈

TSO에서도 허용되는 재배치는?

TSO의 유일한 완화는 저장 버퍼 때문에 생기는 store→load 재배치다. RVWMO는 네 가지 모두 허용한다.

MP 테스트에서 r1 = 1, r2 = 0을 RVWMO에서 막는 가장 가벼운 조합은?

쓰는 쪽은 데이터→플래그 쓰기 순서를, 읽는 쪽은 플래그→데이터 읽기 순서를 지켜야 한다. 제어 의존성은 load를 묶지 못한다. fence.tso는 W→W와 R→R을 모두 묶으므로 양쪽에 넣으면 막힌다.

PPO 규칙 11(제어 의존성)이 순서를 보장하는 경우는?

분기에 의존하는 store만 순서가 보장된다. 투기적 실행으로 분기 뒤의 load를 미리 실행하는 것은 허용된다.

fence.tso의 인코딩으로 옳은 것은?

fm = 1000, pred = RW(0011), succ = RW(0011)이다. 0x0330000f는 fence rw,rw, 0x0100000f는 pause, 0x0ff0000f는 fence iorw,iorw다.

하트가 자기 저장 버퍼의 값을 먼저 읽어 오는 것(전달)을 허용하는 RVWMO의 조항은?

Load Value 공리는 전역 순서상 앞선 store뿐 아니라 프로그램 순서상 앞선 같은 하트의 store도 후보로 삼는다. 그래서 load가 전역 순서에서 자기 store보다 앞에 있어도 그 값을 읽을 수 있다.

C/C++ atomic_store(memory_order_release)의 RVWMO 권장 매핑은?

release는 “앞의 모든 접근이 이 store보다 먼저 보이게” 해야 하므로 FENCE를 store 앞에 두고 pred = RW, succ = W를 쓴다.

Ztso에 대한 설명으로 옳은 것은?

Ztso는 명령을 추가하지 않는다. 그 대신 TSO를 가정한 코드는 Ztso가 없는 구현에서 틀리게 동작할 수 있으므로 바이너리에 표시해야 한다. 쓰기→읽기 순서가 필요하면 여전히 FENCE가 필요하다.

더 읽을거리

RVWMO Memory Consistency Model, Version 2.0 (Unprivileged ISA v20260120)
RVWMO Explanatory Material — 리트머스 테스트, 매핑 표(Table 12–17), 설계 근거
"Ztso" Extension for Total Store Ordering, Version 1.0
RV32I Base Integer Instruction Set — Memory Ordering Instructions (FENCE)
Sarita V. Adve, Kourosh Gharachorloo, “Shared Memory Consistency Models: A Tutorial” (IEEE Computer, 1996) — SC·TSO·약한 모델 입문의 고전
Daniel Lustig 외, RISC-V Memory Model Task Group의 공리적(Alloy/herd) 모델 — 규격 부록 “Formal Memory Model Specifications”