The problem of pairwise CFL-reachability is to decide whether two given program locations in different threads are simultaneously reachable in the presence of recursion in threads and scheduling constraints imposed by synchronization primitives. Pairwise CFL-reachability is the core problem underlying concurrent program analysis especially dataflow analysis. Unfortunately, it is undecidable even for the most commonly used synchronization primitive, i.e., mutex locks. Lock usage in concurrent programs can be characterized in terms of lock chains, where a sequence of mutex locks is said to be chained if the scopes of adjacent (non-nested) mutexes overlap. Although pairwise reachability is known to decidable for threads interacting via nested locks, i.e., chains of length one, these techniques donpsilat extend to programs with non-nested locks used in crucial applications like databases and device drivers. In this paper, we exploit the fact that lock usage patterns in real life programs do not produce unbounded lock chains. For such programs, we show that pairwise CFL-reachability becomes decidable. Our new results narrow the decidability gap for pairwise CFL-reachability by providing a more refined characterization for it in terms of boundedness of lock chains rather than the current state-of-the-art, i.e., nestedness of locks (chains of length one).

A large number of industrial concurrent programs are being designed based on a model which combines threads with event-based communication. These programs consist of several threads which perform computation by dispatching tasks to other threads via asynchronous function calls. These asynchronous function calls are implemented using function objects, which are essentially wrappers containing a pointer to the function that should be executed on a particular thread with the corresponding arguments. In many cases, the arguments, in turn, contain function objects which serve as callbacks. Verifying such programs which involves reasoning about complex concurrency constructs comprising function pointers and callback functions is extremely tricky especially in the presence of recursion. In this paper, we present a fast and accurate static data race detection technique for multi-threaded C programs with asynchronous function calls and demonstrate its application to real-life software.

Dataflow analysis for concurrent programs is a problem of critical importance but, unfortunately, also an undecidable one. A key obstacle is to determine precisely how dataflow facts at a location in a given thread could be affected by operations of other threads.This problem, in turn, boils down to pairwise reachability, i.e., given program locations c1and c2in two threads T1and T2, respectively, determining whether c1 and c2 are simultaneously reachable in the presence of constraints imposed by synchronization primitives. Unfortunately, pairwise reachability is undecidable for most synchronization primitives. However, we leverage the surprising result that the closely related problem of parameterized pairwise reachability of c1and c2, i.e., whether for some n1and n2, c1and c2are simultaneously reachable in the program T1n1||T2n2comprised of n1copies of T1and n2copies of T2,is not only decidable for many primitives, but efficiently so. Although parameterization makes pairwise reachability tractable it may over-approximate the set of pairwise reachable locations and can, therefore, be looked upon as an abstraction technique.Where as abstract interpretation is used for control and data abstractions, we propose the use of parameterization as an abstraction for concurrency. Leveraging abstract interpretation in conjunction with parameterization allows us to lift two desirable properties of sequential dataflow analysis to the concurrent domain, i.e., precision and scalability.

We propose a framework for improving both the scalability as well as the accuracy of pointer alias analysis, irrespective of its flow or context-sensitivities, by leveraging a three-pronged strategy that effectively combines divide and conquer, parallelization and function summarization. A key step in our approach is to first identify small subsets of pointers such that the problem of computing aliases of any pointer can be reduced to computing them in these small subsets instead of the entire program. In order to identify these subsets, we first apply a series of increasingly accurate but highly scalable (context and flow-insensitive) alias analyses in a cascaded fashion such that each analysis Ai works on the subsets generated by the previous one Ai-1. Restricting the application of Ai to subsets generated by Ai-1, instead of the entire program, improves it scalability, i.e., Ai is bootstrapped by Ai-1. Once these small subsets have been computed, in order to make our overall analysis accurate, we employ our new summarization-based flow and context-sensitive alias analysis. The small size of each subset offsets the higher computational complexity of the context-sensitive analysis. An important feature of our framework is that the analysis for each of the subsets can be carried out independently of others thereby allowing us to leverage parallelization further improving scalability.

In this paper, we propose a new technique for the verification of concurrent multi-threaded programs. In general, the problem is known to be undecidable even for programs with just two threads. However, we exploit the observation that, in practice, a large fraction of concurrent programs can either be modeled as pushdown systems communicating solely using locks or can be reduced to such systems by applying standard abstract interpretation techniques or by exploiting separation of data from control. Moreover, standard programming practice guidelines typically recommend that programs use locks in a nested fashion. In fact, in languages like Java and C#, locks are guaranteed to be nested. For such a framework, we show, by using the new concept of Lock Constrained Multi-Automata Pair (LMAP), that pre*-closures of regular sets of states can be computed efficiently. This is accomplished by reducing the pre*-closure computation for a regular set of states of a concurrent program with nested locks to those for its individual threads. Leveraging this new technique then allows us to formulate a fully automatic, efficient and exact (sound and complete) decision procedure for model checking threads communicating via nested locks for indexed linear-time temporal logic formulae

With the success of formal verification techniques like equivalence checking and model checking for hardware designs, there has been growing interest in applying such techniques for formal analysis and automatic verification of software programs. This paper provides a brief tutorial on model checking of C programs. The essential approach is to model the semantics of C programs in the form of finite state systems by using suitable abstractions. The use of abstractions is key, both for modeling programs as finite state systems and for reducing the model sizes in order to manage verification complexity. We provide illustrative details of a verification platform called F-Soft, which provides a range of abstractions for modeling software, and uses customized SAT-based and BDD-based model checking techniques targeted for software.

The parameterized model checking problem (PMCP) is to decide whether a temporal property holds for a uniform family of systems, C||U/sup n/, comprised of a control process, C, and finitely, but arbitrarily, many copies of a user process, U, executing concurrently with interleaving semantics. We delineate the decidability/undecidability boundary of the PMCP for all possible systems that arise by letting processes coordinate using different subsets of the following communication primitives: conjunctive Boolean guards, disjunctive Boolean guards, pairwise rendezvous, asynchronous rendezvous and broadcast actions. Our focus is on the following linear time properties: (p1) LTL/spl bsol/X formulae over C; (p2) LTL formulae over C; (p3) regular properties specified as regular automata; and (p4) /spl omega/-regular automata. We also establish a hierarchy based on the relative expressive power of the primitives by showing that disjunctive guards and pairwise rendezvous are equally expressive, in that we can reduce the PMCP for regular and /spl omega/-regular properties for systems with disjunctive guards and pairwise rendezvous are equally expressive, in that we can reduce the PMCP for regular and /spl omega/-regular properties for systems with disjunctive guards to ones with pairwise rendezvous and vise versa, but that each of asynchronous rendezvous and broadcasts is strictly more expressive than pairwise rendezvous (and disjunctive guards). Moreover, for systems with conjunctive guards, we give a simple characterization of the decidability/undecidability boundary of the PMCP by showing that allowing stuttering sensitive properties bridges the gap between decidability (for p1) and undecidability (for p2). A broad framework for modeling snoopy cache protocols is also presented for which the PMCP for p3 is decidable and that can model all snoopy cache protocols given by Culler and Emerson (1988) thereby overcoming the undecidability results.