Abstract
The tree share structure proposed by Dockins et al. provides an elegant model for tracking disjoint ownership in concurrent separation logic. However, decision procedures for tree shares are difficult to implement due to the lack of a systematic theoretical study. We show that the first-order theory of the full Boolean algebra of tree shares (with all tree-share constants) is decidable and has the same complexity as the first-order theory of Countable Atomless Boolean Algebras. We further prove that combining this additive structure with a constant-restricted unary multiplicative "relativization" operator yields a non-elementary lower bound. We analyze the source of this lower bound and demonstrate that it arises from the interaction between the two theories, by establishing an upper bound for a generalization of the restricted multiplicative theory in isolation.