An Automatic Parameterized Verification of FLASH Cache Coherence Protocol

摘要

FLASH protocol is an industrial-scale cache coherence protocol, which is a challenging benchmark in the formal verification area. Verifying such protocol yields both scientific and commercial values. However, the complicated mechanism of protocols and the explosive searching states make it extremely hard to solve. An alternative solution is to carry out proof scripts combining manual work with a computer, which is adopted by most works in this area. However, this alternation makes the verification process neither effective nor rigorous. Therefore, in this paper, we elaborate the detailed process of how paraVerifier generates formal proofs automatically. It can generate a formal proof without manual works, and guarantee the rigorous correctness at the same time. Furthermore, we also illustrate the flow chart of READ and WRITE transactions in FLASH protocol, and analyze the semantics hiding behind the auto-searched invariants. We show that paraVerifier can not only automatically generate formal proofs, but offer comprehensive analyzing reports for better understanding.