Peek and Poke with Dependent Types

• Thomas Hallgren
• ProgLog meeting talk 2006-12-13
  • (based on a Programatica meeting talk, January 2006)

House Today (1)

Uses GHC (the Glasgow Haskell Compiler)

• The compiler is big!
• The run-time system is big!
  • If we are implementing a micro-kernel in Haskell, this will be the biggest part.
• Can it be trusted?
• Can critical properties be verified formally?

House Today (2)

Does the Haskell type system give us what we need?

• The H(ardware) monad interface [1] relies on run-time checks for safety
  • Although safety isn't compromised, bugs can go undetected until run-time.
  • For some things, silent truncation is used, so bugs will result in misbehavior rather than error messages.
• We don't know how to deal safely with DMA.

At the Machine Level...

Primitives for memory access

• type Addr = Word32 peek ∈ Addr → H Word8 poke ∈ Addr → Word8 → H ()
• Correspond to instructions directly supported by the CPU.
• Unsafe! Allows any memory location to be overwritten.
  • With unrestricted use, no interesting run-time invariants can be guaranteed.

Safety Through Abstraction

• Safety = maintaining invariants...
• Invariants can only guaranteed for programs written above certain abstraction levels.
• Most code should be written on top of the safe abstractions, obviously!

Hardware Monad Examples

• Safety by abstract data types + silent truncation:
  type PAddr = (PhysPage,POffset) type PhysPage -- abstract type POffset = Word12 getPAddr ∈ PAddr → H Word8 setPAddr ∈ PAddr → Word8 → H () allocPhysPage ∈ H (Maybe PhysPage)
• Safety by abstract data types + run-time bounds checks:
  data MemRegion -- abstract type Offset = Word32 pokeByteOff ∈ Storable a ⇒ MemRegion → Offset → a → H () peekByteOff ∈ Storable a ⇒ MemRegion → Offset → H a

Another Experiment: An Alfa version of House?

• (1) Start with a minimal compiler and run-time system
  • There is hope that critical properties can be verified formally
  • Grow it without sacrificing formal verification
• (2) Make use of dependent types
  • More safety constraints can be captured as type-safety
    • Fewer bugs!
  • More safety checks can be moved from run-time to compile-time
    • Potential for better performance!

A Minimal Compiler and Run-Time System

• Compiler:
  • Front-end: Alfa (programming environment, type checking)
  • Back-end: ~750 lines of Haskell code (excluding standard libraries)
    • Input: a useful subset of the language Alfa supports
    • Output: a small subset of C
• Run-time system size: ~630 lines of C
  • Including a simple copying garbage collector: ~120 lines of C
  • Compile-time configurable for hosted and bare-metal use

Compiler and run-time system

Based on the <ν,G> machine [2]

• Designed to support parallel execution on a multi-processor machine
  • Easy to support low-latency interrupt handling
• Very simple memory management
  • No stack, everything is in the heap
  • Root set for GC: just one pointer (ν, the current redex)

An example

Hello world!

• A bootable executable that displays a message on the screen of a PC.
• Requires writing to the text screen buffer located at a particular absolute address in the PC physical memory layout.

Peek and Poke again

Primitives for memory access

• type Addr = Word32 peek16 ∈ Addr → H Word16 poke16 ∈ Addr → Word16 → H ()
• Unsafe! Allows any memory location to be overwritten.
  • With unrestricted use, no interesting run-time invariants can be guaranteed.

Abstraction for limited memory access

• A Safe Interface:
  Readable ∈ Addr → Prop Writable ∈ Addr → Prop peek16 ∈ (a∈Addr) → Readable a → H Word16 poke16 ∈ (a∈Addr) → Writable a → Word16 → H ()
• Primitives to declare what constitutes safe memory access:
  Unsafe.readable ∈ (a∈Addr) → Readable a Unsafe.writable ∈ (a∈Addr) → Writable a
• Dependent types! Propositions as Types!
  Let's us talk about values (memory addresses) at the type level.

Text screen buffer access (1)

• Limit access to the text screen buffer
  data Range = Range { lo,hi∈Addr } screen ∈ Range screen = Range 0xb8000 0xb8fff InRange ∈ Range → Addr → Prop screenPoke ∈ (a∈Addr) → InRange screen a → Word16 → H ()
• Implementation of screenPoke
  writableScreen ∈ (a∈Addr) → InRange screen a → Writable a writableScreen a r = Unsafe.writable a screenPoke ∈ (a∈Addr)→ InRange screen a → Word16 → H () screenPoke a r d = poke16 a (writableScreen a r) d

Text screen buffer access (2)

Using Predicate Based Subtyping

• Let Σ T P denote the subset of type T that satisfies P
  • values are pairs: (value x∈T,proof of P x)
• We can now define
  type ScreenAddr = Σ Addr (InRange screen) screenPoke ∈ ScreenAddr → Word16 → H ()

Abstraction for displaying text

• Putting characters with attributes at specific screen locations
  • type Attr = ... xRange = Range 0 79 yRange = Range 0 24 type Column = Σ Word32 (InRange xRange) type Row = Σ Word32 (InRange yRange) putac ∈ Column → Row → Attr → Char → H ()
• Outputting text (scrolling if necessary)
  • putString ∈ String → H ()
• The code that needs to deal with the extra safety constraints is small and localized!

Alfa proofs (or lack thereof)

• Computing the memory address for given screen coordinates:
  charAddr ∈ Column → Row → ScreenAddr charAddr (x,xr) (y,yr) = (lo screen + 2*(80*x+y),?)
• A lemma for charAddr:
  All x,y . InRange xRange x ⇒ InRange yRange y ⇒ InRange screen (lo screen + 2*(80*x+y))
• Decidable, should prove itself:
  • Formulate it as an expression of type Bool. The proof that a boolean is True is trivial.
  • But the interpreter in Agda seems to be too inefficient to handle this...
  • Others have worked on this problem [3].

Example of extended static checking

Displaying strings that fit on the screen

• Fits ∈ Word32 → String → Prop puts ∈ (x,y∈Word32) → (s∈String) → Fits x s → InRange yRange y → H ()
• Useful for the correctness of the "Hello world" program :-)

Hello world!

• main = puts 35 12 "Hello, world!" () ()
• Statically checked that:
  • No poking outside the text screen buffer.
  • The message fits on the screen (and does not wrap to the next line).

Problems

• Modulo arithmetic
  • Simple inequalities don't hold!
    • i < base+size ⇔ i-base < size ?
    • base ≤ i ⇒ base ≤ i+1 ?
• Termination checking
  • Used forms of recursion not recognized by the termination checker.

Future work?

• Do more of the current H monad interface.
• Make more complex memory access patterns safe:
  • Manipulating linked data structures.
  • Safe DMA programming.
• A dependently typed H monad (sketchy)?
  • type H M_pre M_post a peek ∈ (a∈Addr) → H M M (M a) poke ∈ (a∈Addr) → T → H M M[a→T] ()
• Separation Logic in the types? [4]
• Verifying the compiler and run-time system properties. (Use ideas from [5]?)

The End

Any more questions?

References

• [1] By us: A Principled Approach to Operating System Construction in Haskell, ICFP 2005.
• [2] Lennart Augustsson and Thomas Johnsson: Parallel Graph Reduction with the <ν,G> machine, FPCA 1989.
• [3] Benjamin Gregoire and Xavier Leroy, A compiled implementation of strong reduction, ICFP 2002.
• [4] John C. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002.

References

[5] Xavier Leroy: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL 2006.