×

zbMATH — the first resource for mathematics

A cylinder computation model for many-core parallel computing. (English) Zbl 1416.68074
Summary: Many-core parallel computing and programming are new challenges to formal specification and verification. This paper presents a semantic model for many-core parallel computing systems so that the systems can be modeled and verified in a manageable way. The model is called Cylinder Computation Model (CCM) which is based on projection constructs in Projection Temporal Logic (PTL) and Modeling, Simulation and Verification Language (MSVL). To this end, the syntax and semantics of CCM are presented in detail. Further, some logic laws regarding CCM are given and the normal form of CCM programs is formalized and proved. Moreover, the operational semantics of CCM and an algorithm for implementing CCM programs within MSVL are also demonstrated. Finally, an example, simple word processor, is given to show how CCM works under MSVL paradigm.

MSC:
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
PNML
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Manna, Z., Temporal logic programming, Journal of Symbolic Computation, 8, 277-295, (1989) · Zbl 0691.03015
[2] Arden, D., Delayed-logic and finite-state machines, (Theory of Computing Machine Design, (1960), Univ. of Michigan Press), 1-35
[3] Hoare, C. A.R., Communicating sequential processes, Communications of the ACM, 21, 666-677, (1978) · Zbl 0383.68028
[4] Hoare, C. A.R., Communicating sequential processes, (1985), Prentice Hall International London · Zbl 0637.68007
[5] Milner, R., (A Calculus of Communicating systems, LNCS, vol 92, (1980), Springer-Verlag) · Zbl 0452.68027
[6] Milner, R., Communication and concurrency, (1989), Prentice Hall London · Zbl 0683.68008
[7] Duan, Z.; Koutny, M.; Holt, C., Projection in temporal logic programming, (Pfenning, F., Proceedings of Logic Programming and Automated Reasoning 1994, LNAI, vol. 822, (1994), Springer-Verlag), 333-334
[8] Duan, Z.; Zhang, N., A complete axiomatization of propositional projection temporal logic, (Proceedings of TASE 2008, (2008), IEEE Press New York), 271-278
[9] Duan, Z.; Yang, X.; Koutny, M., Semantics of framed temporal logic programs, (Proceedings of ICLP 2005, LNCS, vol. 3668, (2005), Springer-Verlag Barcelona), 256-270
[10] Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic, Acta Informatica, 45, 43-78, (2008) · Zbl 1141.68039
[11] Duan, Z., Temporal logic and temporal logic programming, (2005), Science Press Beijing
[12] Z. Duan, C. Tian, A unified model checking approach with projection temporal logic, in: Proceedings of ICFEM 2008, 2008, pp. 167-186.
[13] Duan, Z.; Yang, X.; Koutny, M., Frammed temporal logic programming, Science of Computer Programming, 70, 31-61, (2008) · Zbl 1131.68036
[14] Lamport, L., The temporal logic of actions, ACM Transactions on Programming Languages and Systems, 16, 872-923, (1994)
[15] Jensen, K.; Kristensen, L. M.; Wells, L., Coloured Petri nets and CPN tools for modelling and validation of concurrent systems, International Journal on Software Tools for Technology Transfer, 9, 213-254, (2007)
[16] Jensen, K., Coloured Petri nets: a high level language for system design and analysis, (Rozenberg, G., Advances in Petri Nets 1990, LNCS, vol. 483, (1991), Springer-Verlag), 342-416
[17] Koutney, M.; Pietkiewicz-Koutney, M., Synthesis of Petri nets with localities, Scientific Annals of Computer Science, 19, 1-23, (2009) · Zbl 1424.68107
[18] M. Koutney, A compositional model of timed petri nets, in: Proceedings of ICATPN 2000, 2000, pp. 303-322.
[19] J. Billington, S. Christensen, K. Hee, E. Kindler, O. Kummer, L. Petrucci, R. Post, C. Stehno, M. Weber, The petri net markup language: concepts, technology, and tools, in: Proceedings of ICATPN 2003, 2003, pp. 483-505.
[20] Fujita, M.; Kono, S.; Tanaka, H.; Moto-oka, T., Tokio: logic programming language based on temporal logic and its compilation to PROLOG, (Proceedings of ICLP 1986, LNCS, vol. 225, (1986)), 695-709 · Zbl 0596.68013
[21] Gabbay, D. M., Modal and temporal logic programming, (Temporal Logics and their Applications, (1987), Academic Press), 197-237
[22] Keller, R. M., Formal verification of parallel programs, Communications of the ACM, 19, 7, 371-384, (1976) · Zbl 0329.68016
[23] Milner, R., Communicating and mobile system: the \(\Pi\)-calculus, (1999), Cambridge University Press Cambridge · Zbl 0942.68002
[24] Moszkowski, B. C., Executing temporal logic programs, (1986), Cambridge University Press Cambridge · Zbl 0658.68014
[25] Owicki, S.; Gries, D., Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, 19, 5, 279-285, (1976) · Zbl 0322.68010
[26] Tendler, J. M.; Dodson, J. S.; Fields, J. S.; Le, H.; Sinharoy, B., Power4 system microarchitecture, IBM Journal of R&D, 46, 1, 5-26, (2002)
[27] Rondogiannis, R.; Gergatsoulis, M.; Panayiotopoulos, T., Cactus: a branching time logic programming languages, (Proceedings of 1st International Joint Conference Qualitative and Quantitative Practical Reasoning, LNAI, vol. 1244, (1997)), 511-524
[28] C.S. Tang, Toward a unified logical basis for programming languages, in: Proceedings of IFIP Congress, 1983, pp. 425-429.
[29] Tian, C.; Duan, Z., Complexity of propositional projection temporal logic with star, Mathematical Structures in Computer Science, 19, 73-100, (2009) · Zbl 1161.03008
[30] W.W. Wadge, Tense logic programming: a respectable alternative, in: Proceedings of the 1988 International Symposium on Lucid and Intensional Programming, 1988, pp. 26-32.
[31] Orgun, M. A.; Wadge, W. W., A theory and practice of temporal logic programming, (Intensional Logics for Programming, (1992), Oxford University Press), 23-50
[32] Yang, X.; Duan, Z., Operational semantics of framed tempura, Journal of Logic and Algebraic Programming, 78, 22-51, (2008) · Zbl 1170.68006
[33] Ma, Y.; Duan, Z.; Wang, X.; Yang, X., An interpreter for framed tempura and its application, (TASE 2007, (2007), IEEE Press), 251-260
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.