Using UDFs: ad hoc induction

• When meta allocated, check that:

  • owns(meta) = {}

• To give meta control of block `b’

• Result: kernel can trust metadata without understanding it or owns!

old_set = owns(meta)
<let libFS scribble on meta>
if owns(meta) != old_set U {b} then
error “bogus modification!”

Previous slide

Next slide

Back to first slide

View graphic version