Despite decades of research and practical experience, developers have few tools for programming reliable distributed applications without resorting to expensive coordination techniques. Conflict-free replicated datatypes (CRDTs) are a promising line of work that enable coordination-free replication and offer certain eventual consistency guarantees in a relatively simple object-oriented API. Yet CRDT guarantees extend only to data updates; observations of CRDT state are unconstrained and unsafe. We propose an agenda that embraces the simplicity of CRDTs, but provides richer, more uniform guarantees. We extend CRDTs with a query model that reasons about which queries are safe without coordination by applying monotonicity results from the CALM Theorem, and lay out a larger agenda for developing CRDT data stores that let developers safely and efficiently interact with replicated application state.

Conflict-free replicated data types (CRDTs) are a promising tool for designing scalable, coordination-free distributed systems. However, constructing correct CRDTs is difficult, posing a challenge for even seasoned developers. As a result, CRDT development is still largely the domain of academics, with new designs often awaiting peer review and a manual proof of correctness. In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Key to this process is a new formal definition of CRDT correctness that combines a reference sequential type with a lightweight ordering constraint that resolves conflicts between non-commutative operations. Our process follows the tradition of work in verified lifting, including an encoding of correctness into SMT logic using synthesized inductive invariants and hand-crafted grammars for the CRDT state and runtime. Katara is able to automatically synthesize CRDTs for a wide variety of scenarios, from reproducing classic CRDTs to synthesizing novel designs based on specifications in existing literature. Crucially, our synthesized CRDTs are fully, automatically verified, eliminating entire classes of common errors and reducing the process of producing a new CRDT from a painstaking paper proof of correctness to a lightweight specification.

Abstract: Analysis of Kepler mission data suggests that the Milky Way includes billions of Earth-sized planets in the habitable zone of their host stars. Current technology enables the detection of technosignatures emitted from a large fraction of the Galaxy. We describe a search for technosignatures that is sensitive to Arecibo-class transmitters located within ∼420 ly of Earth and transmitters that are 1000 times more effective than Arecibo within ∼13000 ly of Earth. Our observations focused on 14 planetary systems in the Kepler field and used the L-band receiver (1.15–1.73 GHz) of the 100 m diameter Green Bank Telescope. Each source was observed for a total integration time of 5 minutes. We obtained power spectra at a frequency resolution of 3 Hz and examined narrowband signals with Doppler drift rates between ±9 Hz s−1. We flagged any detection with a signal-to-noise ratio in excess of 10 as a candidate signal and identified approximately 850,000 candidates. Most (99%) of these candidate signals were automatically classified as human-generated radio-frequency interference (RFI). A large fraction (>99%) of the remaining candidate signals were also flagged as anthropogenic RFI because they have frequencies that overlap those used by global navigation satellite systems, satellite downlinks, or other interferers detected in heavily polluted regions of the spectrum. All 19 remaining candidate signals were scrutinized and none were attributable to an extraterrestrial source.