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

Groups > comp.programming.threads > #2750

Here is my proof

Show all headers | View raw

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.

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

Thread

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

csiph-web