This paper revisits the fundamental problem of monitoring the linearizability of concurrent stacks, queues, sets, and multisets. Given a history of a library implementing one of these abstract data types, the monitoring problem is to answer whether the given history is linearizable. For stacks, queues, and (multi)sets, we present monitoring algorithms with complexities 𝓞(𝑛 2 ), 𝓞(𝑛 𝑙𝑜𝑔 𝑛), and 𝓞(𝑛), respectively, where 𝑛 is the number of operations in the input history. For stacks and queues, our results hold under the standard assumption of data-independence, i.e., the behavior of the library is not sensitive to the actual values stored in the data structure. Past works to solve the same problems have cubic time complexity and (more seriously) have correctness issues: they either (i) lack correctness proofs or (ii) the suggested correctness proofs are erroneous (we present counter-examples), or (iii) have incorrect algorithms. Our improved complexity results rely on substantially different algorithms for which we provide detailed proofs of correctness. We have implemented our stack and queue algorithms in 𝐿𝑖𝑀𝑜 (Linearizability Monitor). We evaluate 𝐿𝑖𝑀𝑜 and compare it with the state-of-the-art tool 𝑉𝑖𝑜𝑙𝑖𝑛 – whose correctness proofs we have found errors in – which checks for linearizability violations. Our experimental evaluation confirms that 𝐿𝑖𝑀𝑜 outperforms 𝑉𝑖𝑜𝑙𝑖𝑛 regarding both efficiency and scalability.

The problem of whether a recursive query can be rewritten as query without recursion is a fundamental reasoning task, known as the boundedness problem. Here we study the boundedness problem for Unions of Conjunctive Regular Path Queries (UCRPQs), a navigational query language extensively used in ontology and graph database querying. The boundedness problem for UCRPQs is known to be decidable, ExpSpace-complete. Here we focus our analysis on UCRPQs using simple regular expressions, which are of high practical relevance and enjoy a lower reasoning complexity. We show that the complexity for the boundedness problem for this UCRPQs fragment is Pi-p-2-complete, and that an equivalent bounded query can be produced in polynomial time whenever possible. When the query turns out to be unbounded, we also study the task of finding an equivalent maximally bounded query, which we show to be feasible in Pi-p-2 . As a side result of independent interest stemming from our developments, we study a notion of succinct finite automata and prove that its membership problem is NP-complete.