Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.pascal.misc > #734

Here is my reasonning again

Show all headers | View raw

Here is my reasonning again, i think my reasonning is correct
so my proof is correct... please read again...

Hello,

Question:

Amine, how can we know that your algorithm of your
new concurrent FIFO queue works ? is it formally proved ?


Answer:

You can simply reason about the algorithm to prove that it is
correct , i will do it in front of you...

You can download the source code of the algorithm from here:

http://pages.videotron.com/aminer/

We begin by the pop() method, its source code look like this:


===

function TWQueue.push(tm : long):boolean;
var lastHead,newtemp:long;
i,j:integer;
begin

if getlength >= fsize
   then
       begin
           result:=false;
           exit;
       end;

newTemp:=LockedIncLong(head);
lastHead:=newtemp-1;

repeat
asm pause end;
until fcount1^[lastHead and fMask].flag=0;
setObject(lastHead,tm);
fcount1^[lastHead and fMask].flag:=1;
if fwait then sema.signal;
result:=true;
end;

===


you have to know that "fsize" is fixed to the length of the queue
minus a "margin" that is equal to 1000 , that means that it's limited to 
1000 threads in total that can run at the same time the push(), but you 
can vary the margin to higher the number of threads that can
run the push() at the same time...

So if getlength equal fsize-1 that means that 1000 threads can cross
because "if getlength >= fsize" can be false at the same time, but
even if it is false at the same time , there a margin of 1000 threads,
so my reasonning is correct here.

Now we look at the rest of the code...

Every cell of the array based queue look like this:

type cell = record
     obj:long;
     flag:long;
     {$IFDEF CPU32}
     cache:typecache2;
     {$ENDIF CPU32}
     {$IFDEF CPU64}
     cache:typecache3;
     {$ENDIF CPU64}
     end;

It's cache padded to a cache-line size and the array is aligned on
64 bytes so that to avoid false-sharing...

After that we increment the "head" like this with an atomic increment...

newTemp:=LockedIncLong(head);
lastHead:=newtemp-1;

and if fcount1^[lastHead and fMask].flag=0 that means there is no item
in the cell , we will write the item on the cell by doing this:

setObject(lastHead,tm);

and after that we set the flag of the cell to 1 so that the pop()
can read from it when it's set to 1 like this:

fcount1^[lastHead and fMask].flag:=1;

so as you have noticed i have reasonned and explained to you the push() 
side, and i think my reasonning is correct here.


Now we will look at the pop() side, here is the code of the pop() side:

===

function TWQueue.pop(var obj:long):boolean;

var lastTail,newtemp,newtemp1,newtemp2 : long;
begin

if fwait then sema.wait;

repeat

newtemp1:=tail;
newtemp2:=newtemp1+1;

if newtemp2<=head then
  else
   begin
    result:=false;
    exit;
   end;
if CAS(tail,newtemp1,newtemp2) then break;
sleep(0);
until false;

lastTail:=newtemp1;
repeat
asm pause end;
until fcount1^[lastTail and fMask].flag=1;
obj:=getObject(lastTail);
fcount1^[lastTail and fMask].flag:=0;
result:=true;

end;

==

The very first thing to know on the pop() side is that we must increment 
the "tail" everytime but how can we increment the tail without going 
over the "head", this is why in my invention i have used a lockfree 
mechanism like this

==

repeat

newtemp1:=tail;
newtemp2:=newtemp1+1;

if newtemp2<=head then
  else
   begin
    result:=false;
    exit;
   end;
if CAS(tail,newtemp1,newtemp2) then break;
sleep(0);
until false;

==

It's like in lockfree algorithms , i have to copy and memories
the "tail" into the newtemp1 variable and after that increment newtemp1 
, so if newtemp1+1 is less or equal to "head" that means we are correct 
and we have not go over the head , after that with a lockfree mechanism 
we will test with a CAS that tail is still equal to newtemp1 to be able 
to increment the "tail" , so my reasonnning is correct here.

After that we have to wait to see if there is an item in the cell by
doing this:

repeat
asm pause end;
until fcount1^[lastTail and fMask].flag=1;


If there is an item on the cell we will get it
and set the flag of the cell to 0 to say to
the push() threads that they can push() to this cell by doing this:


obj:=getObject(lastTail);
fcount1^[lastTail and fMask].flag:=0;



So as you have noticed this is my new algorithm
and i have presented to you my reasonning to prove
to you that my algorithm is correct, and i think
my algorithm is correct.



Thank you,
Amine Moulay Ramdane.

Back to comp.lang.pascal.misc | Previous | Next | Find similar

Thread

Here is my reasonning again aminer <aminer@toto.net> - 2014-04-24 20:28 -0700

csiph-web