FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu
(Database
group, Microsoft Research, Redmond, WA, USA)
Tahina Ramananandro
(RiSE: Research
in Software Engineering, MSR Redmond)
Aseem
Rastogi
(Microsoft
Research, Bengaluru, Karnataka, India)
Nikhil
Swamy (RiSE)
Aymeric Fromherz
(Prosecco, INRIA Paris, France)
Kesha Hietala
(Department of Computer Science,
University of Maryland, College Park, MD, USA)
Bryan Parno
(Computer Science Department, Carnegie Mellon University,
Pittsburgh, PA, USA; Electrical and Computer Engineering Department,
Carnegie Mellon University)
Ravi
Ramamurthy (Database group, MSR Redmond)
ACM/SIGPLAN CPP 2023 (accepted for publication, to appear)
FastVer is a protocol that uses a variety of memory-checking techniques to monitor the integrity of key-value stores with only a modest runtime cost. Arasu et al. formalize the high-level design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementation – FastVer is implemented in unverified C++ code.
In this work, we present FastVer2, a low-level, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to Arasu et al.'s high-level specification. Our proof is the first end-to-end system proven using Steel, and in doing so we contribute new ghost-state constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer.
We evaluate FastVer2 by comparing it against FastVer. Athough our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future.