Predicate detection for parallel computations

One of the fundamental problems in runtime verification of parallel program is to check if a predicate could become true in any global state of the system. The problem is challenging because of the nondeterministic process or thread scheduling of the system. Predicate detection alleviates this problem by analyzing the computation of the program and predicting whether the predicate could become true by exercising an alternative process schedule. The technique was first introduced by Cooper et al. and Garg et al. for distributed debugging. Later, jPredictor applies this technique for concurrent debugging. We improve the technique of predicate detection in three ways. The first part of this dissertation presents the first online-and-parallel predicate detector for general-purpose predicate detection, named ParaMount. ParaMount partitions the set of consistent global states and each subset can be enumerated in parallel using existing sequential enumeration algorithms. Our experimental results show that ParaMount speeds up the existing sequential algorithms by a factor of 6 with 8 threads. Moreover, Paramount can run along with the execution of users’ program and hence it is applicable even to non-terminating programs. The second part develops a fast enumeration algorithm, named QuickLex, for consistent global states. In comparison with the original lexical algorithm (Lex), QuickLex uses an additional O(n2) space to reduce the time complexity from O(n2) to O(n·∆(P)), where n is the number of processes or threads in the computation and ∆(P) is the maximal number of incoming edges of any event. The third part introduces Loset — a new model for parallel computations with locking constraints. We show that the reachability problem in a loset is NP-complete. To tackle the NP-completeness, we present several useful properties. Specifically, if the final global state is reachable, then all lock-free feasible global states are reachable. In addition, we show that the reachability of a global state G can be determined using a sub-computation instead of the entire computation. Moreover, we introduce the strong feasibility of a global state, which is an upper approximation of reachability that can be calculated efficiently. Our experiments show that the property accurately models the reachability for all 11 benchmarks.Electrical and Computer Engineerin