Assignment: Verdi

Due: Tue, 03 May 2016 09:00:00 -0700

Question

The papers discuss a verified implementation of a replicated key-value store. What is the TCB for this system as implemented in Verdi?

Question

What kinds of composition does Verdi enable (for instance, using VSTs)? What kinds of composition doesn’t it enable?

Question

The papers present examples of specifications both in terms event traces and in terms of the global state of the system. What’s the difference? Which do you prefer? When is one better than the other? Are there other kinds of specifications that could not be easily expressed as either state-based or trace-based?

Question

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.