Static and Dynamic Formal Analysis of Concurrent Systems and Languages: A Semantics-Based Approach

摘要

Concurrency is ubiquitous in modern software. The computing base of systems software, including operating systems and databases, has always been highly concurrent and with the introduction of language- level thread primitives in languages like Java and C# and the advent of distributed web services, concurrency has become commonplace even in application software. The design of concurrent software is notoriously error-prone due to the nondeterministic interaction among concurrently executing threads. Therefore, it is important to develop techniques for specifying correctness properties of concurrent software and tools for automatically checking these properties.A burning problem in program verification today is how to model the world of concurrent systems. The excellent models of sequential behavior that have evolved during the past thirty years of sequential program verification do not adequately reflect the nature of a concurrent universe. In this work, we present solutions to the commonly know problems of concurrency by using appropriate semantic models for concurrency, namely rewriting logic, and traces and Petri nets. We argue that using the appropriate semantic model helps one to define the problem in a simple, intuitive, and effective way in the first place, and then provides sound solutions for these now well-defined problems. This work addresses some verification problems for concurrent programs and systems. The approaches presented here fall into two main category of static versus dynamic verification.In the dynamic category, we use rewriting logic as a true concurrency model to specify concurrent programs and systems. We established the tool JavaFAN based on rewriting logic semantics of Java at both language and bytecode level. We provide a methodology in which formal semantics is then used as a basis to develop formal analyses tools (interpreter, model checker, and safety property checker) for analyzing programs in any language, in the case of JavaFAN tool for Java programs at both levels. We furthermore advanced these ideas by developing a generic partial order reduction module that with minimum effort can be added to any language specification and automatically enrich it with POR capabilities. We took this idea even further by providing reduction methods that can work on the specification of any concurrent system. Experimental result suggest that these methods are effective in practice, despite their generality and relative effortless implementations.In the static category, the focus of this work is to provide an appropriate notion of static abstraction for concurrent programs, called control net, based on Petri nets which captures the abstraction of program into a control only (no data) structure and at the same time captures the interaction mechanism of the threads and preserves the independence of their execution where applicable. This model is then used to show how two very important static analyses problems in the context of concurrency, namely atomicity and dataflow analyses can be cleanly defined for the program traces (partially-ordered runs) generated by the control net, and how clean algorithmic solutions can be provided to solve these problems. Experimental results suggest that these solutions are feasible in practice.