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

Groups > comp.programming.threads > #2754

Re: Here is my proof again

Show all headers | View raw

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.

Back to comp.programming.threads | Previous | Next — Previous in thread | Find similar | Unroll thread

Thread

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

csiph-web