We present an automatic approach to detecting symmetry relations for general concurrent models. Despite the success of symmetry reduction in mitigating state explosion problem, one essential step towards its soundness and effectiveness, i.e., how to discover sufficient symmetries with least human efforts, is often either overlooked or oversimplified. In this work, we show how a concurrent model can be viewed as a constraint satisfaction problem (CSP), and present an algorithm capable of detecting symmetries arising from the CSP which induce automorphisms of the model. To the best of our knowledge, our method is the first approach that can automatically detect both process and data symmetries as demonstrated via a number of systems.

Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: (1) All executions of concurrent operations are serializable, and (2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on refinement checking of finite-state systems specified as concurrent processes with shared variables. To tackle state space explosion, we develop and apply symmetry reduction, dynamic partial order reduction, and a combination of both for refinement checking. We have built the method into the PAT model checker, and used PAT to automatically check a variety of implementations of concurrent objects, including the first algorithm for scalable nonzero indicators. Our system is able to find all known and injected bugs in these implementations.

Concurrent data structures are widely used but notoriously difficult to implement correctly. Linearizability is one main correctness criterion of concurrent data structure algorithms. It guarantees that a concurrent data structure appears as a sequential one to users. Unfortunately, linearizability is challenging to verify since a subtle bug may only manifest in a small portion of numerous thread interleavings. Model checking is therefore a potential primary candidate. However, current approaches of model checking linearizability suffer from severe state space explosion problem and are thus restricted in handling few threads and/or operations. This paper describes a scalable, fully automatic and general linearizability checking method based on [16] by incorporating symmetry and partial order reduction techniques. Our insights emerged from the observation that the similarity of threads using concurrent data structures causes model checking to generate large redundant equivalent portions of the state space, and the loose coupling of threads causes it to explore lots of unnecessary transition execution orders. We prove that symmetry reduction and partial order reduction can be combined in our approach and integrate them into the model checking algorithm. We demonstrate its efficiency using a number of real-world concurrent data structure algorithms.

It has been a common practice nowadays to employ third-party libraries in software projects. Software libraries encapsulate a large number of useful, well-tested and robust functions, so that they can help improve programmers' productivity and program quality. To interact with libraries, programmers only need to invoke Application Programming Interfaces (APIs) exported from libraries. However, programmers do not always use libraries as effectively as expected in their application development. One commonly observed phenomenon is that some library behaviors are re-implemented by client code. Such re-implementation, or imitation, is not just a waste of resource and energy, but its failure to abstract away similar code also tends to make software error-prone. In this paper, we propose a novel approach based on trace subsumption relation of data dependency graphs to detect imitations of library APIs for achieving better software maintainability. Furthermore, we have implemented a prototype of this approach and applied it to ten large real-world open-source projects. The experiments show 313 imitations of explicitly imported libraries with high precision average of 82%, and 116 imitations of static libraries with precision average of 75%.