A general method for rendering static analyses for diverse concurrency models modular

• Published in: The Journal of systems and software 2019-01, Vol.147, p.17-45
• Main Authors: Stiévenart, Quentin, Nicolay, Jens, Meuter, Wolfgang De, Roover, Coen De
• Format: Article
• Language: English
• Subjects: Actors; Concurrency; Modular analysis; Static analysis; Threads
• ISSN: 0164-1212; 1873-1228
• DOI: 10.1016/j.jss.2018.10.001

•A discussion of the limitations of static analysis techniques for concurrent programs.•A general method for building scalable modular analysis of concurrent programs.•The application of this method to actors and to threads.•A theoretical and empirical evaluation of the resulting analyses.•A new benchmark suite for evaluating static analysis of multi-threaded applications. Shared-memory multi-threading and the actor model both share the notion of processes featuring communication, respectively by modifying shared state and by sending messages. Existing static analyses for concurrent programs either model every possible process interleavings and therefore suffer from the state explosion problem, or feature modularity but lack in precision or in their support for dynamic processes. In this paper we present a general method for obtaining a scalable analysis of concurrent programs featuring dynamic process creation. Our ModConc method transforms an abstract concurrent semantics modeling processes and communication into a modular static analysis treating the behavior of processes separately from their communication. We present ModConc in a generic way and demonstrate its applicability by instantiating it for multi-threaded and actor-based programs. The resulting analyses are evaluated in terms of precision, performance, scalability, and soundness. While a typical non-modular static analysis time out on half of our 56 benchmarks with a 30 min timeout, ModConc analyses successfully analyze all of them in less than 30 s, while remaining on par in terms of precision. Analyzing concurrent processes in isolation while modeling their communications is the key ingredient in supporting scalable analysis of concurrent programs featuring dynamic process communication.