Modelling concurrent objects running on the TSO and ARMv8 memory models.

•Presents a method for using a standard linearizability proof method on hardware weak memory models.•Generates a transition system, which reflects on weak memory model behaviour, from a given piece of code.•Covers the widely used TSO memory model, as well as the latest version of the ARM processor, ARMv8.•Enables the use of a model checker to check correctness of code, taking into account TSO/ARMv8 weak memory behaviour.