×

zbMATH — the first resource for mathematics

Genetic programming and model checking: Synthesizing new mutual exclusion algorithms. (English) Zbl 1183.68376
Cha, Sungdeok (Steve) (ed.) et al., Automated technology for verification and analysis. 6th international symposium, ATVA 2008, Seoul, Korea, October 20–23, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-88386-9/pbk). Lecture Notes in Computer Science 5311, 33-47 (2008).
Summary: Recently, genetic programming and model checking were combined for synthesizing algorithms that satisfy a given specification. In particular, we demonstrated this approach by developing a tool that was able to rediscover the classical mutual exclusion algorithms [G. Katz and D. Peled, “Model checking-based genetic programming with an application to mutual exclusion”, Lect. Notes Comput. Sci. 4963, 141–156 (2008; Zbl 1134.68411)] with two or three global bits. In this paper we extend the capabilities of the model checking-based genetic programming and the tool built to experiment with this approach. In particular, we add qualitative requirements involving locality of variables and checks, which are typical of realistic mutual exclusion algorithms. The genetic process mimics the actual development of mutual exclusion algorithms, by starting with an existing correct solution, which does not satisfy some performance requirements, and converging into a solution that satisfies these requirements. We demonstrate this by presenting some nontrivial new mutual exclusion algorithms, discovered with our tool.
For the entire collection see [Zbl 1148.68001].
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
CESAR; MCGP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: ICALP, pp. 169–181 (1980) · Zbl 0456.68016 · doi:10.1007/3-540-10003-2_69
[2] Floyd, R.: Assigning meaning to programs. In: American Mathematical Society symposium on Applied Mathematics, vol. 19, pp. 19–31 (1967) · doi:10.1090/psapm/019/0235771
[3] Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification testing and Verification, pp. 3–18 (1995)
[4] Hoare, C.A.R.: An axiomatic basis for computer programming. Communication of the ACM 12, 576–583 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[5] Holland, J.H.: Adaptation in Natural and Artificial Systems: An Introductory Analysis with Applications to Biology, Control and Artificial Intelligence. MIT Press, Cambridge (1992)
[6] Johnson, C.G.: Genetic programming with fitness based on model checking. In: Ebner, M., O’Neill, M., Ekárt, A., Vanneschi, L., Esparcia-Alcázar, A.I. (eds.) EuroGP 2007. LNCS, vol. 4445, pp. 114–124. Springer, Heidelberg (2007) · doi:10.1007/978-3-540-71605-1_11
[7] Katz, G., Peled, D.: Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 141–156. Springer, Heidelberg (2008) · Zbl 1134.68411 · doi:10.1007/978-3-540-78800-3_11
[8] Kessels, J.L.W.: Arbitration without common modifiable variables. Acta Inf. 17, 135–141 (1982) · Zbl 0468.90006 · doi:10.1007/BF00288966
[9] Kirkpatrick Jr., S., Vecchi, M.P.: Optimization by simulated annealing. Science 220(4598), 671–680 (1983) · Zbl 1225.90162 · doi:10.1126/science.220.4598.671
[10] Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge (1992) · Zbl 0850.68161
[11] Koza, J.R.: Genetic Programming II: Automatic Discovery of Reusable Programs. MIT Press, Cambridge (1994) · Zbl 0850.68160
[12] Kupferman, O., Vardi, M.: Memoryfull branching-time logic. In: Logic in Computer Science, pp. 265–274 (2006)
[13] Montana, D.J.: Strongly typed genetic programming. Evolutionary Computation 3(2), 199–230 (1995) · Zbl 05412779 · doi:10.1162/evco.1995.3.2.199
[14] Niebert, P., Peled, D., Pnueli, A.: Discriminative model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 504–516. Springer, Heidelberg (2008) · Zbl 1155.68444 · doi:10.1007/978-3-540-70545-1_48
[15] Peterson, F.: Economical solutions to the critical section problem in a distributed system. In: STOC: ACM Symposium on Theory of Computing (STOC) (1977)
[16] Pnueli, A., Rosner, R.: On the synthesis of reactive systems. In: POPL, Austin, Texas, pp. 179–190 (1989) · Zbl 0686.68015
[17] Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: 5th International Symposium on Programming, pp. 337–350 (1981)
[18] Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972) · Zbl 0251.05107 · doi:10.1137/0201010
[19] Taubenfeld, G.: Synchronization Algorithms and Concurrent Programming. Prentice-Hall, Inc., Upper Saddle River (2006)
[20] Tsay, Y.K.: Deriving a scalable algorithm for mutual exclusion. In: Kutten, S. (ed.) DISC 1998. LNCS, vol. 1499, pp. 393–407. Springer, Heidelberg (1998) · doi:10.1007/BFb0056497
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.