Lockfree_SPMC and the correctness
Amine
Hello,
My lockfree_SPMC, is doing this
on the pop() side:
1 repeat
2 lastHead:=head[0];
3 obj:=getObject(integer(lastHead));
4 if tail[0]<>head[0]
5 then begin
6 if CAS(head[0],lasthead,lasthead+1)
7 then
8 begin
9 result:=true;
10 exit;
12 end;
13 end
14 else
15 begin
16 result:=false;
17 exit;
18 end;
19 until false;
Let suppose that head = tail -1 , and one or many threads
have crossed line number 4, one of them will succeed
and the others will rollback, and they will find that
head is equal to tail and they will exit. So, that's correct.
In the push side we are safe also..
And i have responded to Dmitriy V'jukov also, read this:
Dmitriy V'jukov wrote:
> Assume consumer has read the object, then he is
>preempted so that he misses 1000 pops and pushes,
>then the consumer scheduled again and his CAS
>accidentally succeeds.
It can't succeed cause head[0] will be different from lastHead
and CAS(head[0],lasthead,lasthead+1) will return false.
>In result, he returns very old object that
> was already consumed. I think here is another
> issue. Assume consumer successfully verifies
> that tail[0]<>head[0], then he is preempted and
>misses 1000 pushes and 1001 pops, so that head
> stay the same, however now tail==head. CAS
tail==head but head and lasthead are not equal, so
CAS will not succeed.
And suppose that between line 2 and line 4 head has
changed, it will exit if tail = head or it will rollback.
And in line 2 in the pop() side i am doing this:
lastHead:=head[0];
lasthead is local and head is a global variable
and in assembler it gives:
mov [004054d0], eax
it is: mov memory, register
and it take only *one* clock, so, we can not get a garbage
value in lasthead, and if head have changed it will rollback.
Dmitriy V'jukov wrote:
>Chris,
>Regarding race detected by Relacy. I think it's a benign race and data
>items must be declared as atomic<> instead of var<>. Assume following
>situation. Consumer reads data item, them he is preempted for a long
>time. In that time, producer and other consumers may 'spin queue
>around', i.e. ARRAY_SIZE elements will be consumed and ARRAY_SIZE
>elements will be produced. So now producer may actually write to the
>location first preempted consumer 'just' read - that's why Relacy
>shows a data race I think. However then CAS will inevitably fail for
>that preempted consumer, so algorithm correctness is not broken.
>Btw, can't Pascal compiler reorder following 2 operations for
>producer:
>setObject(Tail[0],tm);
>inc(tail[0]);
>?
>I guess there is no such guarantee in the language spec.
I have looked at the assembler code and it does not reorder
the two operations.
Hence, my lockfree_SPMC and lockfree_priority_SPMC
are safe and correct.
Thank you for your time.
Regards,
Amine.
Chris M. Thomasson
news:55d911c7-de45-4131...@l31g2000vbp.googlegroups.com...
[...]
> I have looked at the assembler code and it does not reorder
> the two operations.
>
> Hence, my lockfree_SPMC and lockfree_priority_SPMC
> are safe and correct.
Are you sure that any Pascal compiler will never reorder the operations?
[...]
Amine
No Chris, not for any Pascal compiler.
I have just verified for Delphi and Freepascal.
Regards,
Amine.
Chris M. Thomasson
Of course you can totally eliminate this "possibility" by coding your
`lockfree_SPMC' algorithm in pure assembly language; assemble and link to
the object file.