Lecture preparation
Before lecture, read the paper assigned below, and submit two items
to the
submission website:
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
beforehand.
- Submit your answer for the question below, before the beginning of the lecture.
Also keep in mind that you will need to write a
paper summary for your choice of papers
throughout the semester.
Assignment
Read the paper
SibylFS: formal specification and oracle-based testing
for POSIX and real-world file systems
by Ridge et al.
Why are we reading this paper?
-
Focus on specifications, a different and fruitful application of formal
methods if not systems verification.
-
Scaling up these techniques to a real system, not designed for the
purposes of the authors.
What to learn from this paper?
-
What is this paper setting out to do and why is that useful?
-
Contrast this approach with testing.
-
Why is it hard to specify real systems?
Answer this question
A challenge for the SibylFS authors is that there exists no reference
implementation of POSIX, but there are many file systems that implement
something that is close to POSIX. To allow for different implementations,
the SibylFS's specification is non-deterministic in several areas.
Give an example of such a non-determinism in the SibylFS specification and
explain what degrees of freedom it provides to file-system implementors.
