두 변수로 메모리 순서 비교하기
순차 일관성의 여섯 교차 순서와 저장 버퍼 모형을 비교하고 장벽의 조건·실제 ISA의 경계를 설명합니다.
공유 메모리에서 같은 주소의 복사본 관계와 여러 주소의 순서는 다른 질문이었습니다. 이제 X·Y 두 변수의 작은 litmus 사례로 차이를 계산합니다. litmus는 특정 관측이 가능한지 묻는 짧은 동시 실행 예입니다.
초기 값·연산·관측을 고정하기
X=Y=0이며 각 읽기/쓰기는 중간이 쪼개지지 않는 원자적 연산입니다. 코어 A의 결과를 rA, 코어 B의 결과를 rB에 보관합니다. rA·rB는 각 코어의 로컬 값입니다. 괄호의 이름은 아래 시간표에서 쓸 연산 이름입니다.
| 코어 A의 프로그램 순서 | 코어 B의 프로그램 순서 |
|---|---|
| X=1 쓰기 (AX) | Y=1 쓰기 (BY) |
| Y 읽기 → rA (AR) | X 읽기 → rB (BR) |
질문은 “두 코어가 모두 0을 읽는 (rA,rB)=(0,0)이 가능한가?”입니다. 이 예제는 코드의 순서와 다른 코어에 쓰기가 보이는 순서를 구분하는 데 사용합니다. 언어 수준의 일반 변수로 데이터 경쟁을 일으킨 C/C++ 프로그램을 실행하여 CPU 규칙만으로 결과를 예측하는 예제가 아닙니다.
SC에서는 프로그램 순서를 지킨 한 줄을 만듭니다
순차 일관성(SC) 모형에서는 모든 메모리 연산을 한 줄의 전체 순서에 놓고, 각 코어의 프로그램 순서 AX<AR·BY<BR을 유지합니다. 읽기는 그 전체 순서에서 가장 최근 쓰기 또는 초기 값을 봅니다. 가능한 순서는 여섯 개입니다.
| 전체 순서 | rA, Y를 읽은 값 | rB, X를 읽은 값 |
|---|---|---|
| AX, AR, BY, BR | 0 | 1 |
| AX, BY, AR, BR | 1 | 1 |
| AX, BY, BR, AR | 1 | 1 |
| BY, BR, AX, AR | 1 | 0 |
| BY, AX, BR, AR | 1 | 1 |
| BY, AX, AR, BR | 1 | 1 |
00이 불가능한 이유를 부등식으로도 확인합니다. rA=0이면 AR<BY, rB=0이면 BR<AX입니다. 프로그램 순서 AX<AR와 BY<BR를 함께 연결하면 AX<AR<BY<BR<AX가 되어 한 전체 순서에서 성립할 수 없습니다. “프로그램이 겹쳐서 실행됐으니 모두 0일 수도 있다”는 추측은 SC의 순서 제약을 빠뜨린 것입니다.
저장 버퍼가 있으면 프로그램 순서와 공개 시점이 다릅니다
다음은 자체 정의한 약한 순서 교육 모형입니다. 각 코어가 쓰기를 자기 저장 버퍼에 넣고 다음 읽기를 진행할 수 있습니다. 다른 변수를 읽을 때는 공통 메모리에서 읽습니다. 이 사례는 자기 버퍼에 같은 주소의 pending write를 읽는 경우가 없어 store-to-load forwarding 규칙은 사용하지 않습니다. 각 쓰기는 나중에 한 번 flush되어 공통 메모리에 원자적으로 반영됩니다. 실제 CPU의 모든 메모리 모델을 이 규칙으로 대체하지 않습니다.
| 단계 | 사건 | 공통 X·Y | 저장 버퍼 | 관측 |
|---|---|---|---|---|
| 1 | A가 X=1을 버퍼에 넣음 | 0·0 | A: X=1 | — |
| 2 | B가 Y=1을 버퍼에 넣음 | 0·0 | A: X=1, B: Y=1 | — |
| 3 | A가 공통 Y 읽음 | 0·0 | 그대로 | rA=0 |
| 4 | B가 공통 X 읽음 | 0·0 | 그대로 | rB=0 |
| 5 | A의 쓰기 flush | 1·0 | B: Y=1 | 관측값은 이미 0 |
| 6 | B의 쓰기 flush | 1·1 | 비어 있음 | 최종 메모리만 1·1 |
최종 공통 메모리 X=Y=1이고 한 위치의 값이 합의돼도 이미 읽은 rA·rB가 00인 관측을 되돌리지 않습니다. 이 모형에서 coherence가 다루는 한 주소의 쓰기와 여러 주소 사이의 관측 순서는 다른 조건입니다.
전체 후보 순서를 실행으로 확인하기
permutations는 주어진 사건의 순서를 모두 나열합니다. index로 코어 내부의 선후 조건을 검사하고 허용하지 않는 순서는 버립니다. SC에서는 쓰기와 공개를 한 사건으로 두고, 저장 버퍼에서는 enqueue와 flush를 분리합니다. 아래 fenced는 각 코어의 쓰기 공개가 끝나야 뒤 읽기를 허용한다는 추가 제약입니다. 실제 ISA의 특정 fence 명령을 시뮬레이션한 것이 아닙니다.
from itertools import permutations
def outcomes(buffered=False, fenced=False):
events = ("AX", "AR", "BY", "BR", "AF", "BF") if buffered else ("AX", "AR", "BY", "BR")
results = set()
accepted = 0
for order in permutations(events):
constraints = [("AX", "AR"), ("BY", "BR")]
if buffered:
constraints += [("AX", "AF"), ("BY", "BF")]
if fenced:
constraints += [("AF", "AR"), ("BF", "BR")]
if any(order.index(first) > order.index(second) for first, second in constraints):
continue
accepted += 1
x = y = 0
ra = rb = None
for event in order:
if event == ("AF" if buffered else "AX"):
x = 1
elif event == ("BF" if buffered else "BY"):
y = 1
elif event == "AR":
ra = y
elif event == "BR":
rb = x
results.add((ra, rb))
return accepted, results
sc = {(0, 1), (1, 0), (1, 1)}
assert outcomes() == (6, sc)
assert outcomes(buffered=True) == (80, sc | {(0, 0)})
assert outcomes(buffered=True, fenced=True) == (20, sc)
for buffered, fenced in [(False, False), (True, False), (True, True)]:
count, values = outcomes(buffered, fenced)
print(count, sorted(values))memory_order.py로 실행하면 허용 사건 순서 수 6·80·20과 관측 집합을 출력합니다. 이 수는 코드 실행 전에 사건 자리를 세어 확인할 수 있습니다.
- SC의 네 자리에서 A의 두 사건 자리를 고르는 방법은
(1,2), (1,3), (1,4), (2,3), (2,4), (3,4)의 6개입니다. A 내부는 AX→AR, 남은 B 자리는 BY→BR로 고정됩니다. - 저장 버퍼 모형에서는 A 내부에
AX→AR→AF와AX→AF→AR두 순서가 있고, B 내부도 두 순서입니다. 여섯 자리에서 A가 차지할 세 자리를 고르는 방법은 20개입니다. 첫 A 자리가 1·2·3·4일 때 나머지 두 자리의 선택 수가 각각 10·6·3·1이므로 합은 20입니다. 총수는20×2×2=80입니다. - 양쪽 공개 대기는 A 내부를 AX→AF→AR, B 내부를 BY→BF→BR로 고정하므로 자리 선택 20개만 남습니다.
80은 모든 CPU에서 이 사례가 실행되는 횟수·확률이 아니라 위 제약을 만족하는 이 모형의 사건 배열 수입니다. 코드의 Python 스레드를 실제 동시 실행한 결과도 아닙니다. results는 같은 (rA,rB)를 여러 번 세지 않는 집합이므로 사건 배열 수와 서로 다른 관측값 수를 구분합니다.
장벽이 해결하는 범위를 고르기
두 코어 모두 쓰기 enqueue→그 쓰기의 공개 완료→읽기를 강제하면 SC와 같은 관측 집합이 남습니다. 한 코어에만 이 제약을 두면 다른 코어의 읽기와 쓰기 공개가 앞서거나 늦어져 00을 배제할 수 없습니다. 장벽을 넣을 위치와 필요한 순서 쌍을 지정해야 합니다. 순서 장벽을 추가해도 잃어버린 갱신의 read-modify-write가 자동으로 원자적이 되지는 않습니다.
RISC-V 공식 RVWMO 규격 소스는 global memory order, preserved program order, fence·acquire/release 조건을 정의합니다. 이 절은 그 전체 제약을 구현한 검증기가 아니며 store buffer를 설명하기 위한 작은 자체 모형입니다. 실제 ISA 결과, 컴파일러 변환, 캐시 protocol 상태, I/O 순서는 이 실행으로 검증하지 않았습니다.
독립 문제: 한 코어의 공개만 기다리면
A에서는 X의 flush가 AR보다 먼저 일어나야 합니다. B에서는 BY 뒤의 BR 실행을 허용하지만 Y의 flush를 기다리지 않습니다. 00이 가능한 사건 순서를 쓰세요. 최종 X·Y=1이라는 사실이 rA·rB도 1임을 뜻하는지 설명하세요.
힌트
B가 X의 공개 전에 읽고, A가 Y의 공개 전에 읽게 놓습니다. A의 프로그램 순서와 flush 제약은 모두 지켜야 합니다.
풀이
예를 들어 BY enqueue→BR(X=0)→AX enqueue→AF(X=1 공개)→AR(Y=0)→BF(Y=1 공개)입니다. A의 공개 대기 조건을 지켜도 B는 0을 읽을 수 있으므로 관측은 00입니다. 나중에 flush로 갱신된 최종 메모리는 과거에 읽은 로컬 관측을 바꾸지 않습니다. 다음 성능과 종합 추적에서 값의 정확성과 접근 비용을 함께 구분합니다.