RustBelt 연구에서 제안한 "공유 불변식" 개념을 통해, 내부 가변성이 있는 타입에서 공유 참조를 안전하게 모델링하는 방법을 설명한다. 타입이 소유 모드와 공유 모드라는 두 얼굴을 갖는다는 관점에서, `Cell`과 `Mutex` 같은 사례를 통해 `&T`의 의미가 타입별로 어떻게 달라지는지를 논의한다.
This post is about an aspect of the RustBelt paper. Concretely, I’d like to share some of our thoughts on the nature of types and shared references. Let’s see how well this goes. :)
공유 참조(shared reference)는 Rust 타입 시스템에서 극도로 강력한 메커니즘이며, 이를 우리의 형식적 모델에서 잘 다루는 방법을 찾는 데 꽤 애를 먹었습니다. 이 글에서는 우리가 고안한 모델을 소개합니다. 먼저 타입의 “모델”이 무엇을 의미하는지, 그리고 공유 참조를 다루는 일이 왜 그렇게 어려운지 이야기하는 것으로 시작하겠습니다.
공유 참조가 미묘한 이유는 내부 가변성 때문입니다. 이는 공유 참조의 본질을 근본적으로 바꿔 놓습니다. 이를 이해하기 위해, 잠시 Rust가 내부 가변성을 허용하지 _않는다_고 가정하고, Rust 타입의 모델이 대략 어떻게 보일 수 있는지 설명하겠습니다.
이미 “의미(semantic) 타입”이라는 생각에 대해 이전에 적은 바 있는데, 요지는 타입이 필드에 대해 self.cap >= self.len(예: Vec) 또는 !is_zero(self.0)(예: NonZero) 같은 _추가적인 불변식(invariants)_을 부과할 수 있다는 개념입니다. 그러므로 여기서 제가 “(의미) 타입”이라고 말할 때는, 사실상 “타입의 (구문적) 정의(즉 데이터 레이아웃) 그리고 이 타입에 대해 모듈이 부과하는 추가 불변식”을 의미합니다. 두 타입이 구문적으로 같더라도 서로 다른 불변식을 가질 수 있고, 그런 경우 한쪽에서 다른 쪽으로 캐스팅하는 것은 끔찍하게 안전하지 않을 것입니다. 즉 구문적으로 비슷해 보여도 완전히 다른 타입인 셈입니다. 타입에서 진짜 중요한 것은 이 질문에 대한 답입니다: 어떤 바이트 시퀀스가 주어졌을 때, 이 시퀀스가 그 타입의 올바른 값인가? 1 모든 Rust 타입에 대해 이 질문에 답할 수 있다면, 우리는 Rust 타입 시스템의 “(의미) 모델”을 찾은 것입니다. (구문적) 데이터 레이아웃은 허용되는 시퀀스에 기본적인 구조(예: 길이)를 부과하지만, 불변식은 추가 요구사항을 부과함으로써 해당 타입에서 허용되는 시퀀스 집합을 임의로 _정제(refine)_할 수 있습니다. (실제로 정제 타입(refinement types)은 이러한 추가 제한을 타입 시스템에 반영하는 한 방법이지만, 오늘 이야기하고 싶은 주제는 아닙니다.)
예를 들어, 0 바이트 네 개의 시퀀스는 i32에서는 유효하지만 NonZero<i32>에서는 유효하지 않습니다. 또 다른 예로, 어떤 포인터가 Box<i32>에서 유효하려면 소유된 메모리2의 네 바이트를 가리켜야 하고, 그 네 바이트는 유효한 i32여야 합니다. 마지막으로, 어떤 포인터가 &'a mut T에서 유효하려면 size_of::<T>() 바이트의 메모리3를 가리켜야 하고, 그 메모리는 라이프타임 'a 동안 빌려진(borrowed) 상태여야 하며, 그 바이트들은 T에서 유효해야 합니다.
따라서 우리 모델에서 공유 참조를 다루는 길은 명확해 보입니다: 포인터가 &'a T에서 언제 유효한가를 알아내면 됩니다. 내부 가변성을 무시하면, 이 질문은 상당히 쉽게(지금은 완전히 형식화하려는 것이 아니므로 더욱 그렇죠 ;) 답할 수 있습니다: 라이프타임 'a가 지속되는 동안, 포인터는 size_of::<T>() 바이트의 불변(immutable) 메모리를 가리켜야 합니다(즉 이 라이프타임 동안 바이트가 변하지 않음; 그 전후의 변경에는 제약을 두지 않음). 그리고 그 바이트들은 T에서 유효해야 합니다.
이 모델을 바탕으로, 왜 T: Copy일 때 임의의 x: &'a T에 대해 *x가 가능한지 설명할 수 있습니다: 접근은 오직 라이프타임 'a 동안에만 발생할 수 있으므로, 포인터를 역참조할 수 있습니다. 게다가 T: Copy이므로, 우리는 바이트를 복사하여 원본과 복사본 둘 다 T에서 유효하게 만들 수 있다는 것을 압니다(“유효한 시퀀스”라는 것이 Box<i32>처럼 소유권 요구사항을 부과할 수도 있으므로, 이런 복제는 모든 T에 대해 일반적으로 가능하지는 않습니다). 마지막으로, 메모리가 불변임을 알고 있으므로, 메모리를 완전히 소유하지 않았더라도 이 접근을 수행할 수 있습니다: 다른 모든 코드(예: 다른 스레드) 역시 이 메모리에서 읽기 작업만 수행한다고 신뢰할 수 있습니다. 전체적으로, 우리는 x에 부과된 불변식을 위반하지 않았고, 우리가 복사한 데이터는 유효한 T라고 결론 내릴 수 있습니다.
하지만 내부 가변성은 &'a T에 대한 이 모델을 깨뜨립니다. 우리는 일반적으로 가리키는 메모리가 읽기 전용이라고 선언할 수 없습니다. 그렇게 하면 Cell::set 같은 많은 연산이 노골적으로 안전하지 않게 됩니다. 실제로 이 때문에 공유 참조가 “불변 참조”라고 불리지 않으며, 비록 보통 가변 참조의 쌍대(dual)로 여겨지긴 합니다. (개인적으로는 가변 참조를 “고유 참조(unique reference)”라고 불러야 한다고 생각합니다. 두 참조의 구분은 가변성보다는 고유성의 문제라는 점을 각인시키기 위해서죠. 뭐 어쨌든요.)
그렇다면 기존 모델이 깨진 상황에서, 대신 무엇을 할 수 있을까요? 몇 가지 예를 살펴보겠습니다.
&Cell<T>왜 Cell::set은 안전한 연산일까요? 이유는 두 가지입니다. 첫째, Cell<T>는 Sync가 아니므로, &Cell<T>를 한 스레드에서 다른 스레드로 보낼 수 없습니다. 그 결과, 어떤 Cell에 대한 모든 공유 참조는 항상 같은 스레드에 존재합니다. 이는 이미 데이터 레이스의 가능성을 배제합니다. 둘째, Cell<T>는 데이터로의 깊은 포인터(deep pointer) 획득을 허용하지 않습니다. 따라서 Cell<Result<bool, i32>>를 Ok(true)에서 Err(42)로 바꿔도, Result 내의 bool을 기대하는 포인터를 무효화하지 않습니다.
우리 모델로 돌아오면, &'a Cell<T>는 다음과 같이 말할 수 있습니다: 이것은 size_of::<T>() 바이트의 메모리를 가리키는 포인터인데, 'a 동안 현재 스레드에서 실행 중인 모든 코드가 접근할 수 있지만, 다른 코드에서는 접근할 수 없다; 그리고 그 바이트들은 T에서 유효하다. 이 정의는 &Cell<T>가 Send가 아님을(모델이 “현재 스레드”를 참조하므로 스레드를 바꾸면 불변식이 깨질 수 있음) 강제하고, 따라서 Cell<T>가 Sync여서는 안 됨을 뜻합니다. 또한 Cell<Result<bool, i32>> 안쪽으로의 포인터를 금지합니다: 예컨대 Ok 데이터에 대한 포인터, 즉 &Cell<bool> 타입의 포인터를 갖고 싶다고 해봅시다. 이 포인터가 해당 타입에서 실제로 유효하다는 것을 보일 수 없습니다. 왜냐하면 현재 스레드의 누구든지 (바깥) Cell<Result<bool, i32>>를 언제든 수정할 수 있고, 거기에 Err(42)를 쓰면 &Cell<bool>이 항상 유효한 bool을 가리켜야 한다는 요구사항을 위반하게 되기 때문입니다! 따라서 위에서 논의한 두 제한은 &Cell<T>에 대한 불변식으로부터 직접적으로 따라옵니다.
&Mutex<T>Mutex의 경우, 왜 Mutex::lock과 MutexGuard::deref_mut이 안전한 연산인지에 대한 정당화는 다시 다릅니다: Mutex는 이름에서도 알 수 있듯 _상호 배제(mutual exclusion)_를 구현하여, 한 번에 오직 하나의 스레드만이 락을 보유할 수 있습니다. 결과적으로, 그 스레드에게 내부 데이터에 대한 가변 접근을 부여하더라도 다른 스레드와의 데이터 레이스나 기타 충돌을 일으키지 않습니다.
모델에서는(여기서는 점점 더 많은 세부사항을 생략하겠습니다) &'a Mutex<T>가 유효하다는 것은, 라이프타임 'a 동안 그 포인터가 가리키는 메모리에 접근하는 모든 이가 락킹 규율을 준수한다는 뜻이라고 하겠습니다. MutexGuard는 대응되는 Mutex의 락을 실제로 소유하고 있을 때 유효합니다. 이 둘을 합치면 모든 Mutex와 MutexGuard 연산의 안전성을 정당화하기에 충분합니다.
이제 다시 질문으로 돌아갑니다: 언제 포인터가 타입 &'a T에서 유효할까요? 위에서 보았듯이, 이 질문에 대한 답은 실제로 타입 T에 크게 의존합니다! i32나 bool에 대해서는 우리의 옛 읽기 전용 모델이 여전히 통하지만, Cell이나 Mutex에 대해서는 각각의 타입에 매우 특화된 완전히 다른 불변식이 필요합니다.
이 다양성을 다루기 위해서는, 타입이 무엇인지에 대한 우리의 생각을 바꿔야 합니다. 앞서 타입은 이 질문에 관한 것이라고 했습니다: 어떤 바이트 시퀀스가 주어졌을 때, 이 시퀀스가 그 타입의 올바른 값인가? 이제 우리는 타입이 다음 질문에도 답할 수 있어야 한다고 확장합니다: 어떤 포인터와 라이프타임이 주어졌을 때, 이 포인터가 주어진 라이프타임 동안 이 타입에 대한 유효한 공유 참조인가? 다시 말해, 모든 타입은 공유가 무엇을 의미하는지 스스로 _선택_할 수 있습니다.
이 점을 곱씹는 동안, 왜 Rust에 Send와 Sync가 모두 있는지, 그리고 겉보기에는 밀접해 보이는데도 왜 서로가 서로를 함의하지 않는지를 설명할 수 있습니다. 저는 이 마커 트레잇들을 처음 배울 때 꽤 혼란스러웠습니다. 이유는 T와 &T가 사실 매우 다른 타입이기 때문입니다. T의 작성자는 두 타입(대체로) 독립적으로 불변식을 선택합니다. 따라서 그중 하나를 다른 스레드로 보내는 것이 안전하다고 해서, 다른 하나에 대한 결론은 도출되지 않습니다.
이 선택의 주된 결과는, 추가 불변식을 가진 모든 타입에 대해 두 가지 불변식을 선택해야 한다는 것입니다:
원칙적으로 이는 Vec처럼 내부 가변성 자체에는 관심이 없는 타입을 포함해 모든 타입에 적용됩니다. 하지만 &Vec<Mutex<T>> 같은 타입을 다뤄야 하므로, 이 문제를 건너뛸 수는 없습니다. 기능으로서의 내부 가변성은 타입 시스템 전체에 “전염”됩니다. 다만 이는 보통 큰 문제가 되지 않아야 합니다: &'a Vec<T>는 len과 cap이 읽기 전용이고, 벡터의 초기화된 모든 원소가 스스로 'a 동안 공유된다는 불변식을 가지면 됩니다. “내부 타입”의 공유 불변식을 그대로 사용하고 나머지를 읽기 전용으로 두는 전략은 대다수 타입에 적용 가능할 것입니다.
물론, 하나의 타입을 이루는 두 불변식이 완전히 무관할 수는 없습니다. 우선, 어떤 y: T가 주어지면, 이를 어떻게든 “공유를 시작”하여 &y: &T를 얻을 수 있어야 합니다. 또한 T: Copy라면, x: &T에 대해 *x를 읽어 T의 복사본을 얻을 수 있어야 합니다. 공유를 읽기 전용 메모리로 균일하게 정의했던 첫 번째 모델에서는 자동으로 성립했지만, 이제 공유를 “구성 가능”하게 만들었으니 이 성질을 명시적으로 요구해야 합니다.
하지만 이것만으로는 충분치 않습니다: 언젠가 공유는 끝나고, 프로그램의 어떤 부분은 다시 소유 불변식이 성립하길 기대합니다. 공유가 시작될 때 일어난 모든 일은 어떤 식으로든 되돌려져야 합니다 — 저는 이것을 “공유 해제(un-sharing)”로 생각합니다. 이것이 까다로운 이유는 공유 참조가 말 그대로 공유될 수 있기 때문입니다(당연하죠). 단순한 읽기 전용 공유의 경우조차, 공유 참조가 커버하는 메모리에 대해 아무도 더 이상 옛 읽기 전용 접근을 사용하지 않음을 보장해야 합니다. Rust에서는 공유 해제가 일어날 때, 그 옛 공유 참조들의 라이프타임이 만료되므로 이것이 가능합니다.
그래서 우리 모델에서는 _공유가 본질적으로 라이프타임과 연결_됩니다. 앞서 타입이 두 불변식으로 이뤄진다고 말한 것을 되돌아보면, 두 번째 불변식은 어떤 T의 값이 어떤 라이프타임 동안 공유되는 것에 관한 것임을 알 수 있습니다. 라이프타임 없는 공유는 없습니다. 무언가를 공유하기 시작할 때마다(즉, 이전에 소유하던 데이터에서 &x를 만들 때마다), 우리의 모델은 이 공유가 지속될 라이프타임을 선언할 것을 요구합니다. 라이프타임이 끝나면, 공유 해제가 자동으로 일어나므로 모델에서 이를 따로 명시할 필요가 없습니다. (물론, 이와 관련된 증명 작업이 사라지는 것은 아닙니다. 이제 우리는 특정 라이프타임 동안만 소유한 것들로 무엇을 할 수 있는지에 대한 규칙을 따라야 하며, 그 규칙은 공유 해제가 항상 가능하도록 충분히 제한적입니다.)
이 글에서는 내부 가변성을 다루기 위해 RustBelt 논문에서 고안한, 타입이 별도의 “공유 불변식”을 갖는다는 아이디어를 설명했습니다. 제가 아는 한, 이는 지금까지 내부 가변성에 대한 유일한 형식적 고찰이었고, 우리 모두가 작동하는 접근법을 찾을 때까지 일종의 시행착오를 겪었습니다. 이것이 내부 가변성에 대한 최종 결론이라는 뜻은 아닙니다. Mutex<T>나 Cell<T>가 왜 안전한지 정당화하는 다른 방법들도 있을 수 있습니다.
어쨌든 이 모델은 RustBelt의 형식 작업뿐 아니라 Rust 타입 시스템 자체를 생각하는 데에도 제게 큰 도움이 되었습니다. 예컨대, 저는 잠시 왜 Cell이 공변(covariant)이 아닌지 궁금했습니다. 실제로 T <: U라면, Cell<T>를 Cell<U>로 바꾸는 것은 완전히 안전합니다 — 즉 어떤 바이트 시퀀스가 Cell<T>에서 유효하다면, 그것은 Cell<U>에서도 유효합니다. (사실 Cell<T>의 소유 불변식은 T의 것과 _완전히 동일_합니다!) 이것이 바로 우리가 공변성에 필요로 하는 것이죠, 그렇지 않나요? 음, 꼭 그렇지는 않습니다 — 우리의 타입에는 두 불변식이 있으므로, 포인터가 공유된 Cell<T>일 때 그것이 공유된 Cell<U>이기도 해야 한다는 요구도 필요합니다. 그런데 이것은 결정적으로 참이 아닙니다! 따라서 소유된 Cell은 공변이지만, 공유된 Cell은 아닙니다. 소유 서브타이핑과 공유 서브타이핑을 분리하는 Rust 타입 시스템의 확장을 생각해볼 수 있고, 그렇다면 Cell은 실제로 “소유-공변(owned-covariant)”이 될 수 있을 것입니다.
이 글을 마치며, 좀 더 일반적인 생각을 남기고자 합니다. Rust 타입 시스템에서 공유 참조의 역할을 더 추상적으로 설명하는 한 가지 방법은, &T가 T를 “공유 모드(shared mode)”로 전환한다는 것입니다. 모든 타입은 “소유(owned)”와 “공유(shared)”라는 두 모드를 갖고 있으며, 우리는 보통 x: T에 관련된 “소유” 모드만을 생각합니다. 하지만 Rust는 다른 모드로 전환하는 방법을 제공하고, 그곳에서 타입은 완전히 다른 “얼굴”을 가질 수 있습니다 — 예를 들어, Cell<T>와 T는 “소유” 모드에서는 _동일_하지만, “공유” 모드에서는 매우 다릅니다. 저는 이와 비슷한 개념을 가진 다른 타입 시스템을 알지 못합니다. 그럼에도 Rust의 공유 참조가 초특별한 마법 같은 기능으로 논의되는 것을 본 적은 없습니다(하지만 이 연구를 하고 나니, 정말 그렇다고 생각하긴 합니다!). 오히려 고유한 성질 때문에 가변 참조가 특별해 보입니다(그리고 이것은 mutpocalypse라 불린 혁명이었죠). 그러니 어쩌면 이것은 Rust 개발자들이 심지어 자각하지 못한 채로 떠올린 극히 영리한 아이디어일 수도 있고, 아니면 우리 모델의 부산물일 뿐이라 길게 논할 가치가 없는 것일 수도 있습니다. (물론 제 의견은 있죠. ;)
그리고 또 다른 질문이 있습니다: 왜 정확히 두 모드일까요? 더 많은 모드를 갖는 것이 가치가 있을까요? 솔직히 모르겠습니다만, 예전에 glaebhoerl의 이 글을 읽었을 때 그런 생각을 했습니다. 그 글의 첫 부분을 저는 “Cell을 하나의 모드로 볼 수 있다”라고 번역하고 싶습니다.
의견이나 생각이 있으시다면 Rust 포럼의 논의에 참여해 주세요! 또한 이 글이 얼마나 이해하기 쉬웠는지에 대한 피드백도 환영합니다. 연구 결과를 블로그 글로 번역해 본 것은 이번이 처음이라서요.
여기서 “바이트 시퀀스”라는 개념은 초기화되지 않은 메모리나 포인터 같은 복잡성 때문에 미묘하다는 점을 언급해야 합니다. 이 주제로는 나중에 다시 돌아오고 싶고, 이 글에서는 크게 중요하지 않을 것입니다.↩
또한 소유권(ownership) 개념을 어떻게 더 정밀하게 만들 수 있는지에 대해서는 대부분 무시하겠습니다. 더 파고들고 싶으시다면 키워드는 분리 논리(separation logic)입니다. 우리는 차용을 다루기 위해 분리 논리를 확장해야 했지만, 이 모든 세부사항은 이 글과 크게 관련이 없습니다. 그게 계획입니다, 아무튼.↩
네, 여기서는 크기가 정해지지 않은 타입(unsized types)은 무시합니다.↩