CPSC 508 Winter 1 2019: Quiz #3

Please use whatever word processing software that you'd like to write your answers, but please send me either plain text (≤ 80 characters per line) or PDF. I will be grading the quiz blind (that is, I don't want to know whose quiz I am grading), so please do not put your name anywhere in the document you submit. Instead, call the file you send me lastname.{txt,pdf} (where you fill in lastname with your own last name). Please email your quiz to: mseltzer@cs.ubc.ca. (I convert the files to randomly numbered files, grade them, and then convert the names back.)

Here are the papers we've read (alphabetical by author):

1. Anderson: Serverless Network File Systems
2. Chen: Using Crash Hoare Logic for Certifying the FSCQ File System
3. Gu: CertiKOS:An extensible Architecture for Building Certified Concurrent OS Kernels
4. Hagmann: Reimplementing the Cedar File System Using Logging and Group Commit
5. Howard: Scale and Performance in a Distributed File System
6. Jorgensen: The eXpress Data Path: Fast Programmable Packet Processing in the Operating System Kernel
7. Klein: seL4: Formal Verification of an OS Kernel Using Crash Hoare Logic
8. Mickens: Blizzard: Fast, Cloud-scale Block Storage for Cloud-oblivious Applications
9. Nelson: Hyperkernel: Push-Button Verification of an OS Kernel
10. Pu: The Synthesis Kernel
11. Rinard: Enhancing Server Availability and Security Through Failure-Oblivious Computing
12. Rosenblum: The Design and Implementation of a Log-Structured File System
13. Sandberg: Design and Implementation of the Sun Network Filesystem
14. Schroeder: Experience with Grapevine: The Growth of a Distributed System

Best of Both Worlds

This question was so much fun last time let's do it again! We've read several papers that can be categorized as providing the best of two worlds, e.g., the great taste of the very best ice cream with the calories of a carrot. For each paper below, identify the two things that are being achieved.

1. Pu: The Synthesis Kernel
2. Mickens: Blizzard: Fast, Cloud-scale Block Storage for Cloud-oblivious Applications
3. Rinard: Enhancing Server Availability and Security Through Failure-Oblivious Computing

OS Verification

We read a lovely collection of verification papers, each of which used slightly different verification approaches. For each paper listed below, describe in 2-3 sentences their overall approach to verification and what tools they used.

1. Chen: Using Crash Hoare Logic for Certifying the FSCQ File System
2. Gu: CertiKOS:An extensible Architecture for Building Certified Concurrent OS Kernels
3. Klein: seL4: Formal Verification of an OS Kernel Using Crash Hoare Logic
4. Nelson: Hyperkernel: Push-Button Verification of an OS Kernel

File Systems

You have just begun a Ph.D. program and your advisor suggests that a great thesis would be a wwwFs - the world wide web file system. The basic idea is that you could type cd www.seltzer.com/margo/teaching/CPSC508.19/papers; ls and you would see my complete collection of papers.

Either A) explain why you immediately decide to change advisor (give technical reasons why this is not a dissertation worthy project), or B) discuss what techniques you would borrow from any of the papers we've read and justify the techniques you choose.

Paper Survey