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

Groups > comp.programming.threads > #2753 > unrolled thread

Here is my proof again

Back to article view | Back to comp.programming.threads

Contents

  Here is my proof again Ramine <ramine@1.1> - 2014-12-07 11:57 -0800
    Re: Here is my proof again Ramine <ramine@1.1> - 2014-12-07 12:10 -0800

#2753 — Here is my proof again

Hello,

I have added more to the sequential consistency proof,
and i have corrected some typos , please read again...


Here is my proof:

Look at the source code, when Fcount5^.fcount5 equal 0 in the writer 
side , the reader side will be run in a Seqlock mode, , i don't need to 
proove Seqlock because my Seqlock algorithm is correct, just compare it 
to the other Seqlock algorithms and you will notice it, what i need to 
proof is when Fcount6^.fcount6 modulo "the number of cores" is equal to 
0 , that means that we are in a distributed mode, so when we are in a 
distributed mode, the reader side of my algorithm will enter the 
distributed reader-writer lock or it will wait for the distributed 
reader-writer lock to exit, if the reader side enters the distributed 
reader-writer lock , if Fcount6^.fcount6 has not changed on the 
RUnlock(), the reader thread will exit with a "true" value, if 
Fcount6^.fcount6 has changed, the RUnlock() method will catch it and it 
will rollback with Seqlock mechanism, now if  Fcount6^.fcount6 modulo 
"the number of cores" is equal to 0 on RLock() , and the reader side 
waits for the writer side to enter the distributed reader-writer lock,
the reader side after that will enter the distributed reader-writer lock 
and  if Fcount6^.fcount6 modulo "the number of cores" has changed
on RUnlock(), the reader side will rollback in a Seqlock mode, if not,
RUnlock() will exit with the value of "true". So all in all my algorithm 
is correct.

About the sequential consistency of  my scalable distributed sequential 
lock, my algorithm works on x86 architecture and i think my algorithm is 
correct cause look at the source code of the WLock() method, since i am 
using a Ticket spinlock with a proportional backoff on the writer side, 
the Ticket spinlock is using a "lock add" assembler instruction to 
increment a counter in the Enter() method of the ticket spinlock , and 
this "lock add" assembler instruction is a barrier for stores and loads 
on x86, and the stores of Fcount6^.fcount6 and FCount5^.fcount5
are not reordred with the stores of the writer section, so the WLock() 
method is sequential consistent and correct, now look at the WUnlock() , 
we don't need an "sfence" cause stores on WUnlock() are not reordered 
with older stores on x86 , so WUnlock() method is sequential consistent 
and correct, now look at the RLock() method, the loads inside RLock() 
method are not reordered with the loads of the reader section  ,  and on 
RUnlock(), the loads of RUnlock() are not reordered with older loads of 
the critical section , so all in all my algorithm i think my algorithm 
is sequential consistent and correct on x86. So be confident cause i 
have reasoned correctly and i think my algorithm is correct and it is a 
powerful synchronization mechanism that can replace RCU and that can 
replace Seqlock cause it beats Seqlock.


So this was my proof that my algorithm is correct.

You can download my scalable distributed sequential lock version 1.11 from:

https://sites.google.com/site/aminer68/scalable-distributed-sequential-lock


Read this about my scalable distributed sequential lock:


Disclaimer:

My software is provided on an "as-is" basis, with no warranties,
express or implied.  The entire risk and liability of using it is yours. 
Any damages resulting from the use or misuse of this software will be 
the responsibility of the user.



Thank you,
Amine Moulay Ramdane.

[toc] | [next] | [standalone]

#2754

On 12/7/2014 11:57 AM, Ramine wrote:
>
> Hello,
>
> I have added more to the sequential consistency proof,
> and i have corrected some typos , please read again...
>
>
> Here is my proof:
>
> Look at the source code, when Fcount5^.fcount5 equal 0 in the writer
> side , the reader side will be run in a Seqlock mode, , i don't need to
> proove Seqlock because my Seqlock algorithm is correct, just compare it
> to the other Seqlock algorithms and you will notice it, what i need to
> proof is when Fcount6^.fcount6 modulo "the number of cores" is equal to
> 0 , that means that we are in a distributed mode, so when we are in a
> distributed mode, the reader side of my algorithm will enter the
> distributed reader-writer lock or it will wait for the distributed
> reader-writer lock to exit, if the reader side enters the distributed
> reader-writer lock , if Fcount6^.fcount6 has not changed on the
> RUnlock(), the reader thread will exit with a "true" value, if
> Fcount6^.fcount6 has changed, the RUnlock() method will catch it and it
> will rollback with Seqlock mechanism, now if  Fcount6^.fcount6 modulo
> "the number of cores" is equal to 0 on RLock() , and the reader side
> waits for the writer side to enter the distributed reader-writer lock,
> the reader side after that will enter the distributed reader-writer lock
> and  if Fcount6^.fcount6 modulo "the number of cores" has changed
> on RUnlock(), the reader side will rollback in a Seqlock mode, if not,
> RUnlock() will exit with the value of "true". So all in all my algorithm
> is correct.
>
> About the sequential consistency of  my scalable distributed sequential
> lock, my algorithm works on x86 architecture and i think my algorithm is
> correct cause look at the source code of the WLock() method, since i am
> using a Ticket spinlock with a proportional backoff on the writer side,
> the Ticket spinlock is using a "lock add" assembler instruction to
> increment a counter in the Enter() method of the ticket spinlock , and
> this "lock add" assembler instruction is a barrier for stores and loads
> on x86, and the stores of Fcount6^.fcount6 and FCount5^.fcount5
> are not reordred with the stores of the writer section, so the WLock()
> method is sequential consistent and correct, now look at the WUnlock() ,
> we don't need an "sfence" cause stores on WUnlock() are not reordered
> with older stores on x86 , so WUnlock() method is sequential consistent
> and correct, now look at the RLock() method, the loads inside RLock()
> method are not reordered with the loads of the reader section  ,  and on
> RUnlock(), the loads of RUnlock() are not reordered with older loads of
> the critical section , so all in all my algorithm i think my algorithm


I mean here "reader section" , not critical section.

> is sequential consistent and correct on x86. So be confident cause i
> have reasoned correctly and i think my algorithm is correct and it is a
> powerful synchronization mechanism that can replace RCU and that can
> replace Seqlock cause it beats Seqlock.
>
>
> So this was my proof that my algorithm is correct.
>
> You can download my scalable distributed sequential lock version 1.11 from:
>
> https://sites.google.com/site/aminer68/scalable-distributed-sequential-lock
>
>
> Read this about my scalable distributed sequential lock:
>
>
> Disclaimer:
>
> My software is provided on an "as-is" basis, with no warranties,
> express or implied.  The entire risk and liability of using it is yours.
> Any damages resulting from the use or misuse of this software will be
> the responsibility of the user.
>
>
>
> Thank you,
> Amine Moulay Ramdane.

[toc] | [prev] | [standalone]

Back to top | Article view | comp.programming.threads

csiph-web