A case study on the lightweight verification of a multi-threaded task server

摘要

We present a case study on the verification of the design of a commercial multi-threaded task server (MTTS), developed by the Novabase company, used for massively parallelizing computational tasks. In a first stage, we employed the Plural tool, which is designed to perform lightweight verification of Java programs using a data-flow analysis (DFA) framework, to specify and verify the MTTS. We wrote the Plural specification for the MTTS based on the code developed by Novabase, its informal documentation, and our discussions with Novabase engineers, who validated our understanding of the MTTS application. The Plural specification language is based on typestates and access permissions. In a second stage, we developed the Pulse tool, which enhances the analysis performed by Plural, and used the tool on the MTTS specifications. Pulse translates Plural specifications into an abstract state-machine model that captures the semantics of all the possible concurrent programs implementing the given specifications, and uses the evmdd-smc symbolic model checker to verify the machine model. The experimental results on the MTTS specification show that the exhaustive model-checking approach scales reasonably well and is efficient at finding errors in specifications that were not previously detected with the data-flow analysis (DFA) capabilities of Plural.