×

A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring. (English) Zbl 1435.68196

Summary: Runtime verification aims at extracting information from a running system, and using it to detect and possibly react to behaviors violating a given correctness property. Decentralized runtime verification involves a set of monitors observing the behavior of the underlying system. When the monitors themselves can fail, and communication among them is unreliable, it is unavoidable that the monitors may have different views of the system’s state and hence that they emit different opinions about its correctness at runtime. It is known that few correctness properties can be monitored in such a setting, when the set of opinions is the set \(\{\mathrm{True}, \mathrm{False}\}\). In this paper, we initiate the investigation of decentralized fault-tolerant runtime monitoring under an arbitrary set of opinions. Specifically, we characterize the size of the opinion set required for monitoring a given correctness property in a decentralized manner. It turns out that the key factor impacting this size is the maximum number of times the monitored property can change its truth value over all executions of the monitors. Our lower bound is independent of the way the set of opinions returned by the monitors is globally interpreted, and it holds even when verifying a static system. Moreover, our lower bound is tight in the sense that we design a distributed protocol enabling any given set of monitors to verify any given correctness property on static systems, using as many different opinions as the one given by our lower bound.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68M14 Distributed systems
68M15 Reliability, testing and fault tolerance of networks and computer systems
Full Text: DOI

References:

[1] Afek, Y.; Attiya, H.; Dolev, D.; Gafni, E.; Merritt, M.; Shavit, N., Atomic snapshots of shared memory, J. ACM, 40, 4, 873-890 (1993) · Zbl 0783.68029 · doi:10.1145/153724.153741
[2] Arafat, O., Bauer, A., Leucker, M., Schallhart, C.: Runtime verification revisited. Tech. Rep. TUM-I0518, Technischen Universität München (2005)
[3] Attiya, H.; Rajsbaum, S., The combinatorial structure of wait-free solvable tasks, SIAM J. Comput., 31, 4, 1286-1313 (2002) · Zbl 1015.68080 · doi:10.1137/S0097539797330689
[4] Attiya, H.; Welch, Jl, Distributed Computing: Fundamentals, Simulations and Advanced Topics (2004), Hoboken: Wiley, Hoboken
[5] Awerbuch, B., Varghese, G.: Distributed program checking: A paradigm for building self-stabilizing distributed protocols. In: 32nd IEEE Symposium on Foundations of Computer Science (FOCS), pp. 258-267 (1991). 10.1109/SFCS.1991.185377
[6] Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTC), LNCS, vol. 4337, pp. 260-272. Springer (2006) · Zbl 1177.68141
[7] Bauer, A.; Leucker, M.; Schallhart, C., Comparing LTL semantics for runtime verification, J. Log. Comput., 20, 3, 651-674 (2010) · Zbl 1213.68363 · doi:10.1093/logcom/exn075
[8] Giannakopoulou, Dimitra; Méry, Dominique, FM 2012: Formal Methods (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1250.68029
[9] Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: 27th IEEE International Symposium on Parallel and Distributed Processing (IPDPS), pp. 1025-1036 (2013). http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6569024
[10] Bonakdarpour, B., Fraigniaud, P., Rajsbaum, S., Rosenblueth, D.A., Travers, C.: Decentralized asynchronous crash-resilient runtime verification. In: 27th International Conference on Concurrency Theory (CONCUR), pp. 16:1-16:15. LIPIcs 59, Schloss Dagstuhl (2016) · Zbl 1392.68234
[11] Bonakdarpour, Borzoo; Fraigniaud, Pierre; Rajsbaum, Sergio; Travers, Corentin, Challenges in Fault-Tolerant Distributed Runtime Verification, Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 363-370 (2016), Cham: Springer International Publishing, Cham · Zbl 1392.68234
[12] Butler, Michael; Schulte, Wolfram, FM 2011: Formal Methods (2011), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1216.68024
[13] Bracho, J.; Montejano, L., The combinatorics of colored triangulations of manifolds, Geometriae Dedicata, 22, 3, 303-328 (1987) · Zbl 0631.57017 · doi:10.1007/BF00147939
[14] Abdulla, Parosh Aziz; Leino, K. Rustan M., Tools and Algorithms for the Construction and Analysis of Systems (2011), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1213.68016
[15] Chandy, Km; Lamport, L., Distributed snapshots: determining global states of distributed systems, ACM Trans. Comput. Syst., 3, 1, 63-75 (1985) · doi:10.1145/214451.214456
[16] Chauhan, H., Garg, V.K., Natarajan, A., Mittal, N.: A distributed abstraction algorithm for online predicate detection. In: 32nd IEEE Symposium on Reliable Distributed Systems (SRDS), pp. 101-110 (2013). http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6656126
[17] Cooper, R., Marzullo, K.: Consistent detection of global predicates. In: ACM Workshop on Parallel and Distributed Debugging, pp. 167-174 (1991). http://dl.acm.org/citation.cfm?id=122759
[18] Falcone, Y.; Fernandez, J.; Mounier, L., What can you verify and enforce at runtime?, Int. J. Softw. Tools Technol. Transf., 14, 3, 349-382 (2012) · doi:10.1007/s10009-011-0196-8
[19] Fischer, Mj; Lynch, Na; Paterson, Ms, Impossibility of distributed consensus with one faulty process, J. ACM, 32, 2, 374-382 (1985) · Zbl 0629.68027 · doi:10.1145/3149.214121
[20] Fraigniaud, P.; Korman, A.; Peleg, D., Towards a complexity theory for local distributed computing, J. ACM, 60, 5, 35 (2013) · Zbl 1281.68133 · doi:10.1145/2499228
[21] Fraigniaud, Pierre; Rajsbaum, Sergio; Roy, Matthieu; Travers, Corentin, The Opinion Number of Set-Agreement, Lecture Notes in Computer Science, 155-170 (2014), Cham: Springer International Publishing, Cham
[22] Fraigniaud, P.; Rajsbaum, S.; Travers, C., Locality and checkability in wait-free computing, Distrib. Comput., 26, 4, 223-242 (2013) · Zbl 1311.68026 · doi:10.1007/s00446-013-0188-x
[23] Fraigniaud, Pierre; Rajsbaum, Sergio; Travers, Corentin, Minimizing the Number of Opinions for Fault-Tolerant Distributed Decision Using Well-Quasi Orderings, LATIN 2016: Theoretical Informatics, 497-508 (2016), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1475.68205
[24] Genon, A., Massart, T., Meuter, C.: Monitoring distributed controllers: When an efficient LTL algorithm on sequences is needed to model-check traces. In: 14th International Symposium on Formal Methods (FM), LNCS, vol. 4085, pp. 557-572. Springer (2006)
[25] Ha, J., Arnold, M., Blackburn, S.M., McKinley, K.S.: A concurrent dynamic analysis framework for multicore hardware. In: 24th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 155-174. ACM (2009)
[26] Henle, M.: A Combinatorial Introduction to Topology. Dover (1983). http://store.doverpublications.com/0486679667.html#productdescription · Zbl 0527.55001
[27] Herlihy, M., Kozlov, D., Rajsbaum, S.: Distributed Computing Through Combinatorial Topology. Morgan Kaufmann-Elsevier (2013). http://store.elsevier.com/Distributed-Computing-Through-Combinatorial-Topology/Maurice-Herlihy/isbn-9780124045781/ · Zbl 1341.68004
[28] Herlihy, M., Rajsbaum, S., Tuttle, M.R.: Unifying synchronous and asynchronous message-passing models. In: 17th ACM symposium on Principles of distributed computing (PODC), pp. 133-142 (1998). 10.1145/277697.277722 · Zbl 1333.68061
[29] Herlihy, M.; Shavit, N., The topological structure of asynchronous computability, J. ACM, 46, 6, 858-923 (1999) · Zbl 1161.68469 · doi:10.1145/331524.331529
[30] Herlihy, M.; Shavit, N., The Art of Multiprocessor Programming (2008), San Francisco: Morgan Kaufmann Publishers Inc., San Francisco
[31] Kupferman, Orna; Y. Vardi, Moshe, Formal Methods in System Design, 19, 3, 291-314 (2001) · Zbl 0995.68061 · doi:10.1023/A:1011254632723
[32] Lynch, N., Distributed Algorithms (1996), Hoboken: Elsevier, Hoboken · Zbl 0877.68061
[33] Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: 29th IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 494-503 (2015)
[34] Raynal, M., Concurrent Programming—Algorithms, Principles, and Foundations (2013), Berlin: Springer, Berlin · Zbl 1276.68001
[35] Raynal, M., Distributed Algorithms for Message-Passing Systems (2013), Berlin: Springer, Berlin · Zbl 1282.68004
[36] Scheffel, T., Schmitz, M.: Three-valued asynchronous distributed runtime verification. In: 12th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 52-61 (2014). http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6950639
[37] Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: 26th IEEE International Conference on Software Engineering (ICSE), pp. 418-427 (2004). http://dl.acm.org/citation.cfm?id=998675
[38] Sen, K., Vardhan, A., Agha, G., Rosu, G.: Decentralized runtime analysis of multithreaded applications. In: 20th IEEE International Parallel and Distributed Processing Symposium (IPDPS) (2006). http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10917
[39] Zhu, H., Dwyer, M.B., Goddard, S.: Predictable runtime monitoring. In: 21st IEEE Euromicro Conference on Real-Time Systems, (ECRTS), pp. 173-183 (2009). http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5161487
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.