UARTドライバを書いてみましょう
QEMUの’virt’ マシンにはPL011というUARTがあるので、それに対するドライバを書いてみましょう。
Speaker Notes
Uart::new
がアンセーフでその他のメソッドがセーフであるということに注目してください。これは、Uart::new
の安全性要求が満たされている(すなわち特定のUARTに対して一つしかドライバのインスタンスが存在せず、そのアドレス空間に対してエイリアスが全く存在しない)ことをその呼び出し元が保証する限り、それ以降は必要な事前条件が満たされていると想定することができwrite_byte
を常に安全に呼び出すことができるようになることが理由です。- 逆に(
new
をセーフにして、write_byte
をアンセーフに)することもできましたが、そうするとwrite_byte
の全呼び出し箇所において安全性を考慮しなければならなくなり、利便性が低下します - これはアンセーフなコードに対してセーフなラッパーを構築する場合の共通パターンです:健全性に関する証明に関する労力を多数の場所から少数の場所に集約します。