Linearizability Of A Lock-Free Concurrent Skiplist

With the popularity of the Internet and cloud computing, massive data processing become increasingly important to IT professionals. Massive data processing methods often use concurrent programming, that multiple threads run simultaneously on multiple processors and share a common data area. The interaction of multiple threads leads to a more complicated procedure and unpredictable errors. Thus, to verify the correctness of a concurrent program by rigorous mathematical methods makes sense.Lock-free concurrent skiplist is a data structure that can be simultaneously accessed by multiple threads without any lock. It’s time complexity is logarithmic, just lick balanced tree, but don’t need rebalance operating. Lock-free concurrent skiplist is a ideal choice for massive data storage, but it’s correctness haven’t been formally verified.Linearizability is a correctness criterion for concurrent data structure. It means the fine-grained object implementation to have the same effect with an atomic operation. Based on the modular verification of linearizability with non-fixed linearization points, we verified the linearizability of lock-free concurrent skiplist.To verify the linearizability of lock-free concurrent skiplist, we makes the following contributions:· We first build a simple abstract machine and programming language, and produce the inference rules based on the syntax and semantics. Then, we programming with our new language model to implement the lock-free concurrent skiplist algorithm. At last, we design the abstract atomic operations on high-level.· We find the potential linearization point and add assistant statements to the code of the implementation.· We constructe the specification of the algorithm as invariant I, rely R and guarantee G based on LRG-logic.· Finally, for the first time, we verified the linarizability of the lock-free concurrent skiplist formally.