Making safe OS kernel extensions expressive, efficient, and easy to program