[lnkForumImage]
TotalShareware - Download Free Software
Confronta i prezzi di migliaia di prodotti.
Asp Forum
 Home | Login | Register | Search 


 

Forums >

comp.programming.threads

Here is my proof

Ramine

12/7/2014 7:20:00 PM

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-seque...



Thank you,
Amine Moulay Ramdane.
2 Answers

Ramine

12/7/2014 7:30:00 PM

0


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

Ramine

12/7/2014 7:37:00 PM

0

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-seque...
>
>
>
> Thank you,
> Amine Moulay Ramdane.
>