Verifying concurrent multicopy search structures

Multicopy search structures such as log-structured merge (LSM) trees are optimized for high insert/update/delete (collectively known as upsert) performance. In such data structures, an upsert on key k , which adds ( k , v ) where v can be a value or a tombstone, is added to the root node even if k is already present in other nodes. Thus there may be multiple copies of k in the search structure. A search on k aims to return the value associated with the most recent upsert. We present a general framework for verifying linearizability of concurrent multicopy search structures that abstracts from the underlying representation of the data structure in memory, enabling proof-reuse across diverse implementations. Based on our framework, we propose template algorithms for (a) LSM structures forming arbitrary directed acyclic graphs and (b) differential file structures, and formally verify these templates in the concurrent separation logic Iris. We also instantiate the LSM template to obtain the first verified concurrent in-memory LSM tree implementation.

Download Full-text

Monadic Tree Print

Journal of Applied Computer Science Methods ◽

10.1515/jacsm-2015-0005 ◽

2014 ◽

Vol 6 (2) ◽

pp. 147-157

Author(s):

Konrad Grzanek

Keyword(s):

Programming Language ◽

Data Structures ◽

Functional Programming ◽

Directed Acyclic Graphs ◽

Functional Programming Language ◽

Output Stream ◽

Acyclic Graphs ◽

Large Trees

Abstract Directed acyclic graphs and trees in particular belong to the most extensively used data structures. Visualizing them properly is a key to a success when developing complex algorithms that make use of them. Textual visualizations a la UNIX tree command is essential when the urge is to deal with large trees. Our aim was to design a library that would exploit this approach and to make an implementation of it for a purely functional programming language. The library uses monads to print directly into an output stream or to generate immutable Strings. This paper gives a detailed overview of the solution.

Download Full-text

Storing Set Families More Compactly with Top ZDDs

Algorithms ◽

10.3390/a14060172 ◽

2021 ◽

Vol 14 (6) ◽

pp. 172

Author(s):

Kotaro Matsuda ◽

Shuhei Denzumi ◽

Kunihiko Sadakane

Keyword(s):

Data Structures ◽

Binary Decision Diagrams ◽

Real Data ◽

Directed Acyclic Graphs ◽

Main Memory ◽

Large Set ◽

Decision Diagrams ◽

Binary Decision ◽

Acyclic Graphs

Zero-suppressed Binary Decision Diagrams (ZDDs) are data structures for representing set families in a compressed form. With ZDDs, many valuable operations on set families can be done in time polynomial in ZDD size. In some cases, however, the size of ZDDs for representing large set families becomes too huge to store them in the main memory. This paper proposes top ZDD, a novel representation of ZDDs which uses less space than existing ones. The top ZDD is an extension of the top tree, which compresses trees, to compress directed acyclic graphs by sharing identical subgraphs. We prove that navigational operations on ZDDs can be done in time poly-logarithmic in ZDD size, and show that there exist set families for which the size of the top ZDD is exponentially smaller than that of the ZDD. We also show experimentally that our top ZDDs have smaller sizes than ZDDs for real data.

Download Full-text

Reasoning about conditional constraint specification problems and feature models

Artificial intelligence for engineering design analysis and manufacturing ◽

10.1017/s0890060410000600 ◽

2011 ◽

Vol 25 (2) ◽

pp. 163-174 ◽

Cited By ~ 2

Author(s):

Raphael Finkel ◽

Barry O'Sullivan

Keyword(s):

Constraint Satisfaction ◽

Directed Acyclic Graphs ◽

Constraint Satisfaction Problems ◽

Product Configuration ◽

Feature Models ◽

Model Builder ◽

A Value ◽

Acyclic Graphs ◽

All Solutions ◽

Constraint Specification

AbstractProduct configuration is a major industrial application domain for constraint satisfaction techniques. Conditional constraint satisfaction problems (CCSPs) and feature models (FMs) have been developed to represent configuration problems in a natural way. CCSPs are like constraint satisfaction problems (CSPs), but they also include potential variables, which might or might not exist in any given solution, as well as classical variables, which are required to take a value in every solution. CCSPs model, for example, options on a car, for which the style of sunroof (a variable) only makes sense if the car has a sunroof at all. FMs are directed acyclic graphs of features with constraints on edges. FMs model, for example, cell phone features, where utility functions are required, but the particular utility function “games” is optional, but requires Java support. We show that existing techniques from formal methods and answer set programming can be used to naturally model CCSPs and FMs. We demonstrate configurators in both approaches. An advantage of these approaches is that the model builder does not have to reformulate the CCSP or FM into a classic CSP, converting potential variables into classical variables by adding a “does not exist” value and modifying the problem constraints. Our configurators automatically reason about the model itself, enumerating all solutions and discovering several kinds of model flaws.

Download Full-text

Formal verification of a concurrent bounded queue in a weak memory model

Proceedings of the ACM on Programming Languages ◽

10.1145/3473571 ◽

2021 ◽

Vol 5 (ICFP) ◽

pp. 1-29

Author(s):

Glen Mével ◽

Jacques-Henri Jourdan

Keyword(s):

Formal Verification ◽

Data Structures ◽

Experimental Verification ◽

Separation Logic ◽

Memory Model ◽

Formal Reasoning ◽

Concurrent Data Structures ◽

Concurrent Separation Logic

We use Cosmo, a modern concurrent separation logic, to formally specify and verify an implementation of a multiple-producer multiple-consumer concurrent queue in the setting of the Multicore OCaml weak memory model. We view this result as a demonstration and experimental verification of the manner in which Cosmo allows modular and formal reasoning about advanced concurrent data structures. In particular, we show how the joint use of logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and the weak memory model.

Download Full-text

A Uniform Framework for Concept Definitions in Description Logics

Journal of Artificial Intelligence Research ◽

10.1613/jair.334 ◽

1997 ◽

Vol 6 ◽

pp. 87-110 ◽

Cited By ~ 17

Author(s):

G. De Giacomo ◽

M. Lenzerini

Keyword(s):

Data Structures ◽

Description Logic ◽

Description Logics ◽

Directed Acyclic Graphs ◽

Acyclic Graphs ◽

Class Definition ◽

Recursive Data Structures ◽

Recursive Data ◽

Recursive Definitions ◽

Representation Formalism

Most modern formalisms used in Databases and Artificial Intelligence for describing an application domain are based on the notions of class (or concept) and relationship among classes. One interesting feature of such formalisms is the possibility of defining a class, i.e., providing a set of properties that precisely characterize the instances of the class. Many recent articles point out that there are several ways of assigning a meaning to a class definition containing some sort of recursion. In this paper, we argue that, instead of choosing a single style of semantics, we achieve better results by adopting a formalism that allows for different semantics to coexist. We demonstrate the feasibility of our argument, by presenting a knowledge representation formalism, the description logic muALCQ, with the above characteristics. In addition to the constructs for conjunction, disjunction, negation, quantifiers, and qualified number restrictions, muALCQ includes special fixpoint constructs to express (suitably interpreted) recursive definitions. These constructs enable the usual frame-based descriptions to be combined with definitions of recursive data structures such as directed acyclic graphs, lists, streams, etc. We establish several properties of muALCQ, including the decidability and the computational complexity of reasoning, by formulating a correspondence with a particular modal logic of programs called the modal mu-calculus.

Download Full-text