Due: Wed, 11 May 2016 23:00:00 -0700
To help you understand FSCQ’s Crash Hoare logic, we have provided two simplified implementations:
Read and compare the files. Run through the proofs in Coq and complete the “Admitted” ones (no need to turn in your proofs).
How would you extend the simplified implementation of Crash Hoare logic to model asynchronous disks? How about recovery?
You may consult Prog.v in FSCQ’s implementation.
Describe three ways to improve FSCQ’s performance and discuss possible difficulties in verification.
Provide a list of questions you would like to discuss in class.
Submit a plain text file answers.txt
with your answers to the questions.
Extend FSCQ for fun. For example, you may choose to implement larger files or improve its performance.