Send와 Sync: 안전성이 얹히는 술어, 그리고 그 하나의 구멍

지난 회의 병행 처리 설계는, 그 안전성 이야기의 전부를, 타입 시스템이 어느 값에 대해서나 답할 수 있어야 하는 두 물음에 얹는다: 다른 스레드로 move해 안전한가(그 성질을 Send라 부른다), 그리고 그것으로의 참조를 스레드 간에 공유해 안전한가(Sync). 그 두 술어를 올바르게 하면, 설계가 막기 위해 존재하는 데이터 경쟁은 일어날 수 없다; 틀리면, 보장 전체가 허구다. 이번 회는, 그것들이 어떻게 세워졌는가 —— 일부러 작게 —— 와, 그 작음이 숨기기를 허용한 미묘한 구멍에 대한 것이다.

trait 시스템이 아니라, 두 술어를 더

언어 전체가 도는 절제와 정합하여, Send와 Sync는 선언된 instance와 solver를 가진 trait 시스템이 아니다. 그것들은 구조적 술어 —— 타입을 받아, 그 타입의 형태를 보고 yes냐 no냐를 정하는 함수 —— 로, 언어가 이미 좇던 Trivial과 정리를 요하는 구별의 곁에, 넷째와 다섯째로 더해졌다. “이것은 region에 살 수 있는가?“에 답하는 것과 같은 기구가, 이제 “이것은 스레드를 넘을 수 있는가?“에도 답한다.

도출의 대부분은 기계적이다. 프리미티브는 Send이자 Sync. 튜플은, 그 요소 모두가 move해 안전하면 안전하다. 클로저와 채널은 move도 공유도 안전. region 대여 —— region에 묶인 참조 —— 는 결코 Send가 아니다. 이것은 작고 하중을 짊어지는 규칙이다: 대여가 넘을 수 없기에, 자식 스레드는 부모의 메모리로의 참조를 단순히 쥘 수 없고, “각 스레드는 자기 region을 얻는다” 보장이, 별도의 추적을 요하지 않고 공짜로 흘러 떨어진다.

구조로 부족한 곳은, 작성자가 타입에 표를 붙인다. 자원을 소유하는 능력은 move 가능하지만 단일 소유자이므로, Send지만 Sync가 아니다. 자기 자신의 내부 락을 가진 능력은 공유 가능이라 표시된다 —— Send도 Sync도. 생 파일 디스크립터 같은 본질적으로 단일 스레드인 무언가를 가진 능력은, 어느 쪽도 아니라 표시된다. 표는 나타나는 곳에서 authoritative; 표 없는 것은 그 구조에서 답을 도출한다. 그것은 꼭, 메모리 모델의 Trivial 규칙의 형태 —— 표시된 타입은 선언으로, 표 없는 타입은 그 내용으로 —— 를, 스레드 경계에 재사용한 것이다.

구멍: 이름에서 멈추다

그 도출에 건전성 버그가 있었고, 그것은 멈춰 설 가치가 있다. 구조적 방식이 낳는 정확한 위험이기 때문이다. 술어는 튜플을 올바르게 다뤘다 —— 튜플은 투명하고, 그 전 요소를 체크하는 것은 자연스러웠다. 하지만 이름 있는 레코드나 variant는 다르다: 그 이름은 하나의 것이고, 그 내용 —— 필드, 페이로드 —— 은 별개의 선언에 산다. 술어는, 표 없는 이름 붙은 타입을 만나면, 그 타입 인자를 체크했지만, 그 실제 내용까지 결코 꿰뚫어 보지 않았다. 이름에서 멈춘 것이다.

귀결은 진짜 구멍이었다. 일부러 Send가 아닌 타입 —— 생 디스크립터를 가진 연결, thread-local이라 표시된 —— 을 취한다. 그것을 한 줄의 레코드나 variant에 싼다: 단일 필드가 그 연결인 Box. 술어는, Box가 Send냐 물으면, Send가 아닌 타입 인자를 갖지 않는 표 없는 이름 붙은 타입을 보고, yes라 답했다 —— Box를 열어 안의 Send 아닌 연결을 찾는 것을 결코 하지 않았기에. 그것은, 설계가 스레드 경계를 넘는 것을 특별히 금하는 값을 취해, 사소한 레코드에 싸서, 가로막히지 않고 넘겨 건넬 수 있음을 뜻한다. 병행 처리 모델 전체가 불가능하게 하기 위해 세워진 바로 그 데이터 경쟁이, 래퍼 너머로 닿을 수 있었다.

구멍은 단순함의 그림자다

이 버그는 구현의 우연이 아니다; 지난 회에 이뤄진 선택의 특정한 리스크다. trait solver라면, 누군가 Box는 Send라고 선언할 것을 요하고, 컴파일러는 그 선언을 Box의 내용에 대해 검사했을 것이다 —— 거기의 구멍은, 거부된 선언으로서 자신을 알린다. 구조적 술어는 아무것도 선언하지 않는다; 그것은 잠자코 답을 도출한다. 그것은 더 가볍고 boilerplate를 요하지 않았다 —— 그리고 그것이야말로 구멍이 조용했던 이유다. 술어가 타입의 구조를 읽어 정할 때, 그것이 건전한 것은, 구조의 전부를 읽을 때뿐이다. 그 일부를 읽는 것은, 소리 높여 실패하지 않는다; 그것은 자신 있는, 틀린 yes를 돌려준다. Send와 Sync를 값싸게 한 절제는, 이 특정한 잘못을 가능하게 한 같은 절제다.

수정은 설계를 지키고, 틈을 닫는다. 표는 authoritative인 채 —— 표시된 타입의 답은 선언으로, 바뀌지 않는다. 표 없는 레코드나 variant에 대해, 술어는 이제 타입의 실제 내용을 끌어오고, 타입 파라미터를 치환하여 컨테이너의 요소 타입이 그것이 실제로 쥔 것으로 해결되게 하고, 그 내용으로 재귀한다 —— 이미 방문 중인 타입을 좇는 가드와 함께, 그래서 재귀적 타입(자기 자신을 참조하는 리스트 노드)이 체크를 무한 루프로 보낼 수 없다. 수정 후, 싸인 Send 아닌 값은 올바르게 Send가 아니고, 술어는 Trivial 규칙이 늘 그랬던 것과 꼭 같이 행동한다: 위에 표, 아래까지 죽 구조.

실패가 아니라, 봄으로써 찾아졌다

한 세부가 수정과 같은 만큼 중요하다: 구멍이 어떻게 찾아졌는가. 그것은 실패한 테스트에서 떠오른 것이 아니다 —— thread-local한 값을 레코드에 싸서 보내려는 테스트는 마침 없었고, 통과하는 스위트는 건전 하지 않은 술어 위에서 초록을 계속 보고했을 것이다, 무기한. 그것은 의도적인 감사로 찾아졌다 —— 같은 영역의 무관한 버그에 촉발된, Send/Sync 기구의 횡단적 리뷰로. 누군가, 물리기를 기다리는 것이 아니라, 보장의 구멍을 찾으러 갔다.

그것이, 이런 부류의 건전성 버그가 문제되기 전에 잡히는 유일한 길이다. 그 서명은 침묵이기에: 틀린 답은, 특정한 적대적 프로그램이 나타날 때까지, 옳은 답과 꼭 같아 보인다. 전부의 판매가 검증 가능한 올바름인 언어는, 자기 자신의 보장을, 가정하는 것이 아니라 능동적으로 공격되어야 할 것으로 다뤄야 한다 —— 그리고 연재가 몇 번이고 되돌아오는 정직한 자세는, 그 회의를 자기 자신의 타입 검사기에 겨누는 것을 포함한다.

값이 스레드 경계를 넘어도 되는가를 정하는 술어는, 이제 건전하다. 스레드 간에 값을 옮기는 다른 절반은, 값이 언제 건네졌는가를 좇고, 그 뒤의 사용을 잡는 것이다. 그것은 구조가 아니라 흐름의 문제이고, 그 자신의 미묘한 케이스를 가진다. 다음 회: move 추적.