Efficient abstraction algorithms for predicate detection.

*(English)*Zbl 1371.68180Summary: Analyzing a distributed computation is a hard problem in general due to the combinatorial explosion in the size of the state-space with the number of processes in the system. By abstracting the computation, unnecessary state explorations can be avoided. Computation slicing is an approach for abstracting distributed computations with respect to a given predicate. To detect a predicate in a timely manner during run-time verification, it is important to be able to compute the slice in an incremental manner as and when a new event is generated in the system. In this work, we present several online abstraction algorithms for computing the slice of a distributed computation with respect to regular predicates and its temporal extensions. The family of regular predicates is fairly rich and covers many commonly used predicates for run-time verification. We first present several online algorithms for computing the slice with respect to certain temporal logical regular predicates all of which are centralized. We then present a distributed algorithm for computing the slice with respect to a regular state based predicate; it distributes the work and storage requirements across the system, thus reducing the space and computation complexity per process. We also extend the slicing technique to non-regular predicates by presenting algorithms for computing the slice for two temporal logic operators when the predicate used in the operator is not regular.

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |

68W15 | Distributed algorithms |

68W27 | Online algorithms; streaming algorithms |

PDF
BibTeX
XML
Cite

\textit{A. Natarajan} et al., Theor. Comput. Sci. 688, 24--48 (2017; Zbl 1371.68180)

Full Text:
DOI

##### References:

[1] | Cooper, R.; Marzullo, K., Consistent detection of global predicates, (Proceedings of the ACM/ONR Workshop on Parallel and Distributed Debugging, Santa Cruz, California, USA, (1991)), 163-173 |

[2] | Tilera - tilepro processor |

[3] | Rotta, R.; Prescher, T.; Traue, J.; Nolte, J., In-memory communication mechanisms for many-cores—experiences with the intel SCC, (Proceedings of the TACC-Intel Highly Parallel Computing Symposium, TIHPCS, (2012)) |

[4] | Petrović, D.; Shahmirzadi, O.; Ropars, T.; Schiper, A., High-performance RMA-based broadcast on the intel SCC, (Proceedings of the ACM Symposium on Parallelism in Algorithms and Architectures, SPAA, (2012)), 121-130 |

[5] | Mittal, N.; Sen, A.; Garg, V. K., Solving computation slicing using predicate detection, IEEE Trans. Parallel Distrib. Syst., 18, 12, 1700-1713, (2007) |

[6] | Alagar, S.; Venkatesan, S., Techniques to tackle state explosion in global predicate detection, IEEE Trans. Softw. Eng., 27, 8, 704-714, (2001) |

[7] | Mittal, N.; Garg, V. K., Techniques and applications of computation slicing, Distrib. Comput., 17, 3, 251-277, (2005) · Zbl 1264.68030 |

[8] | Sen, A.; Garg, V. K., Formal verification of simulation traces using computation slicing, IEEE Trans. Comput., 56, 4, 511-527, (2007) · Zbl 1390.68438 |

[9] | Sen, A.; Garg, V. K., Detecting temporal logic predicates in the happened-before model, (Proceedings of the International Parallel and Distributed Processing Symposium, IPDPS, Florida, (2002)) |

[10] | Sen, A.; Garg, V. K., Detecting temporal logic predicates in distributed programs using computation slicing, (Proceedings of the International Conference on Principles of Distributed Systems, OPODIS, (2003)), 171-183 · Zbl 1078.68667 |

[11] | Ogale, V.; Garg, V., Detecting temporal logic predicates on distributed computations, (Proceedings of the Symposium on Distributed Computing, DISC, (2007)), 420-434 · Zbl 1145.68379 |

[12] | Garg, V. K., Elements of distributed computing, (2002), John Wiley and Sons, Incorporated New York, NY |

[13] | Clarke, E. M.; Grumberg, O.; Peled, D. A., Model checking, (2000), MIT Press |

[14] | Godefroid, P., Partial-order methods for the verification of concurrent systems, Lecture Notes in Computer Science, vol. 1032, (1996), Springer-Verlag · Zbl 1293.68005 |

[15] | Stoller, S. D.; Unnikrishnan, L.; Liu, Y. A., Efficient detection of global properties in distributed systems using partial-order methods, (Proceedings of the 12th International Conference on Computer-Aided Verification, CAV, (2000)), 264-279 · Zbl 0974.68501 |

[16] | Mittal, N.; Garg, V. K., Software fault tolerance of distributed programs using computation slicing, (Proceedings of the 23rd IEEE International Conference on Distributed Computing Systems, ICDCS, Providence, Rhode Island, (2003)), 105-113 |

[17] | Leucker, M.; Schallhart, C., A brief account of runtime verification, J. Log. Algebr. Program., 78, 5, 293-303, (2009) · Zbl 1192.68433 |

[18] | Drusinsky, D., The temporal rover and the ATG rover, (Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, London, UK, (2000)), 323-330 · Zbl 0976.68571 |

[19] | Kim, M. Z.; Viswanathan, M.; Kannan, S.; Lee, I.; Sokolsky, O., Java-mac: a run-time assurance approach for Java programs, Form. Methods Syst. Des., 24, 2, 129-155, (2004) · Zbl 1073.68552 |

[20] | Havelund, K.; Roşu, G., An overview of the runtime verification tool Java pathexplorer, Form. Methods Syst. Des., 24, 2, 189-215, (2004) · Zbl 1073.68549 |

[21] | Sen, K.; Roşu, G.; Agha, G., Detecting errors in multithreaded programs by generalized predictive analysis of executions, (Proceedings of the 7th IFIP Iinternational Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS, Athens, Greece, (2005)), 211-226 |

[22] | Chen, F.; Şerbănuţă, T. F.; Roşu, G., Jpredictor: a predictive runtime analysis tool for Java, (Proceedings of the 30th International Conference on Software Engineering, ICSE, Leipzig, Germany, (2008)), 221-230 |

[23] | Chen, F.; Roşu, G., Parametric and sliced causality, (2007), Department of Computer Science, University of Illinois at Urbana-Champaign, Tech. Rep. UIUCDCS-R-2007-2807 · Zbl 1135.68468 |

[24] | Sen, K.; Vardhan, A.; Agha, G.; Roşu, G., Efficient decentralized monitoring of safety in distributed systems, (Proceedings of the 26th International Conference on Software Engineering, ICSE, (2004)), 418-427 |

[25] | Bauer, A.; Falcone, Y., Decentralised LTL monitoring, (Proceedings of the 18th International Symposium on Formal Methods, FM, Paris, France, (2012)), 85-100 · Zbl 1372.68163 |

[26] | Scheffel, T.; Schmitz, M., Three-valued asynchronous distributed runtime verification, (Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE, (2014), IEEE), 52-61 |

[27] | Mostafa, M.; Bonakdarpour, B., Decentralized runtime verification of LTL specifications in distributed systems, (IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, Hyderabad, India, May 25-29, (2015)), 494-503 |

[28] | Lamport, L., Time, clocks, and the ordering of events in a distributed system, Commun. ACM, 21, 7, 558-565, (1978) · Zbl 0378.68027 |

[29] | Mattern, F., Virtual time and global states of distributed systems, (Parallel and Distributed Algorithms: Proceedings of the Workshop on Distributed Algorithms, WDAG, (1989)), 215-226 |

[30] | Fidge, C. J., Timestamps in message-passing systems that preserve the partial-ordering, (Raymond, K., Proceedings of the 11th Australian Computer Science Conference, ACSC, (1988)), 56-66 |

[31] | Mittal, N.; Garg, V. K., On detecting global predicates in distributed computations, (Proceedings of the 21st IEEE International Conference on Distributed Computing Systems, ICDCS, Phoenix, Arizona, USA, (2001)), 3-10 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.