A cylinder computation model for many-core parallel computing

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.