UARTドライバを書いてみましょう

QEMUの’virt’ マシンにはPL011というUARTがあるので、それに対するドライバを書いてみましょう。

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Speaker Notes

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