Linearizability is a correctness criterion for concurrent objects. In this paper, we prove linearizability of a concurrent lock-free stack implementation by showing the implementation to be a non-atomic refinement of an abstract stack. To this end, we develop a generalisation of non-atomic refinement allowing one to refine a single (Z) operation into a CSP process. Besides this extension, the definition furthermore embodies a termination condition which permits one to prove starvation freedom for the concurrent processes.