Given a set S subset of U and a function f: S -> {0, 1} (R), a static retrieval data structure for f supports queries that return f (x) for x E S and an arbitrary value from {0, 1} r for x E U \ S. Retrieval data structures can be used to implement a static approximate membership query (AMQ) data structure, i.e., a Bloom filter alternative, with false positive rate 2(-r) . The information-theoretic space lower bound for both tasks is rSbits, and here we aim to use space r S (1 + P) bits for a small overhead P, including succinct constructions with P = o (1). A well-known approach to this task associates each key x E S with a row vector h (R)(x) is an element of {0, 1}m and stores a matrix Z is an element of {0, 1}(mxr) such that h (R)(x) & centerdot; Z = f (x) for every x E S. We propose a new variant where h (R)(x) contains a short block of random bits at a random position s (x), and is otherwise zero. Sorting the row vectors by s(x) gives a matrix A is an element of {0, 1}(n & times;m) with non-zero entries concentrated in a "ribbon" along a generalized diagonal. This makes a variant of Gaussian elimination particularly efficient at computing Z. We thus obtain simple data structures called Standard Ribbon Retrieval and Homogeneous Ribbon Filter. We then refine the construction using bumping (a variant of backyarding) and overloading (using m < n) to obtain bumped ribbon retrieval ("BuRR"), with overhead O( logw/rw(2)),query time O(1 + rw/log n), and expected construction time O(nw), for a tuning parameter w = O (log n) that opens a trade-off between space and running time. Our experiments reveal our implementations to be the first to simultaneously achieve small overheads and fast running times in practice, with BuRR achieving overheads well below 1 % while being faster than most competitors, which have larger space overheads. This efficiency, including favorable constants, stems from a combination of simplicity, word parallelism, and high locality. We offer a unified theoretical perspective on these three ribbon-based data structures, including a nontrivial rigorous analysis of their running times and memory consumption.

Approximate membership filters are increasingly used in many computing and networking applications and new filter designs are being continuously presented to improve one or more performance metrics. Therefore, understanding their security and privacy is an important issue. Previous works have considered attackers that only have access to an individual filter in isolation. For applications that generate many related filters, such as a filter for a deny list that evolves over time, that analysis is insufficient. This paper considers an attacker with access to several versions of a filter that share most of the same input elements. We find that for typical implementations of Bloom, cuckoo, and quotient filters, the attacker gains little or no advantage with access to multiple versions of a filter. However, typical xor filters do reveal more information about their input elements by querying multiple versions of a filter, and we propose techniques to enhance the privacy of xor filters and others.

In the Uncoordinated Unique Identifiers Problem (UUIDP) there are n independent instances of an algorithm A that generates IDs from a universe (1, ..., m) , and there is an adversary that requests IDs from these instances. The goal is to design A such that it minimizes the probability that the same ID is ever generated twice across all instances, that is, minimizes the collision probability. Crucially, no communication between the instances of A is possible. Solutions to the UUIDP are often used as mechanisms for surrogate key generation in distributed databases and key-value stores. In spite of its practical relevance, we know of no prior theoretical work on the UUIDP. In this paper we initiate the systematic study of the UUIDP. We analyze both existing and novel algorithms for this problem, and evaluate their collision probability using worst-case analysis and competitive analysis, against oblivious and adaptive adversaries. In particular, we present an algorithm that is optimal in the worst case against oblivious adversaries, an algorithm that is at most a logarithmic factor away from optimal in the worst case against adaptive adversaries, and an algorithm that is optimal in the competitive sense against both oblivious and adaptive adversaries.

Filter data structures over-approximate a set of hashable keys, i.e. set membership queries may incorrectly come out positive. A filter with false positive rate $f \in (0,1]$ is known to require $\ge \log_2(1/f)$ bits per key. At least for larger $f \ge 2^{-4}$, existing practical filters require a space overhead of at least 20% with respect to this information-theoretic bound. We introduce the Ribbon filter: a new filter for static sets with a broad range of configurable space overheads and false positive rates with competitive speed over that range, especially for larger $f \ge 2^{-7}$. In many cases, Ribbon is faster than existing filters for the same space overhead, or can achieve space overhead below 10% with some additional CPU time. An experimental Ribbon design with load balancing can even achieve space overheads below 1%. A Ribbon filter resembles an Xor filter modified to maximize locality and is constructed by solving a band-like linear system over Boolean variables. In previous work, Dietzfelbinger and Walzer describe this linear system and an efficient Gaussian solver. We present and analyze a faster, more adaptable solving process we call "Rapid Incremental Boolean Banding ON the fly," which resembles hash table construction. We also present and analyze an attractive Ribbon variant based on making the linear system homogeneous, and describe several more practical enhancements.

A retrieval data structure for a static function $f:S\rightarrow \{0,1\}^r$ supports queries that return $f(x)$ for any $x \in S$. Retrieval data structures can be used to implement a static approximate membership query data structure (AMQ), i.e., a Bloom filter alternative, with false positive rate $2^{-r}$. The information-theoretic lower bound for both tasks is $r|S|$ bits. While succinct theoretical constructions using $(1+o(1))r|S|$ bits were known, these could not achieve very small overheads in practice because they have an unfavorable space--time tradeoff hidden in the asymptotic costs or because small overheads would only be reached for physically impossible input sizes. With bumped ribbon retrieval (BuRR), we present the first practical succinct retrieval data structure. In an extensive experimental evaluation BuRR achieves space overheads well below 1\,\% while being faster than most previously used retrieval data structures (typically with space overheads at least an order of magnitude larger) and faster than classical Bloom filters (with space overhead $\geq 44\,\%$). This efficiency, including favorable constants, stems from a combination of simplicity, word parallelism, and high locality. We additionally describe homogeneous ribbon filter AMQs, which are even simpler and faster at the price of slightly larger space overhead.

In the last decade, significant efforts have been made to reduce the false positive rate of approximate membership checking structures. This has led to the development of new structures such as cuckoo filters and xor filters. Adaptive filters that can react to false positives as they occur to avoid them for future queries to the same elements have also been recently developed. In this paper, we propose a new type of static filters that completely avoid false positives for a given set of negative elements and show how they can be efficiently implemented using xor probing filters. Several constructions of these filters with a false positive free set are proposed that minimize the memory and speed overheads introduced by avoiding false positives. The proposed filters have been extensively evaluated to validate their functionality and show that in many cases both the memory and speed overheads are negligible. We also discuss several use cases to illustrate the potential benefits of the proposed filters in practical applications.

We present a data definition framework that enables the convenient specification of data types in ACL2s, the ACL2 Sedan. Our primary motivation for developing the data definition framework was pedagogical. We were teaching undergraduate students how to reason about programs using ACL2s and wanted to provide them with an effective method for defining, testing, and reasoning about data types in the context of an untyped theorem prover. Our framework is now routinely used not only for pedagogical purposes, but also by advanced users. Our framework concisely supports common data definition patterns, e.g., list types, map types, and record types. It also provides support for polymorphic functions. A distinguishing feature of our approach is that we maintain both a predicative and an enumerative characterization of data definitions. In this paper we present our data definition framework via a sequence of examples. We give a complete characterization in terms of tau rules of the inclusion/exclusion relations a data definition induces, under suitable restrictions. The data definition framework is a key component of counterexample generation support in ACL2s, but can be independently used in ACL2, and is available as a community book.

Using an interactive theorem prover to reason about programs involves a sequence of interactions where the user challenges the theorem prover with conjectures. Invariably, many of the conjectures posed are in fact false, and users often spend considerable effort examining the theorem prover's output before realizing this. We present a synergistic integration of testing with theorem proving, implemented in the ACL2 Sedan (ACL2s), for automatically generating concrete counterexamples. Our method uses the full power of the theorem prover and associated libraries to simplify conjectures; this simplification can transform conjectures for which finding counterexamples is hard into conjectures where finding counterexamples is trivial. In fact, our approach even leads to better theorem proving, e.g. if testing shows that a generalization step leads to a false conjecture, we force the theorem prover to backtrack, allowing it to pursue more fruitful options that may yield a proof. The focus of the paper is on the engineering of a synergistic integration of testing with interactive theorem proving; this includes extending ACL2 with new functionality that we expect to be of general interest. We also discuss our experience in using ACL2s to teach freshman students how to reason about their programs.

Efficiently storing and matching visited states is key to the effectiveness of explicit-state model checkers such as SPIN. Models of concurrent programs often have too many reachable states to enumerate easily in main memory, and an efficient model checker can exhaust main memory in minutes by storing state descriptors exactly. A popular alternative is to over-approximate the set of visited states using a randomized, probabilistic data structure, such as a Bloom filter. Because the approximation is sound and does not slow down the search with revisitation of states, it tends to find errors quickly. Because it is probabilistically complete, the approach can also convincingly demonstrate lack of errors.In this dissertation, I analyze the approximate state storage problem in unprecedented detail, improve upon standard solutions, and demonstrate a novel approach that solves a configuration dilemma facing users of the standard solutions. Especially with my improvements, the best Bloom filter or hash compaction configuration for a given situation is quite good, but choosing the best configuration depends on a good estimate of the number of reachable states. Such an estimate is usually only available after checking a model. I solve this dilemma with an efficient storage scheme that is not tied to a particular estimate, because it is adaptive. Regardless of the number of states encountered at run time, its accuracy is near the information-theoretic optimal. It is also competitively fast, thanks to a novel in-place adaptation algorithm and a favorable access pattern to memory.

Existing techniques for approximate storage of visited states in a model checker are too special-purpose and too DRAM-intensive. Bitstate hashing, based on Bloom filters, is good for exploring most of very large state spaces, and hash compaction is good for high-assurance verification of more tractable problems. We describe a scheme that is good at both, because it adapts at run time to the number of states visited. It does this within a fixed memory space and with remarkable speed and accuracy. In many cases, it is faster than existing techniques, because it only ever requires one random access to main memory per operation; existing techniques require several to have good accuracy. Adapting to accommodate more states happens in place using streaming access to memory; traditional rehashing would require extra space, random memory accesses, and hash computation. The structure can also incorporate search stack matching for partial-order reductions, saving the need for extra resources dedicated to an additional structure. Our scheme is wellsuited for a future in which random accesses to memory are more of a limiting factor than the size of memory.

ACL2 is the latest inception of the Boyer-Moore theorem prover, the 2005 recipient of the ACM software system award. In the hands of an expert, it feels like a finely tuned race car, and it has been used to prove some of the most complex theorems ever proved about commercially designed systems. Unfortunately, ACL2 has a steep learning curve, and novices tend have a very different experience: they crash and burn. As part of a project to make ACL2 and formal reasoning accessible to the masses, we have developed ACL2s, the ACL2 sedan. ACL2s streamlines the learning process with features not previously available for ACL2. Our goal is to develop a tool that is " self-teaching," i.e., it should be possible for an undergraduate to sit down and play with it and learn how to program in ACL2 and how to reason about the programs she writes. The latest version of ACL2s is a significant step in that direction.

The ACL2 theorem prover provides the user a wide range of mechanisms for customization and extension while preserving soundness. ACL2 researchers and power users, however, sometimes work outside this realm in order to add new core functionality, to attach new user interfaces, or to connect ACL2 with other reasoning engines. We first describe new features of ACL2 that enable users to add to the set of “trusted code” in a trackable way. The advantage is that users can dynamically install system extensions they choose to trust in reaching their verification results, and ACL2 will track what was trusted in the process. We then describe features, idioms, and abstractions that leverage the freedoms given to trusted code and the dynamic, reflective nature of Common Lisp to modify ACL2 in deep ways at runtime. Our abstractions are designed to make it easier for system hackers to preserve sound reasoning when writing metatheoretic code.

3Spin and 3Murphi are modified versions of the Spin model checker and the Murϕ verifier. Our modifications enhance the probabilistic algorithms and data structures for storing visited states, making them more effective and more usable for verifying huge transition systems. The tools also support a verification methodology designed to minimize time to finding errors, or to reaching desired certainty of error-freedom. This methodology calls for bitstate hashing, hash compaction, and integrated analyses of both to provide feedback and advice to the user. 3Spin and 3Murphi are the only tools to offer this support, and do so with the most powerful and flexible currently-available implementations of the underlying algorithms and data structures.

Bitstate hashing in SPIN has proved invaluable in probabilistically detecting errors in large models, but in many cases, the number of omitted states is much higher than it would be if SPIN allowed more than two hash functions to be used. For example, adding just one more hash function can reduce the probability of omitting states at all from 99% to under3 %. Because hash computation accounts for an overwhelming portion of the total execution cost of bitstate verification with SPIN, adding additional independent hash functions would slow down the process tremendously. We present efficient ways of computing multiple hash values that, despite sacrificing independence, give virtually the same accuracy and even yield a speed improvement in the two hash function case when compared to the current SPIN implementation.Another key to accurate bitstate hashing is utilizing as much memory as is available. The current SPIN implementation is limited to only 512MB and allows only power-of-two granularity (256MB, 128MB, etc). However, using 768MB instead of 512MB could reduce the probability of a single omission from 20% to less than one chance in 10,000, which demonstrates the magnitude of both the maximum and the granularity limitation. We have modified SPIN to utilize any addressable amount of memory and use any number of efficiently-computed hash functions, and we present empirical results from extensive experimentation comparing various configurations of our modified version to the original SPIN.

Probabilistic techniques for verification of finite-state transition systems offer huge memory savings over deterministic techniques. The two leading probabilistic schemes are hash compaction and the bitstate method, which stores states in a Bloom filter. Bloom filters have been criticized for being slow, inaccurate, and memory-inefficient, but in this paper, we show how to obtain Bloom filters that are simultaneously fast, accurate, memory-efficient, scalable, and flexible. The idea is that we can introduce large dependences among the hash functions of a Bloom filter with almost no observable effect on accuracy, and because computation of independent hash functions was the dominant computational cost of accurate Bloom filters and model checkers based on them, our savings are tremendous. We present a mathematical analysis of Bloom filters in verification in unprecedented detail, which enables us to give a fresh comparison between hash compaction and Bloom filters. Finally, we validate our work and analyses with extensive testing using 3SPIN, a model checker we developed by extending SPIN.

3SPIN is a modified version of the model checker Spin that incorporates enhancements to probabilistic algorithms and data structures for storing visited states. Such probabilistic techniques are an effective strategy for tackling state explosion—for making tractable the verification of huge transition systems. 3SPIN is written to support a verification methodology designed to minimize time to finding errors, or to reaching desired certainty of error-freedom. This methodology calls for bitstate hashing, hash compaction, and integrated analyses of both to provide feedback and advice to the user. 3SPIN is the only tool to offer this support, and does so with the most powerful and flexible currently-available implementations of the underlying algorithms and data structures.