M&S queue is not actually linearizable
Dmitriy Vyukov
ms_queue* q = new ms_queue;
// thread 1
ms_queue_node* node = new ms_queue_node(1);
q->enqueue(node);
// thread 2
ms_queue_node* node = q->dequeue();
if (node)
delete q;
If the queue would be actually linearizable (all operations happen
atomically at some instant in time during a method invocation), then
the program must work correctly. But it can corrupt memory/crash.
Sorry guys, there are 2 distinct operations in enqueue(): (1) make an
item available for consuming, and (2) shift tail pointer, and it's
externally observable that they happen non atomically.
Note that the program works correctly with a mutex-based queue,
because mutexes are implemented in such a way that an actual unlock is
"a last touch". So all mutex-protected operations happen really
atomically w/o any externally observable quirks.
--
Dmitriy V'jukov
Dmitriy Vyukov
> Consider the following program:
>
> ms_queue* q = new ms_queue;
>
> // thread 1
> ms_queue_node* node = new ms_queue_node(1);
> q->enqueue(node);
>
> // thread 2
> ms_queue_node* node = q->dequeue();
> if (node)
> delete q;
>
> If the queue would be actually linearizable (all operations happen
> atomically at some instant in time during a method invocation), then
> the program must work correctly. But it can corrupt memory/crash.
>
> Sorry guys, there are 2 distinct operations in enqueue(): (1) make an
> item available for consuming, and (2) shift tail pointer, and it's
> externally observable that they happen non atomically.
Here is more realistic example which does not work with M&S queue
because it's not linearizable:
struct tcp_connection
{
queue_t q;
...
};
void connection_thread(tcp_connection* c)
{
for (;;)
{
msg_t* m = c->dequeue();
if (m->type == MSG_DISCONNECT)
{
delete c;
return;
}
process(m);
}
}
void io_dispatch_thread()
{
for (;;)
{
select(...);
for_each(SOCKET s in read_set)
{
recv(s, buf, size);
tcp_connection* c = find_connection(s);
c->enqueue(msg_t(MSG_PACKET, data, size));
}
for_each(SOCKET s in exception_set)
{
tcp_connection* c = find_connection(s);
c->enqueue(msg_t(MSG_DISCONNECT));
}
}
}
--
Dmitriy V'jukov
Andy Venikov
> Consider the following program:
>
> ms_queue* q = new ms_queue;
>
> // thread 1
> ms_queue_node* node = new ms_queue_node(1);
> q->enqueue(node);
>
> // thread 2
> ms_queue_node* node = q->dequeue();
> if (node)
> delete q;
>
I'm sorry Dmitriy, what queue are you referring to?
Michael-Scott queue?
Andy.
Dmitriy Vyukov
Yes. This one:
http://www.cs.rochester.edu/research/synchronization/pseudocode/queues.html
("Non-Blocking Concurrent Queue Algorithm")
--
Dmitriy V'jukov
Andy Venikov
Are you saying that construction/destruction of the queue is not
linearizable? I don't think it was the intent.
I think that the whole paper (not the one that you pointed to but
http://www.research.ibm.com/people/m/michael/podc-1996.pdf)
only talks about enque/deque operations being linearizable against each
other.
I don't think it actually talked about queue destruction at all.
But you still have a good point.
Andy.
Dmitriy Vyukov
> Dmitriy Vyukov wrote:
> > On May 13, 7:51 pm, Andy Venikov <swojchelo...@gmail.com> wrote:
> >> Dmitriy Vyukov wrote:
> >>> Consider the following program:
> >>> ms_queue* q = new ms_queue;
> >>> // thread 1
> >>> ms_queue_node* node = new ms_queue_node(1);
> >>> q->enqueue(node);
> >>> // thread 2
> >>> ms_queue_node* node = q->dequeue();
> >>> if (node)
> >>> delete q;
> >> <snip>
>
> >> I'm sorry Dmitriy, what queue are you referring to?
> >> Michael-Scott queue?
>
> > Yes. This one:
> > ("Non-Blocking Concurrent Queue Algorithm")
>
> linearizable? I don't think it was the intent.
> I think that the whole paper (not the one that you pointed to but
>
> http://www.research.ibm.com/people/m/michael/podc-1996.pdf)
>
> only talks about enque/deque operations being linearizable against each
> other.
> I don't think it actually talked about queue destruction at all.
> But you still have a good point.
No, I am not talking about destruction, destruction is purely single-
threaded operation and must be invoked only when no other threads work
with the object.
It's enqueue() that is not linearizable. If it would be linearizable
(*really* linearizable) then it would be safe to destroy the queue
where I destroy it (indeed, the other thread already completed the
enqueue operation, so no other thread works with the queue).
My examples work with a mutex-based queue. And the practical meaning
of linearizability is that one may replace mutex-based object with
linearizable object, and observe no differences. As you see, it's not
the case with M&S queue. So one must be careful when replace mutex-
based queue with M&S queue, the program can start crashing and
corrupting memory (Intel TBB concurrent_queue has the same drawback).
And IMVHO my example with connections looks not too unrealistic to
ignore the problem.
Btw, AFAIR their original paper on the queue contains formal proof of
linearizability. And I believe that the proof is correct in itself, it
just proves something else. The problem of mathematical abstraction...
--
Dmitriy V'jukov
Andy Venikov
<snip>
I'm not sure if you had a typo or not, but here:
>
> No, I am not talking about destruction, destruction is purely single-
> threaded operation and must be invoked only when no other threads work
> with the object.
you say that you're not talking about destruction, and here:
> It's enqueue() that is not linearizable. If it would be linearizable
> (*really* linearizable) then it would be safe to destroy the queue
> where I destroy it
you are talking about destruction.
I understand that your point is that it's not safe to destroy MS queue
without taking special precautions, and it's a good point. I expect a
lot of developers will get bad surprises.
>
> Btw, AFAIR their original paper on the queue contains formal proof of
> linearizability. And I believe that the proof is correct in itself, it
> just proves something else. The problem of mathematical abstraction...
It does, section 3.2
It proves that Dequeue and Enqueue are linearizable relative to each
other. It doesn't talk about queue destruction. I wonder if the authors
didn't talk about destruction deliberately since they didn't have a
solution for it. Or maybe they weren't even trying to solve it - the
paper is all about enqueing/dequeing after all.
> --
> Dmitriy V'jukov
Andy.
Dmitriy Vyukov
> Dmitriy Vyukov wrote:
>
> <snip>
> I'm not sure if you had a typo or not, but here:
>
> > No, I am not talking about destruction, destruction is purely single-
> > threaded operation and must be invoked only when no other threads work
> > with the object.
>
> you say that you're not talking about destruction, and here:
>
> > It's enqueue() that is not linearizable. If it would be linearizable
> > (*really* linearizable) then it would be safe to destroy the queue
> > where I destroy it
>
> you are talking about destruction.
Well, let's say I mentioned destruction :) By my point is actually
about enqueue(), destruction is just so far as.
> I understand that your point is that it's not safe to destroy MS queue
> without taking special precautions, and it's a good point. I expect a
> lot of developers will get bad surprises.
>
> > Btw, AFAIR their original paper on the queue contains formal proof of
> > linearizability. And I believe that the proof is correct in itself, it
> > just proves something else. The problem of mathematical abstraction...
>
> It does, section 3.2
> It proves that Dequeue and Enqueue are linearizable relative to each
> other. It doesn't talk about queue destruction.
But how they describe the guarantees? Did they say that the queue is
linearazable? Or they said "Dequeue and Enqueue are linearizable
relative to each other"? If the former, than all operations must be
linearazable relative to any other.
> I wonder if the authors
> didn't talk about destruction deliberately since they didn't have a
> solution for it. Or maybe they weren't even trying to solve it - the
> paper is all about enqueing/dequeing after all.
I don't know...
--
Dmitriy V'jukov
Andy Venikov
<snip>
> But how they describe the guarantees? Did they say that the queue is
> linearazable? Or they said "Dequeue and Enqueue are linearizable
> relative to each other"? If the former, than all operations must be
> linearazable relative to any other.
Well, it says: "The presented algorithms are linearizable". And since
they only presented Enqueu and Dequeue algorithms and did not present a
queue destruction algorithm, I guess technically they are correct.
But a few people are in for a surprise I gather...
> Dmitriy V'jukov
Andy.