Valen 빌림 검사기, 함수를 거꾸로 훑어 메모리 안전성을 검사
- 역방향 안전성 검사는 함수의 마지막 문장부터 맨 위까지 거꾸로 걸어가며 참조가 이미 무효화되었는지 확인함
- Rust(NLL, Polonius), 기존 Vale, 이전 Valen 검사기는 모두 정방향 패스로 충돌을 검사함
- 거꾸로 가는 이유로 편의성, 루프 처리, 속도를 꼽음. 저자가 아는 한 안전성 검사를 거꾸로 하는 빌림 검사기는 이게 처음임
- Valen은 아직 실험 단계라 버그와 빈틈이 많고, v0.1은 2월쯤 나올 예정임
Hacker News opinions
저는 산에 종이랑 연필 들고 들어가서 머리 싸맸다는 얘기가 재밌더라. 처음엔 컴파일 타임 세대 참조 비슷한 걸로 시작해서 여러 번 바뀌다가 이 역방향 방식까지 간 거임.
엔지니어라면 기본기로 메커니즘부터 뜯어보는 거 맞지. Rust가 왜 lifetime으로 갔는지 궁금함. 이론 쪽에 치우친 건지, 단순화를 놓친 건지, 답 나오자마자 멈춘 건지 모르겠음.
글 끝에 손으로 쓴 글을 읽어달라는 문장 있던데 이거 칭찬하고 싶음. 사람이 서로에게 쓰는 글이 있어야 인터넷이 사람 사는 곳으로 남는다고 봄.
감사함. 나도 진심으로 그렇게 생각함. 쓰는 사람이 시간 들이면 읽는 사람도 그만큼 시간을 주는 거라서.
Rust 쓰는 입장에서 이런 시도가 잘 되길 바람. 도움은 못 줘도 응원은 함.
Hoare 계열 증명 쪽에선 목표 상태에서 거꾸로 거슬러 올라가는 게 흔한 방식임. 빌림 검사를 이렇게 보는 건 말이 됨. 다만 컴파일러 안에서 하면 증명할 항목마다 같은 코드를 여러 번 훑어서 느려짐. 컴파일 시간 얘기 나오면 다들 난리 남.
그럼 값 전체를 한 번에 정방향으로 다시 돌리는 식으로 최적화하면 안 되나?
검증을 더 많이 쓰자는 얘기는 결국 검증 자체를 더 빠르게 만들라는 말 아님? ;)