M. Abadi & L. Lamport (1991):
The existence of refinement mappings.
Theoretical Computer Science 82(2),
pp. 253–284,
doi:10.1016/0304-3975(91)90224-P.
J. Alglave, L. Maranget & M. Tautschnig (2014):
Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.
ACM Trans. Program. Lang. Syst. 36(2),
pp. 7:1–7:74,
doi:10.1145/2627752.
R.-J.R. Back (1990):
Refinement calculus, part II: Parallel and reactive programs.
In: Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness.
Springer,
pp. 67–93,
doi:10.1007/3-540-52559-9\voidb@x width0.4em60.
S. Burckhardt, A. Gotsman, M. Musuvathi & H. Yang (2012):
Concurrent Library Correctness on the TSO Memory Model.
In: H. Seidl: ESOP 2012,
LNCS 7211.
Springer,
pp. 87–107,
doi:10.1007/978-3-642-28869-2\voidb@x width0.4em5.
R.J. Colvin & G. Smith (2018):
A wide-spectrum language for verification of programs on weak memory models.
In: K. Havelund, J. Peleska, B. Roscoe & E. de Vink: FM 2018,
LNCS 10951.
Springer,
pp. 240–257,
doi:10.1007/978-3-319-95582-7\voidb@x width0.4em14.
J. Derrick, G. Smith & B. Dongol (2014):
Verifying linearizability on TSO architectures.
In: E. Albert & E. Sekerinski: iFM 2014,
LNCS 8739.
Springer,
pp. 341–356,
doi:10.1007/978-3-319-10181-1\voidb@x width0.4em21.
B. Dongol & L. Groves (2016):
Contextual Trace Refinement for Concurrent Objects: Safety and Progress.
In: K. Ogata, M. Lawford & S. Liu: ICFEM 2016.
Springer,
pp. 261–278,
doi:10.1007/978-3-319-47846-3\voidb@x width0.4em17.
B. Dongol, R. Jagadeesan, J. Riely & A. Armstrong (2018):
On abstraction and compositionality for weak-memory linearisability.
In: I. Dillig & J. Palsberg: VMCAI'18,
LNCS 10747.
Springer,
pp. 183–204,
doi:10.1007/978-3-319-73721-8\voidb@x width0.4em9.
I. Filipovi\'c, P. W. O'Hearn, N. Rinetzky & H. Yang (2010):
Abstraction for concurrent objects.
Theoretical Computer Science 411(51-52),
pp. 4379 – 4398,
doi:10.1016/j.tcs.2010.09.021.
S. Flur, K.E. Gray, C. Pulte, S. Sarkar, A. Sezgin, L. Maranget, W. Deacon & P. Sewell (2016):
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA.
In: R. Bodik & R. Majumdar: POPL 2016.
ACM,
pp. 608–621,
doi:10.1145/2837614.2837615.
A. Gotsman, M. Musuvathi & H. Yang (2012):
Show No Weakness: Sequentially Consistent Specifications of TSO Libraries.
In: M. Aguilera: DISC 2012,
LNCS 7611.
Springer,
pp. 31–45,
doi:10.1007/978-3-642-28869-2\voidb@x width0.4em5.
M. Herlihy & J. M. Wing (1990):
Linearizability: A Correctness Condition for Concurrent Objects.
ACM Trans. Program. Lang. Syst. 12(3),
pp. 463–492,
doi:10.1145/78969.78972.
M. Moir & N. Shavit (2004):
Concurrent data structures.
Handbook of Data Structures and Applications,
pp. 47:1–47:30,
doi:10.1201/9781420035179.ch47.
S. Owens, S. Sarkar & P. Sewell (2009):
A Better x86 Memory Model: x86-TSO.
In: S. Berghofer, T. Nipkow, C. Urban & M. Wenzel: TPHOLs 2009,
LNCS 5674.
Springer,
pp. 391–407,
doi:10.1007/978-3-642-03359-9\voidb@x width0.4em27.
P. Sewell, S. Sarkar, S. Owens, F.Z. Nardelli & M.O. Myreen (2010):
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors.
Commun. ACM 53(7),
pp. 89–97,
doi:10.1145/1785414.1785443.
G. Smith & K. Winter (2017):
Relating trace refinement and linearizability.
Formal Aspects of Computing 29(6),
pp. 935–950,
doi:10.1007/s00165-017-0418-2.
O. Travkin, A. Mütze & H. Wehrheim (2013):
SPIN as a Linearizability Checker under Weak Memory Models.
In: V. Bertacco & A. Legay: HVC2013,
LNCS 8244.
Springer,
pp. 311–326,
doi:10.1007/978-3-319-03077-7\voidb@x width0.4em21.
eptcs@eptcs.org