- B. N. Bershad et al., “Extensibility, safety and performance in the SPIN operating system,” Proceedings of the 15th ACM Symposium on Operating Systems Principles, SOSP 1995, pp. 267–284, 1995, doi: 10.1145/224056.224077.
개요
Problems and importance
기존 시스템에서 운영체제의 구현과 어플리케이션이 요구하는 것은 다를 수 있다. 예를 들어서 데이터 베이스 시스템은 스스로의 파일 시스템을 작성하고 싶을 수도 있을 것이다 (만일 SPDK가 없다면!). 운영체제는 이러한 Generality와 Performance사이의 균형을 잘 맞춰야 하는데 이러한 문제는 쉽게 해결될 수 없다. 따라서 Language based safty 모델을 사용함으로써, Kernel extension들을 안전하게 사용할 수 있도록 함으로써, 이러한 문제를 극복할 수 있다.
Main Idea and contribution
Modular-3라는 Type safety 언어의 강력한 컴파일 타임 verification에 의존하여서, 마치 Rust처럼 반드시 커널이 제공하는 인터페이스를 통해서만 포인터와 같은 문법적 요소들을 다루도록 하여서 Kernel extension의 안전성을 담보하였다. 이를 통해서 효율적이고, fine-grained한 리소스의 접근을 가능하게 하여 어플리케이션이 커널의 자원을 효과적으로 사용할 수 있도록 하였다.
- Fine-grained Access to system services
- Kernel and extension is co-located for performance
- Logical protectino domain provides resource managements
- Languaged based protection provdies simple and fast protection model
Design
Type safe language를 통해서 다음과 같은 Portection model을 달성하였다.
- Capabilities
- 모든 커널의 리소스들을 사용하기 위해서는 Capabilities를 가지고 있어야 한다. 예를 들어서 포인터와 같은 경우 포인터에 해당하는 Type그리고 Range에 대해서만 Modular-3에 의해서 접근 가능하도록 하였다. 즉 어떠한 오브젝트에 대한 권한이 있어야지만 그 오브젝트가 허용하는 범위 안에서 오브젝트를 사용할 수 있도록 한 것이다.
Implementation
Criticizing
- 우선 Fixed 된 언어로 인하여, 반드시 Modular 3를 사용해야 하는 것은 Friendly측면에서 Critical 한 단점이 된다.
- Array bound checking 과 같은 Dynamic checking으로 인하여 Performance overhead가 있다.
SPIN은 Kernel extension에서 대단히 선구적인 모델로, 거의 큰 틀을 잡은 매우 역사적인 논문이다.