Specifying highly concurrent data structure manipulation