shard — 저장소를 쪼개는 접근 단위
저장소 한 덩어리를 서로 겹치지 않는 조각으로 나눠 각 조각을 따로 바꿀 수 있게 한다. 조각을 대표하는 것이 토큰이고, 토큰은 “이 범위는 내 것” 이라는 권한이다. 그것을 여러 스레드에 태우든 순차로 돌든, 겹치지 않는다는 사실 자체가 값이다.
newtype grid u8 .
var r owned shard.token grid . be shard.open grid 8 .
var h shard.halves grid . be shard.split_at grid r 4 .
var lo owned shard.token grid . be (field h low) .
var hi owned shard.token grid . be (field h high) .
rem 이 뒤로 r 은 쓸 수 없다 --- 쓰면 E-OWN-MOVED막아 주는 것 — 그리고 누가 막는가
E-OWN-MOVED 다. 그것을 막는 것은 이 모듈이 아니라 언어다 — 토큰이 owned 라서 split_at 에 넘기는 순간 손을 떠난다. ② 남의 조각 자리를 만지면 write · read 가 false · none 으로 답한다(멈추지 않는다 — 실패는 값이다). ③ 다른 저장소의 토큰은 브랜드가 타입으로 달라 섞이지 않는다. 막아 주지 않는 것 — 쪼갠 동안 상대 조각을 읽기 전용으로 보기(동결 교차 읽기)와 region 단위 서로소 증명. 짓지 않았고, 짓지 않았다고 적는다.왜 새 문장 없이 지었나. 언어 설계 문서는 이 문제의 답으로 split region R into R1 … Rn by P 라는 새 문장을 적어 두었다. 그런데 언어에는 이미 둘이 있었다 — 브랜드(저장소의 정체성을 타입이 든다)와 owned(값이 하나뿐이고 넘기면 손을 떠난다). 둘을 곱하면 토큰이 곧 접근 단위다(19장).
| op | 모양 | 실패하면 |
|---|---|---|
token · halves | 조각 토큰 · 둘로 나눈 결과(low · high) | — |
open | comptime b, n u64 → owned token b | 없음(범위 0..n) |
split_at | comptime b, t owned token b, at u64 → halves b | 없음(at 은 범위로 잘린다) |
rejoin | comptime b, a owned token b, c owned token b → option (token b) | 순서 · 인접이 어긋나면 none |
covers | comptime b, t token b, i u64 → bool | — |
width | comptime b, t token b → u64 | 계약(op 이 스스로 적는 약속) 위반은 진입에서 멈춘다 |
write | comptime b, t, mem mut slice u64, i, v → bool | 범위 밖이면 false |
read | comptime b, t, mem slice u64, i → option u64 | 범위 밖이면 none |
표 50.1 — shard 의 op
rejoin 의 순서 규약 — 그리고 그것이 계약이 아닌 이유. 합칠 때는 낮은 id 를 먼저 넘긴다(교착 규약: 교차 획득은 언제나 오름차순). 어기면 none 이다. 처음엔 requires lt (field a id) (field c id) . 로 적었는데, 계약 시험 생성기가 두 구조체 인자 사이의 관계에 대해서는 거절 사례를 만들지 못한다. 아무도 검증하지 못하는 계약은 검사가 아니라 문장이므로, 부르는 쪽이 반드시 받는 값으로 내렸다.
반례. 거꾸로 합친다
shard.rejoin g hi lo 는 none 이다. 멈추지 않으므로 반환값을 보지 않으면 합쳐지지 않은 것을 모른 채 지나간다. guard is_some back . 으로 받는다.반례. 브랜드 하나로 저장소 둘을 연다
g 로 shard.open 을 두 번 부르면 컴파일 에러 E-BRAND-REUSED 다. 브랜드는 저장소 하나의 이름이다. 저장소가 둘이면 newtype 도 둘이다(브랜드는 자료를 나르지 않으므로 값이 0 이다).주의. 토큰은 var 에 묶는다(owned 는 가변 장소를 요구한다). split_at 의 at 은 잘린다 — 범위 밖이면 빈 조각이 나오고, 빈 조각은 아무것도 만지지 못하므로 안전하다. 뜨거운 경로에 동기화가 없다 — 토큰이 이미 권한을 말했으므로 남는 것은 범위 검사 하나이고, 시험이 방출된 C 에서 그 경로의 원자 연산 · 락이 0 임을 잰다. 이 모듈은 스레드를 모른다 — 토큰을 실행 단위에 태우는 것은 27장 의 일이다.