CS 260r 2017 L13: IronFleet (3/8)
Email address *
Question 1 *
The Verdi key-value store specification uses per-key traces (page 364 of Verdi), whereas the IronKV key-value store specification uses a transition relation on an abstract hash-table state (Figure 11 on page 10 of IronFleet). Contrast these approaches.
Your answer
Question 2 (optional but recommended)
The Verdi key-value store implementation at https://github.com/uwplse/verdi/blob/master/systems/VarD.v#L110 supports five operations, get, put, delete, compare-and-swap, and compare-and-delete. Now consider the “high-level spec for IronKV” in Figure 11. Write a new version of this spec that supports at least one additional operation from VarD. (NB: In Dafny, the “::” operator means “such that,” not “cons.”)
Your answer
Never submit passwords through Google Forms.
This form was created inside of Google Apps for Harvard. Report Abuse - Terms of Service - Additional Terms