Generating C Code from LOGS Specifications
- 361 Downloads
This paper introduces a tool that automatically translates a concrete form of specifications into C code linked with BSPlib. The translation tool is rigorously developed with important safety properties proved. A Logs specification for Bulk-Synchronous Parallelism is a relation of an initial state, a final state and some intermediate states. Nondeterminism and parallelism correspond to disjunction and conjunction respectively. Various advanced specification commands can be derived from the basic ones. The translator checks syntax, freedom of communication interference, type consistency and communication dependencies before generating the target code. Static analysis (including both static checkings and translation) is presented in abstract interpretation. It is shown that a few laws are complete for transforming any specification into a normal form. These laws are satisfied by the abstract functions. We demonstrate the actual effects of the abstract functions by applying them on the normal form. The approach has been implemented using an object-oriented language.
KeywordsNormal Form Inference Rule Abstract Function Parallel Composition Early Transition
Unable to display preview. Download preview PDF.
- 1.Chen, Y.: A language of flexible objects. Technical Report 29, Department of Computer Science, Leicester University (2004)Google Scholar
- 4.Cousot, P.: Types as abstract interpretations. In: Proceedings of POPL, pp. 316–331. ACM, New York (1997)Google Scholar
- 6.Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixedpoints. In: Proceedings of 4th POPL, pp. 238–252. ACM, New York (1977)Google Scholar
- 11.Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)Google Scholar
- 12.McColl, W.F.: Compositional systems. In: Symposium in Celebration of the work of C.A.R. Hoare (1999)Google Scholar