spsc — 락 없는 SPSC 링 버퍼
스레드 사이로 값을 넘기는 가장 단순한 방법은 락이다. 그런데 생산자가 하나, 소비자가 하나뿐이면 락이 필요 없다 — 생산자는 tail 만 쓰고 소비자는 head 만 쓰며, 서로의 것은 원자적으로 읽기만 한다. 이것이 SPSC(single-producer single-consumer)이고, 락 없는 구조 중 정직하게 짧은 거의 유일한 것이다.
생산자 하나 · 소비자 하나가 계약이다
push 하거나 두 스레드가 pop 하면 이미 SPSC 가 아니고, 이 모듈은 그것을 막지 못한다. 그래서 peek · drain 같은 편의 op 을 넣지 않았다 — 편의 op 이 늘수록 그 계약을 어기는 방법이 늘어난다. 표준 라이브러리에서 작은 표면은 게으름이 아니라 계약을 지키는 수단이다. MPSC · MPMC · seqlock 은 없다 — CAS 재시도와 ABA 가 붙으면 검증되지 않은 코드를 표준으로 만드는 일이 된다.한 칸을 늘 비워 둔다. 그래서 실제 용량은 len buf − 1 이다. 그 대가로 head == tail 이 언제나 “비었다” 를 뜻하고 가득 참과 헷갈리지 않는다.
| op | 하는 일 | 돌려주는 것 |
|---|---|---|
spsc_capacity buf | 담을 수 있는 최대 개수 | len buf − 1 |
spsc_push k ctl buf v | 밀어 넣기(생산자 전용) | 1 성공 · 0 가득 참 |
spsc_pop k ctl buf out | 꺼내기(소비자 전용), 값은 out[0] 에 | 1 성공 · 0 비었음 |
spsc_count_about k ctl buf | 지금 개수(관찰값) | 개수 |
표 50.1 — spsc 의 op
ctl 은 길이 2 이상의 mut slice u64 로 [0] = head(소비자), [1] = tail(생산자)이다. k 는 cap atomic — 공유 자리를 원자적으로 만질 권한이다. count_about 에 about 이 붙은 이유 — 읽는 순간 이미 달라졌을 수 있다. 이름이 그것을 말하지 않으면 쓰는 사람이 그 값을 믿는다.
무엇이 이 코드를 받치나. 두 가지 증명이다. 첫째, 색인을 mod … (len buf) 로 감싸면 언제나 범위 안이다 — lowentc --emit-proof lib/spsc.low 가 링 버퍼의 두 접근(index, index.store)과 색인을 올리는 두 덧셈의 검사가 증명으로 사라졌다고 적는다(41장). 둘째, 데이터 쓰기 → 색인 공개 → 색인 관찰 → 데이터 읽기가 약한 메모리 모델(RC11)에서 데이터를 나른다 — 그리고 알고리즘 자체의 정확성(성공하면 자원이 버퍼로 넘어가고 실패하면 되돌아온다)은 기존 증명(gpfsl 의 circ_buff)을 빌렸다. 우리 spsc_push 가 그 증명의 코드와 한 줄씩 같다는 대응은 사람이 읽어 확인한 것이고 기계 검증되지 않았다(47장).
순서(ordering)는 필요한 만큼만 세다. 생산자가 head 를 읽을 때는 acquire(소비자가 공개한 것), 자기 tail 을 읽을 때는 relaxed(내가 쓴 값), tail 을 공개할 때는 release(앞의 데이터 쓰기가 먼저 보여야 한다)다. 소비자 쪽은 대칭이다. 넷 중 동기화가 필요한 자리는 둘뿐이다. 이 표기(order <이름>)는 한때 파서 결함으로 한 번도 닿지 못했고, 이 라이브러리를 쓰려다 드러나 고쳤다 — 쓰지 않는 기능은 있어도 없는 것이다.
확인하는 것 — 빈 것에서 꺼내기 실패, 가득 참에서 넣기 실패, FIFO, 링을 한 바퀴 넘겨도 그대로. 그 시험은 단일 스레드다(VM 이 단일 스레드다). 진짜 두 스레드에서의 메모리 순서의 정당성은 실행이 아니라 증명이 준다 — 둘을 섞지 않는다.