Efficient Set Sharing using ZBDDs

Abstract. Set sharing is an abstract domain in which each concrete object is repre-sented by the set of local variables from which it might be reachable. It is a useful abstraction to detect parallelism opportunities, since it contains definite informa-tion about which variables do not share in memory, i.e., about when the memory regions reachable from those variables are disjoint. Set sharing is a more precise alternative to pair sharing, in which each domain element is a set of all pairs of local variables from which a common object may be reachable. However, the ex-ponential complexity of some set sharing operations has limited its wider applica-tion. This work introduces an efficient implementation of the set sharing domain using Zero-supressed Binary Decision Diagrams (ZBDDs). Because ZBDDs were designed to represent sets of combinations (i.e., sets of sets), they naturally repre-sent elements of the set sharing domain. We show how to synthesize the operations needed in the set sharing transfer functions from basic ZBDD operations. For some of the operations, we devise custom ZBDD algorithms that perform better in prac-tice. We also compare our implementation of the abstract domain with an efficient, compact, bitset-based alternative, and show that the ZBDD version scales better in terms of both memory usage and running time.