If you can definitely prove that a method has no linearization points, does it necessarily mean that that method is not linearizable? Also, as a sub question, how can you prove that a method has no linearization points?
If you can definitely prove that a method has no linearization points, does it necessarily mean that that method is not linearizable?
Firstly, linearizability is not property of a method, it is property of execution sequence.
how can you prove that a method has no linearization points?
It depends on the execution sequence whether we are able to find linearization point for the method or not.
For example, we have the below sequence, for thread A on a FIFO queue. t1, t2, t3 are time intervals.
A.enq(1) A.enq(2) A.deq(1)
t1 t2 t3
We can choose linearization points(lp) for first two enq methods as any points in time interval t1 and t2 respectively, and for deq any point in t3. The points that we choose are lp for these methods.
Now, consider a faulty implementation
A.enq(1) A.enq(2) A.deq(2)
t1 t2 t3
Linerizability allows lp to respect the real-time ordering. Therefore, lp of the methods should follow the time ordering i.e. t1 < t2 < t3. However, since our implementation is incorrect, we cannot clearly do this. Hence, we cannot find linearization point for the method A.deq(2), in turn our seq. too in not linerizable.
Hope this helps, if you need to know more you can read this book: http://www.amazon.com/Art-Multiprocessor-Programming-Maurice-Herlihy/dp/0123705916