Generating C Code from LOGS Specifications

  • Jianguo Zhou
  • Yifeng Chen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


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.


Normal Form Inference Rule Abstract Function Parallel Composition Early Transition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Chen, Y.: A language of flexible objects. Technical Report 29, Department of Computer Science, Leicester University (2004)Google Scholar
  2. 2.
    Chen, Y., Sanders, J.W.: Top-down design of BSP programs. Parallel Processing Letters 13(3), 389–400 (2003)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Chen, Y., Sanders, J.W.: Logic of global synchrony. ACM Transactions on Programming Languages and Systems 26(2), 221–262 (2004)CrossRefGoogle Scholar
  4. 4.
    Cousot, P.: Types as abstract interpretations. In: Proceedings of POPL, pp. 316–331. ACM, New York (1997)Google Scholar
  5. 5.
    Cousot, P.: Abstract interpretation based formal methods and future challenges. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 138–156. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 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
  7. 7.
    Fortune, S., Wyllie, J.: Parallelism in random access machines. In: 10th Annual ACM Symposium on Theory of Computing, pp. 114–118. ACM Press, New York (1978)CrossRefGoogle Scholar
  8. 8.
    He, J., Miller, Q., Chen, L.: Algebraic laws for BSP programming. In: Fraigniaud, P., Mignotte, A., Robert, Y., Bougé, L. (eds.) Euro-Par 1996. LNCS, vol. 1124, pp. 359–367. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  9. 9.
    Hill, J.M.D., et al.: BSPlib: The BSP programming library. Parallel Computing 24(14), 1927–2148 (1998)CrossRefMathSciNetGoogle Scholar
  10. 10.
    Hoare, C.A.R., et al.: Laws of programming. Communications of the ACM 30(8), 672–686 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)Google Scholar
  12. 12.
    McColl, W.F.: Compositional systems. In: Symposium in Celebration of the work of C.A.R. Hoare (1999)Google Scholar
  13. 13.
    Valiant, L.G.: A bridging model for parallel computation. Communications of the ACM 33(8), 103–111 (1990)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Jianguo Zhou
    • 1
  • Yifeng Chen
    • 2
  1. 1.Depart. of Computer ScienceUniversity of LeicesterLeicesterUK
  2. 2.Depart. of Computer ScienceDurham UniversityDurhamUK

Personalised recommendations