Is a method with no linearization points always no

Question

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 linearizatioon points?

Answer 1

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 linearizatioon 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

Answer 2

This answer is based on me reading about linearizability on wikipedia for the first time, and trying to map it to my existing understanding of memory consistency through happens-before relationships. So I may be misunderstanding the concept.

If you can definitely prove that a method has no linearization points, does it necessarily mean that that method is not linearizable?

It is possible to have a scenario where shared, mutable state is concurrently operated on by multiple threads without any synchronization or visibility aids, and still maintain all invariants without risk of corruption.

However, those cases are very rare.

how can you prove that a method has no linearizatioon points?

As I understand linearization points, and I may be wrong here, they are where happens-before relationships are established between threads. If a method (recursively through every method it calls in turn) establishes no such relationships, then I would assert that it has no linearizatioon points.

Answer 3

To build upon the answers described above, a method can be described as linearizable. As referenced in the book that djoker mentioned: http://www.amazon.com/dp/0123705916/?tag=stackoverfl08-20

on page 69, exercise 32, we see

It should be noted that enq() is indeed a method, that is described as possibily being linearizable/not linearizable.

Proving that there are linearizable points comes down to finding if there are examples that can break linearizability. If you make the assumption that various read/write memory operations in a method are linearizable, and then prove by contradiction that there are non-linearizable situations that result from such an assumption, you can declare that the previously mentioned read/write operation is not a valid linearization point.

Take, for example, the following enq()/deq() methods, assuming they are part of a standard queue implementation with head/tail pointers thaand a backing array "arr":

public terribleQueue(){
  arr = new T[10];
  tail = 0;
  head = 0;
}

void enq(T x){
  int slot = tail;
  arr[slot] = x;
  tail = tail + 1;
}

T deq(){
  if( head == tail ) throw new EmptyQueueException();
  T temp = arr[head];
  head = head + 1;
  return temp;
}  

In this terrible implementation, we can easily prove, for example, that the first line of enq is not a valid linearization point, by assuming that it is a linearization point, and then finding an example displaying otherwise, as seen here:

Take the example two threads, A and B, and the example history:

A: enq( 1 )
A: slot = 0
B: enq( 2 )
B: slot = 0

(A and B are now past their linearization points, therefore we are not allowed to re-order them to fit our history)

A: arr[0] = 1
B: arr[0] = 2
A: tail = 1
B: tail = 2

C: deq()
C: temp = arr[0] = 2
C: head = 1
C: return 2

Now we see that because of our choice of linearization point (which fixes the order of A and B), this execution will be impossible make linearizable, because we cannot make C's deq return 1, no matter where we put it.

Kind of a long winded answer, but I hope this helps