counter++는 한 줄이지만 read·modify·write 세 동작은 자동으로 하나가 아니다

두 실행 흐름이 같은 이전 값을 읽고 각각 계산한 결과를 저장하면, 나중 STORE가 앞선 변경을 덮어 기대한 증가 하나가 사라진다.

LOADr = counter

→

ADDr = r + 1

→

STOREcounter = r

1 · A LOADA가 0을 읽는다. 메모리 0.
2 · B LOADB도 0을 읽는다. 메모리 0.
3 · A STOREA가 계산한 1을 쓴다. 메모리 1.
4 · B STOREB도 “+1”이 아니라 계산해 둔 1을 써서 결과는 1.

Mutex · 복합 invariant

여러 필드와 검사·변경을 하나의 임계 영역으로 묶는다.

Atomic RMW · 단일 값

지원되는 fetch_add 같은 원자적 read-modify-write와 memory order를 쓴다.

Single owner · 메시지

한 실행 흐름만 상태를 바꾸고 나머지는 요청을 전달한다.

공유 + 쓰기같은 상태에 동시 접근하고 하나 이상이 쓰는 경로를 먼저 찾는다.

경계 완전성모든 reader·writer가 같은 lock 또는 atomic 계약을 따르는지 본다.

스케줄 강제반복·barrier·sanitizer로 문제 interleaving을 재현하고 최종 invariant를 검증한다.