Abstract
Verifying the correctness of executions of concurrent and distributed programs is difficult because they show nondeterministic behavior due to different process scheduling order. Predicate detection can alleviate this problem by predicting whether the userspecified condition (predicate) could have become true in any global state of the given concurrent or distributed computation. The method is predictive because it generates inferred global states from the observed execution path and then checks if those global states satisfy the predicate. An important part of the predicate detection method is global states enumeration, which generates the consistent global states, including the inferred ones, of the given computation. Cooper and Marzullo gave the first enumeration algorithm based on a breadth first strategy (BFS). Later, many algorithms have been proposed to improve the space and time complexity. Among the existing algorithms, the Tree algorithm due to Jegou et al. has the smallest time complexity and requires O(P) space, which is linear to the size of the computation P. In this paper, we present a fast algorithm, QuickLex, to enumerate global states in the lexical order. QuickLex requires much smaller space than O(P). From our experiments, the Tree algorithm requires 210 times more memory space than QuickLex. Moreover, QuickLex is 4 times faster than Tree even though the asymptotic time complexity of QuickLex is higher than that of Tree. The reason is that the worst case time complexity of QuickLex happens only in computations that are not common in practice. Moreover, Tree is built on linkedlists and QuickLex can be implemented using integer arrays. In comparison with the existing lexical algorithm (Lex), QuickLex is 7 times faster and uses almost the same amount of memory as Lex. Finally, we implement a parallelandonline predicate detector for concurrent programs using QuickLex, which can detect data races and violation of invariants in the programs.
BibTeX  Entry
@InProceedings{chang_et_al:LIPIcs:2016:6614,
author = {YenJung Chang and Vijay K. Garg},
title = {{QuickLex: A Fast Algorithm for Consistent Global States Enumeration of Distributed Computations}},
booktitle = {19th International Conference on Principles of Distributed Systems (OPODIS 2015)},
pages = {117},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897989},
ISSN = {18688969},
year = {2016},
volume = {46},
editor = {Emmanuelle Anceaume and Christian Cachin and Maria PotopButucaru},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6614},
URN = {urn:nbn:de:0030drops66142},
doi = {10.4230/LIPIcs.OPODIS.2015.25},
annote = {Keywords: consistent global state, algorithm, computation}
}
Keywords: 

consistent global state, algorithm, computation 
Collection: 

19th International Conference on Principles of Distributed Systems (OPODIS 2015) 
Issue Date: 

2016 
Date of publication: 

13.10.2016 