Auto-parallelization of data structure operations for GPUs

We present an auto-parallelization technique for generating GPU implementation of data-structure operations from a sequential specification. The technique partitions the data-structure operations into barrier-separated phases such that each phase executes only homogeneous operations. Homogeneity is dictated by the method type, which is derived from the specification. Two key aspects of our technique are: (i) it ensures linearizability of the data-structure, and (ii) it is capable of composing multiple data-structure operations with the guarantee of optimal barrier placement, which we formally prove. We illustrate the usefulness of our techniques by synthesizing efficient GPU implementations of practical graph algorithms like single-source shortest paths which uses a concurrent worklist, Delaunay mesh refinement that uses a worklist and a mesh, and a doubly linked-list supporting arbitrary insertion and deletion.