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.

Search-in-forest optimizer: A bio-inspired meta-heuristic algorithm for global optimization problems

The present research proposes a new particle swarm optimization-based metaheuristic algorithm entitled “search in forest (SIF) optimizer” to solve the global optimization problems. The algorithm is designed based on the organized behavior of search teams looking for missing persons in a forest. According to SIF optimizer, a number of teams each including several experts in the search field spread out across the forest and gradually move in the same direction by finding clues from the target until they find the missing person. This search structure was designed in a mathematical structure in the form of intra-group search operators and transferring the expert member to the top team. In addition, the efficiency of the algorithm was assessed by comparing the results to the standard representations and a problem with the genetic, grey wolf, salp swarm, and ant lion optimizers. According to the results, the proposed algorithm was efficient for solving many numerical representations, compared to the other algorithms.

A Novel Accuracy and Similarity Search Structure Based on Parallel Bloom Filters

In high-dimensional spaces, accuracy and similarity search by low computing and storage costs are always difficult research topics, and there is a balance between efficiency and accuracy. In this paper, we propose a new structure Similar-PBF-PHT to represent items of a set with high dimensions and retrieve accurate and similar items. The Similar-PBF-PHT contains three parts: parallel bloom filters (PBFs), parallel hash tables (PHTs), and a bitmatrix. Experiments show that the Similar-PBF-PHT is effective in membership query and K-nearest neighbors (K-NN) search. With accurate querying, the Similar-PBF-PHT owns low hit false positive probability (FPP) and acceptable memory costs. With K-NN querying, the average overall ratio and rank-i ratio of the Hamming distance are accurate and ratios of the Euclidean distance are acceptable. It takes CPU time not I/O times to retrieve accurate and similar items and can deal with different data formats not only numerical values.