@inproceedings{acf3f742af0743499bbc5b96d8fef4cf,
title = "Modeling and analysis of the disruptor framework in CSP",
abstract = "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.",
keywords = "CSP, Disruptor, FDR, Formal Modeling, Verification",
author = "Yucheng Fang and Huibiao Zhu and Frank Zeyda and Yuan Fei",
note = "Publisher Copyright: {\textcopyright} 2018 IEEE.; 8th IEEE Annual Computing and Communication Workshop and Conference, CCWC 2018 ; Conference date: 08-01-2018 Through 10-01-2018",
year = "2018",
month = feb,
day = "22",
doi = "10.1109/CCWC.2018.8301703",
language = "英语",
series = "2018 IEEE 8th Annual Computing and Communication Workshop and Conference, CCWC 2018",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "803--809",
editor = "Satyajit Chakrabarti and Saha, \{Himadri Nath\}",
booktitle = "2018 IEEE 8th Annual Computing and Communication Workshop and Conference, CCWC 2018",
address = "美国",
}