Modeling and analysis of the disruptor framework in CSP
Yucheng Fang, Huibiao Zhu, Frank Zeyda, Yuan Fei · 2018
The LMAX Disruptor is a high performance concurrency framework based on CAS (Compare And Swap). It has drawn huge interest from industry due to its efficiency; the LMAX business software using it can, for instance, handle up to six million orders per second. In this paper, we study the main principles and theories of Disruptor and apply the process algebra CSP (Communicating Sequential Process) to model it. Further, we use the model checker FDR (Failure Divergence Refinement) to automatically simulate the developed model, and verify whether the model is consistent with the specification and exhibits relevant secure properties like deadlock freedom, data race freedom and reading correctness. Our results show the correctness and safety of Disruptor in this respect.