Effective Papers

This paper comes from my colleagues at AWS S3 Automated Reasoning Group, detailing their experience applying lightweight formal methods to a new class of storage node developed for S3 storage backend. Lightweight formal methods emphasize automation and usability. In this case, the approach involves three prongs: developing executable reference models as specifications, checking implementation conformance to those models, and building infrastructure to ensure the models remain accurate in the future. ShardStore ShardStore is a new append-only key-value storage node developed for AWS S3 backend. It is over 40K lines of Rust code. Shardstore is a log-structured merge tree (LSM tree) but with shard data stored outside the tree to reduce write amplification. ShardStore employs soft updates for avoiding the cost of redirecting writes through a write-ahead log while still being crash consistent. A soft updates implementation ensures that only writes whose dependencies are persisted are sent ...

This is a 2019 arxiv report . Back in 2019, when the report was out, I wrote a review about it, but did not publish it then because I felt I didn't have enough information on FoundationDB yet. With FoundationDB Sigmod 2021 paper out recently , I am now releasing that earlier write up. I will follow up on this soon with a review of the Sigmod21 paper on FoundationDB. Introduction FoundationDB made a bold design choice of ACID key-value store. They had released a transaction manifesto: Everyone needs transactions Transactions make concurrency simple Transactions enable abstraction Transactions enable efficient data representations Transactions enable flexibility Transactions are not as expensive as you think Transactions are the future of NoSQL FoundationDB, available as opensource , consists of the transactional minimalist storage engine as the base layer, and other layers are developed on top of the base layer to extend functionality. The record layer, that the report describes, is...

This paper from Facebook (Arxiv Feb 2021) is referred in the Google fail-silent Corruption Execution Errors (CEEs) paper as the most related work. Both papers discuss the same phenomenon, and say that we need to update our belief about quality-tested CPUs not having logic errors, and that if they had an error it would be a fail-stop or at least fail-noisy hardware errors triggering machine checks. This paper provides an account of how Facebook have observed CEEs over several years. After running a wide range of silent error test scenarios across 100K  machines, they found that 100s of CPUs are identified as having these errors, showing that CEEs are a systemic issue across generations. This paper, as the Google paper, does not name specific vendor or chipset types. Also the ~1/1000 ratio reported here matches the ~1/1000 mercurial core ratio that the Google paper reports. The paper claims that silent data corruptions can occur due to device characteristics and are repeatable at s...

This paper is from Google and appeared at HotOS 2021 . There is also a very nice 10 minute video presentation for it. So Google found fail-silent Corruption Execution Errors (CEEs) at CPU/cores. This is interesting because we thought tested CPUs do not have logic errors, and if they had an error it would be a fail-stop or at least fail-noisy hardware errors triggering machine checks. Previously we had known about fail-silent storage and network errors due to bit flips, but the CEEs are new because they are computation errors. While it is easy to detect data corruption due to bit flips, it is hard to detect CEEs because they are rare and require expensive methods to detect/correct in real-time.  What are the causes of CEEs? This is mostly due to ever-smaller feature sizes that push closer to the limits of CMOS scaling, coupled with ever-increasing complexity in architectural design. Together, these create new challenges for the verification methods that chip makers use to detect div...

This paper appeared recently in OSDI 2020 . This paper is about clock synchronization in the data center. I presented this paper for our distributed systems zoom meeting group . I took a wider view of the problem by explaining time synchronization challenges and fundamental techniques to achieve precise time synchronization. I will take the same path in this post as well. It is a bit circuitous road, but it gives a scenic pleasurable journey. So let's get going. The benefits of better time synchronization For any distributed system, timestamping and ordering of events is a very important thing. Processes in a distributed system run concurrently without knowing what the other processes are doing at the moment.  Processes learn about each other's states only by sending and receiving messages and this information by definition come from the past state of the nodes. The process needs to compose the coherent view of the system from these messages and all the while the system is movi...

This paper has been awarded a best paper award at OSDI20 , and is authored by Mahesh Balakrishnan, Jason Flinn, Chen Shen, Mihir Dharamshi, Ahmed Jafri, Xiao Shi, Santosh Ghosh, Hazem Hassan, Aaryaman Sagar, Rhed Shi, Jingming Liu, Filip Gruszczynski, Xianan Zhang, Huy Hoang, Ahmed Yossef, Francois Richard, and Yee Jiun Song at Facebook, Inc. Delos is the database that stores control plane state for Facebook, building over a shared log system. Each Delos server stores a local copy of a full database, which keeps materialized state of the log, as a Delos table. This DB/ is maintained over the shared log as RSM by just reading commands from the log in sequence and applying them for materializing on the table. Virtual consensus This high level setup is familiar, so let's dive deeper to get to the novelty in this work. Delos uses virtual consensus, which is a fancy way of saying the following. The DB is maintained over a virtual log, which consists of loglets, each of which is implemen...

This paper is authored by Ankush Desai, Amar Phanishayee, Shaz Qadeer, and Sanjit A. Seshia, and it appeared at OOPSLA 2018. The paper describes the ModP framework extension over the P language . P is a language developed for safe event-driven programming. P models processes as state machines: the state machines communicate via message passing, and events cause state machines to transition between states.  The killer feature of P is unifying modeling with programming! P enables the programmers to write specifications and enables systematic testing both via random testing and exhaustive symbolic execution testing. P is used in event driven systems such as device drivers and robotics . The P GitHub page  states that P is used in Microsoft (P# and Coyote ) and also used extensively at AWS for model-based testing of complex distributed systems.   Compositional testing of distributed systems A problem with systematic testing is that monolithic testing of large systems fa...

This paper is authored by Thomas  Kim, Daniel Lin Kit, Gregory Ganger, Michael  Kaminsky, and David Andersen. It appeared in SOCC 2020. The paper talks about using NVMM for building a distributed key value store. NVMMs are a new technology. They are slowly rolling into the datacenters, but there are still questions about their performance and how many writes it could handle before a write wear. NVMMs have very low latency comparable to DRAM, yet they are 10 times cheaper. Awesome, right? Unfortunately they don't have the same high bandwidth as DRAM or SSDs. Also, they are still not anywhere as cheap as SSDs, and it may not be affordable to want to build all NVMM key-value stores.  Before reading this paper, it is important to understand that this is all about money, money, money. The cost of NVMM and SSDs influences the design decisions, and lead to this non-straightforward heterogeneous design. If cost was not an issue, we could even have DRAMs for all replicas in K-V ...

This paper is by Shuai Mu, Lamont Nelson, Wyatt Lloyd, and Jinyang Li and it appeared in OSDI 2016. This paper presents Janus, another two-in-one shampoo & conditioner solution. Why deal with providing a solution for replication and another solution layered on top for transaction ordering when you can do both together in less time with a unified solution?  TAPIR had investigated this question first, and Janus does a followup. Instead of using the general transaction model considered in TAPIR, Janus uses one shot transactions, where each transaction contains multiple pieces and each piece has one read/write operation on a single key.  This reduced power transaction model allows Janus to implement an abort-free transaction ordering capability. A novel insight in Janus is that it notices it is possible to consolidate replication ordering and transaction ordering using the same setup. To order the transactions and replication alike, Janus takes a dependency graph tracking ap...