Here is my proof again

[Ramine]

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.

[Ramine]

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