lock-free

In the middle of a flurry of work on relaxed semantics, Henzinger et al. published the paper Quantitative Relaxation of Concurrent Data Structures in 2013. Its primary contribution is ironing out a framework for the theory of relaxed semantics. The idea is to allow incorrect transitions between states in the data structure specification while being able to associate different paths or transitions with different costs. Furthermore, they create a relaxed out-of-order stack. Here we will concisely but informally present the theory, and in the end, quickly outline the stack.