Proving correctness of highly−concurrent linearisable objects Dahkki Vafeiadis, V, Herlihy, M, Hoare, T, Shapiro, M