×

zbMATH — the first resource for mathematics

A compiler for MSVL and its applications. (English) Zbl 1407.68096
Summary: In this paper, we present a method for implementing a compiler called MC for Modeling, Simulation and Verification Language (MSVL) based on LLVM. MC accepts a well formed MSVL program as input and generates an executable binary code. Different from other compilers, MC can be used not only to compile programs but also to model and verify programs. The details of implementation including the architecture design, lexical, syntactic and semantic analysis, as well as preprocessing and scheduling algorithms. Besides, we show MC can be utilized as an infrastructure for Artificial Intelligence (AI) planning. Several examples are given to show applications of MC in modeling and verifying programs, as well as AI planning.

MSC:
68N20 Theory of compilers and interpreters
68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
SHOP2; CBMC; SPIN; NuSMV; LLVM; BLAST; RiTHM; JPAX
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Dahl, O.-J.; Dijkstra, E. W.; Hoare, C. A.R., Structured Programming, (1972), Academic Press Ltd. · Zbl 0267.68001
[2] Hoare, T.; Misra, J., Verified software: theories, tools, experiments vision of a grand challenge project, (Working Conference on Verified Software: Theories, Tools, and Experiments, (2005), Springer), 1-18
[3] Clarke, E. M.; Grumberg, O.; Long, D. E., Model checking and abstraction, ACM Trans. Program. Lang. Syst., 16, 5, 1512-1542, (1994)
[4] Clarke, E. M.; Grumberg, O.; Peled, D., Model Checking, (1999), MIT Press
[5] Holzmann, G. J., The model checker spin, IEEE Trans. Softw. Eng., 23, 5, 279-295, (1997)
[6] Cimatti, A.; Clarke, E.; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A., NUSMV 2: an opensource tool for symbolic model checking, (International Conference on Computer Aided Verification, (2002), Springer), 359-364 · Zbl 1010.68766
[7] Pnueli, A., The temporal logic of programs, (18th Annual Symposium on Foundations of Computer Science, (1977), IEEE), 46-57
[8] Clarke, E. M.; Emerson, E. A.; Sistla, A. P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst., 8, 2, 244-263, (1986) · Zbl 0591.68027
[9] Vorobyov, K.; Krishnan, P., Comparing model checking and static program analysis: a case study in error detection approaches, (Proc. SSV, (2010)), 1-7
[10] Ball, T.; Cook, B.; Levin, V.; Rajamani, S. K., Slam and static driver verifier: technology transfer of formal methods inside Microsoft, (Integrated Formal Methods, (2004), Springer), 1-20
[11] D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, The software model checker blast: applications to software engineering. · Zbl 1104.68408
[12] Henzinger, T. A.; Jhala, R.; Majumdar, R.; Sutre, G., Software verification with blast, (Model Checking Software, (2003), Springer), 235-239 · Zbl 1023.68532
[13] Clarke, E.; Kroening, D.; Lerda, F., A tool for checking ANSI-C programs, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (2004), Springer), 168-176 · Zbl 1126.68470
[14] Kroening, D.; Tautschnig, M., CBMC-C bounded model checker, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (2014), Springer), 389-391
[15] Dietsch, D.; Heizmann, M.; Langenfeld, V.; Podelski, A., Fairness modulo theory: a new approach to ltl software model checking, (International Conference on Computer Aided Verification, (2015), Springer), 49-66 · Zbl 1381.68157
[16] Brockschmidt, M.; Cook, B.; Ishtiaq, S.; Khlaaf, H.; Piterman, N., T2: temporal property verification, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (2016), Springer), 387-393
[17] Havelund, K.; Roşu, G., Monitoring Java programs with Java PathExplorer, Electron. Notes Theor. Comput. Sci., 55, 2, 200-217, (2001)
[18] Navabpour, S.; Joshi, Y.; Wu, W.; Berkovich, S.; Medhat, R.; Bonakdarpour, B.; Fischmeister, S., RITHM: a tool for enabling time-triggered runtime verification for C programs, (Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, (2013), ACM), 603-606
[19] Duan, Z., Temporal Logic and Temporal Logic Programming, (2005), Science Press
[20] Duan, Z., An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming, (1996), University of Newcastle upon Tyne, Ph.D. thesis
[21] Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic with infinite models, Acta Inform., 45, 1, 43-78, (2008) · Zbl 1141.68039
[22] Duan, Z.-H.; Koutny, M., A framed temporal logic programming language, J. Comput. Sci. Tech., 19, 3, 341-351, (2004)
[23] Duan, Z.; Tian, C., A unified model checking approach with projection temporal logic, (Formal Methods and Software Engineering, (2008), Springer), 167-186
[24] Zhang, N.; Duan, Z.; Tian, C., Model checking concurrent systems with MSVL, Sci. China Inf. Sci., 59, 11, (2016)
[25] Ma, Y.; Duan, Z.; Wang, X.; Yang, X., An interpreter for framed tempura and its application, (First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE’07, (2007), IEEE), 251-260
[26] Lattner, C.; Adve Llvm, V., A compilation framework for lifelong program analysis & transformation, (International Symposium on Code Generation and Optimization. International Symposium on Code Generation and Optimization, CGO 2004, (2004), IEEE), 75-86
[27] Lattner, C. A., LLVM: an Infrastructure for Multi-Stage Optimization, (2002), University of Illinois at Urbana-Champaign, Ph.D. thesis
[28] Wang, X.; Duan, Z.; Zhao, L., Formalizing and implementing types in MSVL, (International Workshop on Structured Object-Oriented Formal Language and Method, (2013), Springer), 62-75
[29] Zhang, N.; Duan, Z.; Tian, C., Extending MSVL with function calls, (International Conference on Formal Engineering Methods, (2014), Springer), 446-458
[30] Zhang, N.; Duan, Z.; Tian, C., A mechanism of function calls in MSVL, Theoret. Comput. Sci., 654, 11-25, (2016) · Zbl 1353.68184
[31] Zhang, N.; Duan, Z.; Tian, C., A cylinder computation model for many-core parallel computing, Theoret. Comput. Sci., 497, 68-83, (2013) · Zbl 1416.68074
[32] Mo, D.; Wang, X.; Duan, Z., Asynchronous communication in MSVL, (International Conference on Formal Engineering Methods, (2011), Springer), 82-97
[33] Brooks, D.; Martonosi, M., Dynamic thermal management for high-performance microprocessors, (The Seventh International Symposium on High-Performance Computer Architecture. The Seventh International Symposium on High-Performance Computer Architecture, HPCA, (2001), IEEE), 171-182
[34] Coskun, A. K.; Ayala, J. L.; Atienza, D.; Rosing, T. S.; Leblebici, Y., Dynamic thermal management in 3d multicore architectures, (Design, Automation & Test in Europe Conference & Exhibition. Design, Automation & Test in Europe Conference & Exhibition, DATE’09, (2009), IEEE), 1410-1415
[35] Yang, J.; Zhou, X.; Chrobak, M.; Zhang, Y.; Jin, L., Dynamic thermal management through task scheduling, (IEEE International Symposium on Performance Analysis of Systems and Software. IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS 2008, (2008), IEEE), 191-201
[36] Heo, S.; Barr, K.; Asanović, K., Reducing power density through activity migration, (Proceedings of the 2003 International Symposium on Low Power Electronics and Design. Proceedings of the 2003 International Symposium on Low Power Electronics and Design, ISLPED’03, (2003), IEEE), 217-222
[37] Sharma, R. K.; Bash, C. E.; Patel, C. D.; Friedrich, R. J.; Chase, J. S., Balance of power: dynamic thermal management for Internet data centers, IEEE Internet Comput., 9, 1, 42-49, (2005)
[38] Salami, B.; Baharani, M.; Noori, H., Proactive task migration with a self-adjusting migration threshold for dynamic thermal management of multi-core processors, J. Supercomput., 68, 3, 1068-1087, (2014)
[39] Ebi, T.; Faruque, M.; Henkel Tape, J., Thermal-aware agent-based power econom multi/many-core architectures, (IEEE/ACM International Conference on Computer-Aided Design-Digest of Technical Papers. IEEE/ACM International Conference on Computer-Aided Design-Digest of Technical Papers, ICCAD 2009, (2009), IEEE), 302-309
[40] Skadron, K.; Stan, M. R.; Huang, W.; Velusamy, S.; Sankaranarayanan, K.; Tarjan, D., Temperature-aware microarchitecture, Comput. Archit. News, 31, 2, 2-13, (2003)
[41] Yeo, I.; Liu, C. C.; Kim, E. J., Predictive dynamic thermal management for multicore systems, (Proceedings of the 45th Annual Design Automation Conference, (2008), ACM), 734-739
[42] Donald, J.; Martonosi, M., Techniques for Multicore Thermal Management: Classification and New Exploration, Comput. Archit. News, vol. 34, 78-88, (2006), IEEE Computer Society
[43] Ebi, T.; Kramer, D.; Karl, W.; Henkel, J., Economic learning for thermal-aware power budgeting in many-core architectures, (Proceedings of the 9th International Conference on Hardware/Software Codesign and System Synthesis. Proceedings of the 9th International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS, (2011), IEEE), 189-196
[44] Mayer, M. C.; Limongelli, C.; Orlandini, A.; Poggioni, V., Linear temporal logic as an executable semantics for planning languages, J. Log. Lang. Inf., 16, 1, 63-89, (2007) · Zbl 1159.68562
[45] Huang, Y.-C.; Selman, B.; Kautz, H., Control knowledge in planning: benefits and tradeoffs, (AAAI/IAAI, (1999)), 511-517
[46] Bacchus, F.; Kabanza, F., Using temporal logics to express search control knowledge for planning, Artificial Intelligence, 116, 1, 123-191, (2000) · Zbl 0939.68827
[47] Kvarnström, J.; Doherty, P., TALplanner: a temporal logic based forward chaining planner, Ann. Math. Artif. Intell., 30, 1-4, 119-169, (2000) · Zbl 1002.68158
[48] Nau, D. S.; Au, T.-C.; Ilghami, O.; Kuter, U.; Murdock, J. W.; Wu, D.; Yaman, F., SHOP2: an HTN planning system, J. Artificial Intelligence Res., 20, 379-404, (2003) · Zbl 1058.68106
[49] Xie, F.; Müller, M.; Holte, R., Jasper: the art of exploration in greedy best first search, (The Eighth International Planning Competition. The Eighth International Planning Competition, IPC-2014, (2014)), 39-42
[50] Seipp, J.; Braun, M.; Garimort, J.; Helmert, M., Learning portfolios of automatically tuned planners, (ICAPS, (2012))
[51] R. Valenzano, H. Nakhost, M. Müller, J. Schaeffer, N. Sturtevant, Arvandherd 2014, The Eighth International Planning Competition, Description of Participant Planners of the Deterministic Track.
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.