-
Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version)
Authors:
Upamanyu Sharma,
Ralf Jung,
Joseph Tassarotti,
M. Frans Kaashoek,
Nickolai Zeldovich
Abstract:
Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks. This paper uses Grove to verify several distributed system components written in Go, including GroveKV, a realistic distributed multi-threaded key-value…
▽ More
Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks. This paper uses Grove to verify several distributed system components written in Go, including GroveKV, a realistic distributed multi-threaded key-value store. GroveKV supports reconfiguration, primary/backup replication, and crash recovery, and uses leases to execute read-only requests on any replica. GroveKV achieves high performance (67-73% of Redis on a single core), scales with more cores and more backup replicas (achieving about 2x the throughput when going from 1 to 3 servers), and can safely execute reads while reconfiguring.
△ Less
Submitted 14 September, 2023; v1 submitted 6 September, 2023;
originally announced September 2023.
-
Unnatural Language Processing: Bridging the Gap Between Synthetic and Natural Language Data
Authors:
Alana Marzoev,
Samuel Madden,
M. Frans Kaashoek,
Michael Cafarella,
Jacob Andreas
Abstract:
Large, human-annotated datasets are central to the development of natural language processing models. Collecting these datasets can be the most challenging part of the development process. We address this problem by introducing a general purpose technique for ``simulation-to-real'' transfer in language understanding problems with a delimited set of target behaviors, making it possible to develop m…
▽ More
Large, human-annotated datasets are central to the development of natural language processing models. Collecting these datasets can be the most challenging part of the development process. We address this problem by introducing a general purpose technique for ``simulation-to-real'' transfer in language understanding problems with a delimited set of target behaviors, making it possible to develop models that can interpret natural utterances without natural training data. We begin with a synthetic data generation procedure, and train a model that can accurately interpret utterances produced by the data generator. To generalize to natural utterances, we automatically find projections of natural language utterances onto the support of the synthetic language, using learned sentence embeddings to define a distance metric. With only synthetic training data, our approach matches or outperforms state-of-the-art models trained on natural language data in several domains. These results suggest that simulation-to-real transfer is a practical framework for develo** NLP applications, and that improved models for transfer might provide wide-ranging improvements in downstream tasks.
△ Less
Submitted 28 April, 2020;
originally announced April 2020.
-
A Revised and Verified Proof of the Scalable Commutativity Rule
Authors:
Lillian Tsai,
Eddie Kohler,
M. Frans Kaashoek,
Nickolai Zeldovich
Abstract:
This paper explains a flaw in the published proof of the Scalable Commutativity Rule (SCR), presents a revised and formally verified proof of the SCR in the Coq proof assistant, and discusses the insights and open questions raised from our experience proving the SCR.
This paper explains a flaw in the published proof of the Scalable Commutativity Rule (SCR), presents a revised and formally verified proof of the SCR in the Coq proof assistant, and discusses the insights and open questions raised from our experience proving the SCR.
△ Less
Submitted 23 September, 2018;
originally announced September 2018.
