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

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

Here is my proof

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

Contents

  Here is my proof Ramine <ramine@1.1> - 2014-12-07 11:19 -0800
    Re: Here is my proof Ramine <ramine@1.1> - 2014-12-07 11:29 -0800
    Re: Here is my proof Ramine <ramine@1.1> - 2014-12-07 11:36 -0800

#2750 — Here is my proof

Hello,

I have wrote in my previous post this:

"Now i think my algorithm is correct."

You will say: "Amine in computer science we need proof, so
can you prove your algorithm is correct ?"


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 hanged
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, so the WLock() method is sequential consistent and correct, now 
look at the WUnlock() , we don't need an "sfence" cause stores are not 
reordered  with 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



Thank you,
Amine Moulay Ramdane.

[toc] | [next] | [standalone]

#2751

Hello,


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.

1

[toc] | [prev] | [next] | [standalone]

#2752

On 12/7/2014 11:19 AM, Ramine wrote:
> Hello,
>
> I have wrote in my previous post this:
>
> "Now i think my algorithm is correct."
>
> You will say: "Amine in computer science we need proof, so
> can you prove your algorithm is correct ?"
>
>
> 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 hanged

A typo: i mean "has changed", not "has hanged".


> 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, so the WLock() method is sequential consistent and correct, now
> look at the WUnlock() , we don't need an "sfence" cause stores are not
> reordered  with 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
>
>
>
> Thank you,
> Amine Moulay Ramdane.
>

[toc] | [prev] | [standalone]

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

csiph-web