Complexity Analysis of Tree Share Structure

TL;DR

This paper provides a systematic theoretical analysis of the complexity of the tree share structure in concurrent separation logic, establishing decidability results and complexity bounds for its first-order theory.

Contribution

It proves the decidability of the first-order theory of Boolean algebra of tree shares and analyzes the complexity of combining additive and multiplicative theories.

Findings

First-order theory of Boolean algebra of tree shares is decidable.

Combining additive and multiplicative theories results in non-elementary complexity.

Upper bounds are established for generalized theories.

Abstract

The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are hard to implement due to a lack of a systematic theoretical study. We show that the first-order theory of the full Boolean algebra of tree shares (that is, with all tree-share constants) is decidable and has the same complexity as of the first-order theory of Countable Atomless Boolean Algebras. We prove that combining this additive structure with a constant-restricted unary multiplicative "relativization" operator has a non-elementary lower bound. We examine the consequences of this lower bound and prove that it comes from the combination of both theories by proving an upper bound on a generalization of the restricted multiplicative theory in isolation.