Rust 표준 라이브러리에 도입된 Pin API를 RustBelt 타입 모델로 확장하여 형식적으로 고찰하고, Pin/PinBox/Unpin의 의미와 안전성 보증을 공리와 불변식을 통해 설명한다.
최근 표준 라이브러리에 “고정된 참조(pinned references)”를 위한 새 API가 불안정 기능으로 추가되었습니다. 이 참조의 목적은, 그것이 가리키는 메모리의 데이터가 결코 다른 곳으로 이동되지 않을 것임을 표현하는 데 있습니다. @withoutboats는 이 기능이 async IO의 맥락에서의 문제를 어떻게 해결하는지에 관해 글을 썼습니다. 이 글에서는 그 API를 보다 면밀하고 형식적으로 살펴보겠습니다. 구체적으로 RustBelt의 타입 모델을 확장하여 pinning을 지원하는 시도를 해 보겠습니다.
하지만 시작하기 전에, 몇 가지 기초를 정리하고 가겠습니다.
이전에 제 Rust 타입 모델을 다른 글에서 논의했습니다. 이 글을 출발점으로 사용할 것이므로, 지금 읽어 보시면 좋습니다. 짧게 말하자면, 개인적인 불변식을 가진 Rust 타입은 단일한 불변식을 가지는 것이 아니라, 그 타입이 놓일 수 있는 서로 다른 “모드”를 반영하는 여러 불변식을 가진다고 봅니다. @cramertj가 여기서의 용어로 “타입 상태(typestate)”를 제안했고, 저도 그 표현이 타당하다고 생각합니다.
정의 1: Rust 타입. 모든 Rust 타입
T는 각각 불변식을 가진 두 개의 타입 상태를 갖는다:
- 소유(owned) 타입 상태: 불변식
T.own(bytes)(여기서bytes: List<Byte>)는 주어진 바이트 시퀀스가 완전히 소유된 유효한T를 구성하는지를 말한다.- 공유(shared) 타입 상태: 불변식
T.shr('a, ptr)(여기서'a: Lifetime,ptr: Pointer)는ptr이 수명'a동안 공유된T인스턴스를 가리키는 유효한 포인터인지를 말한다.또한, 다음 공리가 항상 성립한다는 의미에서 이 두 상태는 연결되어야 한다:
- 만약 우리가 수명
'a동안,T.own(bytes)가 성립하는 바이트 목록bytes를 가리키는 포인터ptr을 빌렸다면, 공유 타입 상태로 전환하여T.shr('a, ptr)을 얻을 수 있다. (암묵적으로, 원래의 대여가 끝나면 타입은 소유 타입 상태로 되돌아간다.)이 공리는 우리가 소유하고 있는 것에 대한 공유 참조를 만들 수 있음을 보장한다.
여기서 공유가 왜 별도의 타입 상태인지 궁금할 수 있습니다. 누군가 다른 사람이 소유한 T에 대한 읽기 전용 접근으로만 읽히면 되지 않느냐고요? 하지만 이는 &Cell에서는 명백히 맞지 않습니다. 내부 가변성(interior mutability)이 있는 타입을 설명하기 위해서는 공유를 별도의 상태로 취급해야만 합니다. 이전 글에서 이를 자세히 설명했지만, 간단한 예로 RefCell을 완전히 소유하고 있다면 첫 번째 필드(현재의 reader/writer 수를 저장하는 필드)는 특별한 의미를 가지지 않는다는 점을 생각해 보세요. 이는 RefCell::get_mut이 그 필드를 무시하는 것으로도 알 수 있습니다. 사실 RefCell::reset(&mut self) 같은 메서드를 추가해 그 필드를 0으로 초기화해도 안전할 것입니다.
이제 pinning을 지원하도록 타입의 개념을 확장해 봅시다. pinning API의 핵심은 새로운 참조 타입 Pin<'a, T>입니다. 이 타입은 “가리키는 데이터가 그 위치에 계속 남아 있을 것”, 즉 이동되지 않을 것을 보장합니다. 중요한 점은, pinning이 “이동 불가능한 타입”을 제공하지는 않는다는 것입니다! 데이터는 그것을 가리키는 Pin<T>가 생성된 이후에만 pinned 상태가 되며, 그 전에는 자유롭게 이동될 수 있습니다.
관련 RFC는 전혀 새로운 API 표면 전체를 꽤 자세히 설명합니다: Pin, PinBox, 그리고 Unpin 마커 트레이트. 여기서는 이를 반복하지 않고, Pin 참조를 어떻게 사용하고 그 보장을 어떻게 활용하는지 하나의 예만 보이겠습니다:
#![feature(pin, arbitrary_self_types, optin_builtin_traits)]
use std::ptr;
use std::mem::Pin;
use std::boxed::PinBox;
use std::marker::Unpin;
struct SelfReferential {
data: i32,
self_ref: *const i32,
}
impl !Unpin for SelfReferential {}
impl SelfReferential {
fn new() -> SelfReferential {
SelfReferential { data: 42, self_ref: ptr::null() }
}
fn init(mut self: Pin<SelfReferential>) {
let this : &mut SelfReferential = unsafe { Pin::get_mut(&mut self) };
// self_ref가 this.data를 가리키도록 설정한다.
this.self_ref = &this.data as *const i32;
}
fn read_ref(self: Pin<SelfReferential>) -> Option<i32> {
let this : &SelfReferential = &*self;
// self_ref가 NULL이 아니면 역참조한다.
if this.self_ref == ptr::null() {
None
} else {
Some(unsafe { *this.self_ref })
}
}
}
fn main() {
let mut s = PinBox::new(SelfReferential::new());
s.as_pin().init();
println!("{:?}", s.as_pin().read_ref()); // Some(42)를 출력
}
업데이트: 이전에는 예제 코드에서 Option<ptr::NonNull<i32>>를 사용했습니다. 원시 포인터를 직접 사용하는 편이 코드를 더 따라가기 쉬운 것 같아 그렇게 바꾸었습니다. /업데이트
여기서 가장 흥미로운 코드는 원시 포인터 this.self_ref를 역참조하는 read_ref입니다. 이것이 합법적인 이유는 init()이 호출된 이후(포인터를 NULL이 아닌 값으로 설정할 수 있는 유일한 장소)로부터 지금까지 SelfReferential 전체가 이동하지 않았음을 신뢰할 수 있기 때문입니다.
특히, 시그니처를 fn init(&mut self)로 바꾸면 다음과 같은 코드로 쉽게 UB(정의되지 않은 동작)를 일으킬 수 있습니다:
fn main() {
// Box 안에 SelfReferential을 생성/초기화하고, 값을 이동시킨 다음 Box를 drop한다
let s = { let b1 = Box::new(SelfReferential::new()); b1.init(); *b1 };
let mut b2 = PinBox::new(s); // 초기화된 SelfReferential을 새 PinBox로 이동한다
println!("{:?}", b2.as_pin().read_ref()); // 폭발 발생
}
이제 read_ref()는 b1을 위해 할당되었지만 이후 해제된 메모리를 가리키는 포인터를 역참조하게 됩니다! 이는 명백히 잘못입니다.
이 예시는 또한 &mut T에서 Pin<T>로의 안전한 변환이 불가능함을 보여줍니다. 그런 변환이 가능하다면, init(self: Pin<Self>)를 호출하는 방식으로 문제가 있는 init_ref(&mut self)를 구현할 수 있게 됩니다. 반면 Box<T>를 PinBox<T>로 변환하는 것은 괜찮습니다. 왜냐하면 이것은 Box를 소비하므로, 그에 대한 “unpinned” 접근을 누군가가 다시 얻을 수 없기 때문입니다.
Pin은 SelfReferential을 안전하게 사용할 수 있도록 타입을 부여하게 해 줍니다. 이는 Rust의 전통과 잘 맞습니다. 표현력이 풍부한 타입 시스템을 사용하여, 다른 언어에서는 안전하지 않은 API로만 가능한 연산(예: Java 같은 메모리 안전 언어에서도 골칫거리인 이터레이터 무효화 없이 동작하는 이터레이터)을 안전한 API로 제공합니다. 다음에서는 우리가 주장하는 안전한 캡슐화가 실제로 성립함을 어떻게 증명할 수 있는지 설명합니다. 이는 RustBelt 논문에서 개발한 프레임워크 위에 구축되었습니다.
계속하기 전에, 소유권과 메모리 대여를 정확하게 이야기하기 위해 몇 가지 표기법을 소개하려 합니다. 이것을 전부 영어로만 표현하고 형식을 생략하는 것은 실제로 이해를 더 쉽게 만들지 않는다고 느낍니다. 논문에서 사용하는 완전한 형식은 과할 수 있으니, 여기서는 많은 세부를 생략한 단순화된 버전을 사용하겠습니다.
예를 들어, 위에서 말한 공리 (a)는 다음과 같이 쓸 수 있습니다:
forall |'a, ptr|
borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))
-> T.shr('a, ptr)
이는 우리가 자체 타입 T에 대해 T.own과 T.shr를 정의할 때마다 증명해야 하는 형식적 문장입니다. 모든 수명 'a와 포인터 ptr에 대해, borrowed('a, ...)가 성립한다면 T.shr('a, ptr)이 성립한다는 뜻입니다. 보통의 수학적 양화(quantifier)를 Rust스러운 문법(forall |var| ..., exists |var| ...)으로 쓰고, 함축에는 ->를 씁니다. 논리합(||)과 논리곱(&&)은 Rust를 따릅니다.
Rust 타입은 포인터와 그것이 가리키는 것에 관한 내용이 많으므로, 메모리에 대해 말할 수 있는 방법이 필요합니다. ptr.points_to_owned(bytes)(여기서 ptr: Pointer, bytes: List<Byte>)는 ptr이 주어진 bytes를 담고 있는 bytes.len() 바이트의 메모리를 가리키며, 게다가 그 메모리를 우리가 소유하고 있음을 의미합니다. 여기서 _소유_는 그 메모리를 읽고 쓰고 해제할 자유가 있고, 그러한 일을 할 수 있는 주체가 우리뿐임을 뜻합니다.
업데이트: 이전 버전에서는 이 술어를 mem_own이라고 불렀습니다. points_to_owned가 실제로 더 이해하기 쉬울 뿐 아니라, 문헌의 표준 용어와도 맞아 용어를 바꾸었습니다. /업데이트
마지막으로, borrowed('a, P)는 P가 수명 'a 동안만 일시적으로(즉, 빌려진 상태로) 소유됨을 말합니다. 여기서 P는 명제(proposition) 혹은 단언(assertion), 즉 우리가 무엇을 소유한다고 기대하는지에 관한 서술입니다. 위의 공리도 명제이고, ptr.points_to_owned([0, 0])도 명제입니다. 명제는 양화나 대여 같은 것을 사용하고, 메모리와 소유권에 대해 이야기할 수 있는 확장된 bool이라고 생각하시면 됩니다.
이 표기법으로 Box와 가변 참조의 소유 타입 상태를 어떻게 정의할 수 있는지 살펴봅시다:
정의 2:
Box<T>.own과(&'a mut T).own.Box<T>는 포인터를 구성하는 바이트 리스트이며, 그 포인터가 가리키는 메모리를 우리가 소유하고 그 메모리가T.own을 만족한다.&'a mut T도 거의 동일하지만, 메모리와T.own이 수명'a동안만 빌려진 상태라는 점이 다르다. 형식적으로:Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) && ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)(&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) && borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
:=는 “다음과 같이 정의된다”는 의미입니다. 이는 Rust에서 함수 정의와 매우 비슷하며, := 뒤의 부분이 함수 본문에 해당합니다. 바이트 시퀀스를 포인터라는 더 높은 수준의 표현으로 변환하기 위해 try_into를 사용하는 것에 주목하세요. 이는 List<Byte>에 대해 TryInto<U>가 구현되어 있어야 합니다. 변환은 특히 바이트 리스트가 정확히 올바른 길이가 아닐 때 실패합니다.
위와 같이 try_into를 사용하는 것은 사실 흔한 패턴입니다. 바이트에 대한 술어를 정의할 때, 종종 우리는 List<Byte>를 직접 다루기보다 그것을 먼저 더 높은 수준의 표현으로 변환하고 싶습니다. 이를 돕기 위해 보통 T.own(data: U)를 어떤 U에 대해 정의하는데, List<Byte>: TryInto<U>가 되도록 합니다. 즉 원시 바이트 리스트를 먼저 U로 변환하고, 술어는 U 안의 더 높은 수준의 데이터에 직접 접근합니다. 예를 들면 다음과 같습니다:
Box<T>.own(ptr: Pointer) :=
exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
(&'a mut T).own(ptr: Pointer) :=
borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
실제 소유권 술어는 다음과 같이 정의됩니다:
exists |data: U| bytes.try_into() == Ok(data) && T.own(data)
SelfReferential 검증을 위한 타입 확장예제로 돌아가서, SelfReferential이 임의의 안전한 코드에 의해 사용될 수 있음을 _증명_하려면 무엇이 필요할까요? 먼저 타입의 (모든 타입 상태에 대한) 개인 불변식을 적어야 합니다. self.read_ref가 NULL이 아니라면, 그것이 오프셋 0의 첫 필드 self.data의 주소임을 말하고 싶습니다. 하지만 글의 시작에서 제시한 Rust 타입 개념으로 돌아가 보면, T.own에서 “self.data의 주소”를 참조하는 것은 _불가능_합니다! 이는 놀랍지 않습니다. Rust에서 어떤 타입을 소유하고 있다면, 우리는 언제든지 그것을 다른 위치로 이동할 수 있으며, 따라서 불변식은 위치에 의존해서는 안 되기 때문입니다.
그래서 우리의 불변식을 적기 위해 타입 개념을 확장해야 합니다. 기존의 소유 및 공유 타입 상태 위에 새로운 세 번째 타입 상태를 추가하겠습니다:
정의 3a: pinning을 갖춘 Rust 타입. 정의 1을 다음의 새로운 타입 상태로 확장한다:
- 고정(pinned) 상태: 불변식
T.pin(ptr)(여기서ptr: Pointer)은ptr이 pinned로 간주되는T인스턴스를 가리키는 유효한 포인터인지를 말한다.
이 상태는 _바이트 시퀀스_에 대해 말하는 T.own과 달리, “_포인터_가 유효한가”를 이야기합니다. 이는 이동 불가능한 데이터에 대해 말하기 위해 필요한 표현력을 제공합니다. SelfReferential.pin(ptr)은 ptr이 우리가 소유한 메모리를 가리키고, 그 메모리가 어떤 쌍 (data, self_ref)를 저장하며, self_ref가 NULL이거나 오프셋 0의 첫 필드 data의 주소임을 말합니다:
SelfReferential.pin(ptr) := exists |data: i32, self_ref: *const i32|
ptr.points_to_owned((data, self_ref)) &&
(self_ref == ptr::null() || self_ref == ptr.offset(0))
(메모리 레이아웃 관점에서 SelfReferential은 i32와 *const i32의 쌍과 같습니다. 물론 여기서 많은 세부를 생략하고 있지만, 지금은 그 세부가 중요하지 않습니다. 또한 SelfReferential은 소유 및 공유 타입 상태도 가지지만, 거기서는 특별히 흥미로운 일이 일어나지 않습니다.)
이 선택으로 read_ref가 안전하게 실행됨을 정당화하기가 쉽습니다. 함수가 시작될 때 SelfReferential.pin(self)에 의존할 수 있습니다. else 분기에 들어가면, self_ref가 NULL이 아님을 알고, 따라서 그것은 반드시 ptr.offset(0)이어야 합니다. 결과적으로 self_ref의 역참조는 괜찮습니다.
계속하기 전에, 위에서 points_to_owned를 어떻게 사용했는지 설명해야 합니다. 이전에는 이 술어가 List<Byte>에서 동작한다고 했지만, 지금은 i32와 원시 포인터의 쌍에 대해 사용하고 있습니다. 다시 말해, 원시 바이트 리스트보다 더 높은 수준의 메모리 표현을 사용하는 또 하나의 예입니다. 예를 들어, ptr이 i32 타입의 42를 가리킨다고 말하고 싶다면 ptr.points_to_owned(42i32)라고 말할 수 있고, 그 값을 바이트 시퀀스로 바꾸는 방법에 대해 걱정할 필요가 없습니다. 사실 points_to_owned는 List<Byte>에서 동작하는 더 낮은 수준의 points_to_owned_bytes를 다음과 같이 정의함으로써 설명할 수 있습니다:
ptr.points_to_owned(data: U) where List<Bytes>: TryInto<U> :=
exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_owned_bytes(bytes)
앞서와 마찬가지로, 적절히 배치된 바이트 리스트를 U 타입으로 변환하기 위해 TryInto 트레이트를 (약간 남용해) 사용합니다.
pinned 타입 상태를 갖춘 타입 개념으로, 이제 Pin과 PinBox API를 정당화할 수 있습니다. 먼저 모든 타입에 대해 동작하는 메서드부터 시작하고, 이후에 Unpin이 필요한 추가 메서드를 논의하겠습니다. 그 과정에서 새로운 pinned 타입 상태를 기존 상태와 연결하기 위해 어떤 추가 공리가 필요한지 알아보게 됩니다. 여기서부터는 꽤 기술적으로 들어갑니다.
역시 타입을 검증하려면, 먼저 모든 타입 상태에 대한 그 불변식을 정의해야 합니다. 소유 타입 상태에 집중해 봅시다:
정의 4:
PinBox<T>.own과Pin<'a, T>.own. 바이트 리스트가 유효한PinBox<T>를 이루려면, 그 바이트가 포인터ptr를 구성하고 우리가T.pin(ptr)을 소유해야 한다.Pin<'a, T>의 경우에는,ptr이 수명'a동안T.pin(ptr)을 빌려온 상태이면 유효하다.PinBox<T>.own(ptr) := T.pin(ptr)Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))
impl<T> From<Box<T>> for PinBox<T>부터 시작합시다. 이는 Box<T>를 제자리에서 PinBox<T>로 바꿀 수 있습니다. 우리는 self가 Box<T>의 소유 타입 상태 불변식을 만족한다고 가정할 수 있고, 반환값(같은 포인터)이 PinBox<T>의 소유 타입 상태 불변식을 만족함을 증명해야 합니다. 이 변환을 정당화하려면, 완전히 소유된 T에 대한 포인터를 같은 위치의 pinned T로 바꾸어야 합니다. 이는 일반적으로 요구하기에 합리적인 원칙으로 보이므로, 이를 타입의 정의에 추가하겠습니다:
정의 3b: pinning을 갖춘 Rust 타입. 정의 3a에 다음 공리를 추가하여 확장한다:
- 만약 우리가
T.own(bytes)가 성립하는 바이트 리스트bytes를 가리키는 포인터ptr을 소유하고 있다면, pinned 타입 상태로 전환하여T.pin(ptr)을 얻을 수 있다. 형식적으로:``` forall |ptr, bytes| (ptr.points_to_owned(bytes) && T.own(bytes)) -> T.pin(ptr)
이제 PinBox::new는 Box::new와 PinBox<T>::from을 사용하여 쉽게 구현할 수 있습니다.
PinBox::as_pin의 경우, 우리는 시작점으로 &'a mut PinBox<T>(포인터에 대한 포인터)를 가지고, 내부 포인터를 Pin<'a, T>로 반환합니다. 이는 수명 'a 동안 어떤 bytes에 대한 포인터를 빌렸고, 그 bytes가 (해당 수명 동안) PinBox<T>.own(bytes)를 만족한다는 사실로 정당화됩니다:
borrowed('a, exists |bytes| ptr.points_to_owned(bytes) && PinBox<T>.own(bytes))
PinBox<T>.own을 전개하면, bytes가 실제로 포인터 inner_ptr을 구성하고, T.pin(inner_ptr)(해당 수명 동안)가 성립함을 도출할 수 있습니다. 이는 반환 타입과 정확히 일치하므로, 괜찮습니다!
마지막으로 impl<T> Deref for PinBox<T>를 보겠습니다. 여기서 PinBox의 공유 타입 상태가 중요해집니다. 이 impl은 &'a PinBox<T>를 한 번 역참조하여 &'a T로 바꿉니다. 이를 정당화하려면, T의 pinned 타입 상태에서 공유 타입 상태로 이동할 수 있어야 하며, 이를 위해 마지막 추가 공리를 요구합니다:
정의 3c: pinning을 갖춘 Rust 타입. 정의 3b에 다음 공리를 추가하여 확장한다:
- 만약 우리가 수명
'a동안T.pin(ptr)이 성립하는 포인터ptr을 빌렸다면, 공유 타입 상태로 전환하여T.shr('a, ptr)을 얻을 수 있다. (암묵적으로, 원래의 대여가 끝나면 타입은 소유 타입 상태로 되돌아간다.) 형식적으로:``` forall |'a, ptr| borrowed('a, T.pin(ptr)) -> T.shr('a, ptr)이것이 pinning을 갖춘 Rust 타입의 최종 정의이다.
이제 새로운 pinned 타입 상태를 소유 및 공유 타입 상태와 연결했으므로, 필요한 공리는 모두 갖춘 셈입니다.
다음으로, PinBox<T>의 공유 타입 상태를 정의합니다:
정의 5:
PinBox<T>.shr. 포인터ptr과 수명'a가PinBox<T>의 공유 타입 상태를 만족하려면,ptr이 다른 포인터inner_ptr에 대한 읽기 전용 포인터이고T.shr('a, inner_ptr)가 성립해야 한다. 다시 말해, 공유된PinBox<T>는 공유된T에 대한 읽기 전용 포인터일 뿐이다:PinBox<T>.shr('a, ptr) := exists |inner_ptr| ptr.points_to_read_only('a, inner_ptr) && T.shr('a, inner_ptr)이는 어떤 수명 동안 읽기 전용인 메모리를 이야기하는 방식을 필요로 한다. 우리는
ptr이bytes.len()바이트의 유효한 메모리를 가리키고 그 메모리가bytes를 담고 있으며, 수명'a동안 우리는 그 메모리를 읽을 수 있고 바뀌지 않는다는 것을 말하는 술어ptr.points_to_read_only_bytes('a: Lifetime, bytes: List<Byte>)가 있다고 가정한다. 그런 다음, 평소처럼 더 높은 수준의 메모리 표현에 기반한 편리한 변형을 정의한다:ptr.points_to_read_only('a: Lifetime, data: U) where List<Bytes>: TryInto<U> := exists |bytes| bytes.try_into() == Ok(data) && ptr.points_to_read_only_bytes('a, bytes)
소유와 공유 타입 상태를 연결하는 공리 (a)가 있음을 기억하세요. 우리는 이 공리가 PinBox에 대해서도 성립함을 확인해야 하며—그 증명은 방금 추가한 새로운 공리 (c)에 의존합니다. 이 PinBox<T>.shr 정의로 impl<T> Deref for PinBox<T>를 정당화하는 것은 비교적 간단합니다.
이로써 PinBox에서 사용 가능한 메서드를 마쳤습니다. Pin의 검증도 같은 접근을 따르므로 여기서는 자세히 서술하지 않겠습니다.
Unpin 마커 트레이트는 타입이 pinning에서 _옵트아웃_할 수 있게 해 줍니다. 타입이 Unpin이라면, 그 타입은 실제로 pinned 상태를 신경 쓰지 않으며, 따라서 &'a mut T와 Pin<'a, T>를 자유롭게 변환할 수 있습니다. 형식적으로 말하면:
정의 6:
Unpin. 타입T가Unpin이라는 것은,T.pin(ptr)로부터 우리가 포인터ptr을 소유하고 그것이 바이트 리스트bytes를 가리키며T.own(bytes)가 성립함을 도출할 수 있음을 의미한다. 형식적으로:forall |ptr| T.pin(ptr) -> (exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes))
이는 정의 2b에서 추가한 공리 (b)의 정확한 역방향임에 유의하세요. Unpin 타입의 경우, 소유와 pinned 타입 상태 사이를 자유롭게 오갈 수 있습니다.
명백히 SelfReferential은 Unpin이 아닙니다. 위의 예제 코드는 impl !Unpin으로 이를 명시합니다. 반면 i32 같은 타입의 경우, 그 pinned 타입 상태 불변식 i32.pin(ptr)은 ptr이 가리키는 메모리에만 관심이 있고 ptr의 실제 값에는 관심이 없으므로 Unpin 공리를 만족합니다.
이 정의를 바탕으로, T: Unpin을 가정하면 &'a mut T와 Pin<'a, T>는 동치 타입이며, Box<T>와 PinBox<T>도 마찬가지임이 분명합니다. 이는 Unpin 경계가 있는 모든 메서드를 정당화합니다.
이 제안의 장점 중 하나는 _로컬_이라는 점입니다. 기존 타입(및 새로운 타입)들이 Pin을 고려하지 않고 설계되었더라도, 이 새로운 타입 상태의 존재하에서 여전히 건전합니다. 이는 Unpin 트레이트를 자동 파생해도 마찬가지입니다. 이것이 가능한 이유는, 언제나 T.pin(ptr)을 다음과 같이 정의할 수 있기 때문입니다. 즉, 우리가 bytes를 가리키는 ptr을 완전히 소유하고, T.own(bytes)를 가진다고 말하는 것입니다:
T.pin(ptr) := exists |bytes| ptr.points_to_owned(bytes) && T.own(bytes)
이는 pinned 타입 상태를 다른 상태와 연결하는 추가 공리 (b)와 (c)를 만족하며, 동시에 Unpin도 만족합니다. 후자는 매우 중요합니다. 왜냐하면 자동 트레이트 메커니즘을 통해 Unpin 인스턴스를 자동으로 파생할 수 있고, 생태계 전체를 Pin 호환성 관점에서 다시 검토할 필요가 없기 때문입니다.
새로운 Pin 타입이 SelfReferential 같은 타입에 안전한 API를 부여하는 데 어떻게 사용될 수 있는지(이전에는 불가능했음), 그리고 SelfReferential과 Pin 및 PinBox의 메서드의 정확성을 (반)형식적으로 어떻게 논증할 수 있는지를 살펴보았습니다. pinning이 왜 유용한지, 그리고 일반적으로 타입드 API의 안전성을 어떻게 추론할 수 있는지에 대해 어느 정도 빛을 비추었기를 바랍니다. 다음에는 @cramertj가 제안한 pinning API 확장을 살펴보겠습니다. 이는 어떤 상황에서 drop이 호출될 것을 보장하며, 침습적 컬렉션(intrusive collections)에 어떻게 유용한지 논의하겠습니다.
읽어 주셔서 감사합니다! 여러분의 댓글을 기다립니다. 특히 타입 상태 불변식을 더 정밀하게 만들기 위해 사용한 가상의 문법이 도움이 되었는지 궁금합니다.