A hoare calculus for the verification of synchronous languages

ABSTRACT

The synchronous model of computation divides the execution of a program into macro steps that consist of finitely many atomic micro steps (like assignments). The micro steps of a macro step are executed within the same variable environment (i.e. in parallel) but all updates to the variables are synchronously performed at the level of macro steps. The availability of a formally defined semantics allows one to use formal methods for the verification of synchronous programs. To this end, model checking is already widely used for synchronous programs, but the use of interactive verification e.g. by using a Hoare calculus, is only in its infancies. One reason for this situation is that the assignment rule of the classic Hoare calculus implicitly defines a sequential programming model which is only a special case of the synchronous model of computation.

In this paper, we therefore suggest a generalization of the classic Hoare calculus to deal with synchronous programs. The main idea is thereby that the assignment rule refers to all assignments made in a macro step so that the synchronous model of computation is axiomatized. It is possible to rewrite all synchronous programs so that the assignments of every macro step are collected in a single tuple assignment. This way, our generalization of the assignment rule is applicable to arbitrary synchronous programs. We present non-trivial case studies that show the feasibility of our approach.

References

1. G. Andrews. Parallel programs: proofs, principles, and practice. Communications of the ACM (CACM), 24(3):140--145, March 1981.
2. K. Apt. Ten years of Hoare's logic: A survey - part I. ACM Transactions on Programming Languages and Systems (TOPLAS), 3(4):431--483, 1981.
3. K. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer, 2 edition, 1997.
4. E. Ashcroft and Z. Manna. The translation of "go to" programs to "while" programs. Technical Report CS-TR-71--188, Department of Computer Science, University of California, Stanford, California, USA, January 1971.
5. T. Ball, A. Podelski, and S. Rajamani. Relative completeness of abstraction refinement for software model checking. In J.-P. Katoen and P. Stevens, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2280 of LNCS, pages 158--172, Grenoble, France, 2002. Springer.
6. A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. The synchronous languages twelve years later. Proceedings of the IEEE, 91(1):64--83, 2003.
7. G. Berry. The constructive semantics of pure Esterel. http://www-sop.inria.fr/esterel.org/, July 1999.
8. C. Boehm and G. Jacopini. Flow diagrams, Turing machines, and languages with only two formation rules. Communications of the ACM (CACM), 9(5):366--371, 1966.
9. J. Brandt and K. Schneider. Formal reasoning about causality analysis. In O. A. Mohamed, C. Muñoz, and S. Tahar, editors, Theorem Proving in Higher Order Logics (TPHOL), volume 5170 of LNCS, pages 118--133, Montréal, Québec, Canada, 2008. Springer.
10. J. Brandt and K. Schneider. Round trip to asynchrony and synchrony. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Oldenburg, Germany, 2011.
11. J. Brandt and K. Schneider. Separate translation of synchronous programs to guarded actions. Internal Report 382/11, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, March 2011.
12. S. Brookes. On the axiomatic treatment of concurrency. In S. Brookes, A. Roscoe, and G. Winskel, editors, Seminar on Concurrency (CONCUR), volume 197 of LNCS, pages 1--34, Pittsburgh, Pennsylvania, USA, 1985. Springer.
13. J. Bruno and K. Steiglitz. The expression of algorithms by charts. Journal of the ACM (JACM), 19(3):517--525, July 1972.
14. S. Chaki, E. Clarke, A. Groce, J. Ouaknine, O. Strichman, and K. Yorav. Efficient verification of sequential and concurrent C programs. Formal Methods in System Design (FMSD), 25(2--3):129--166, September 2004.
15. P. Cousot. Methods and logics for proving programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 15, pages 841--993. Elsevier, 1990.
16. F. de Boer, U. Hannemann, and W.-P. de Roever. Hoare-style compositional proof systems for reactive shared variable concurrency. In S. Ramesh and G. Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1346 of LNCS, pages 267--283, Kharagpur, India, 1997. Springer.
17. W. de Roever. Concurrency Verification. Cambridge University Press, 2001.
18. J. Dingel. Towards a unified development methodology for shared-variable parallel and distributed programs. In W. Grieskamp, T. Santen, and B. Stoddart, editors, Integrated Formal Methods (IFM), volume 1945 of LNCS, pages 214--234, Dagstuhl, Germany, 2000. Springer.
19. C. Elgot. Structured programming with and without "go to" statements. IEEE Transactions on Software Engineering (T-SE), SE-2(1):41--54, March 1976.
20. R. Floyd. Assigning meanings to programs. In J. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Symposia in Applied Mathematics, pages 19--32, Providence, Rhode Island, USA, 1967. American Mathematical Society.
21. P. Godefroid. Software model checking: The VeriSoft approach. Formal Methods in System Design (FMSD), 26(2):77--101, March 2005.
22. D. Gries. The Science of Programming. Springer, 1981.
23. N. Halbwachs. Synchronous programming of reactive systems. Kluwer, 1993.
24. C. Hoare. An axiomatic basis for computer programming. Communications of the ACM (CACM), 12(10):576--580, 1969.
25. J. Joyce and C.-J. Seger. The HOL-Voss system: Model-checking inside a general-purpose theorem-prover. In J. Joyce and C.-J. Seger, editors, Theorem Proving in Higher Order Logics (TPHOL), volume 780 of LNCS, pages 185--198, Vancouver, British Columbia, Canada, 1994. Springer.
26. V. Kahlon and C. Wang. Universal causality graphs: A precise happens-before model for detecting bugs in concurrent programs. In T. Touili, B. Cook, and P. Jackson, editors, Computer Aided Verification (CAV), volume 6174 of LNCS, pages 434--449, Edinburgh, Scotland, UK, 2010. Springer.
27. R. Karp and V. Ramachandran. A survey of parallel algorithms for shared-memory machines. Technical Report UCB/CSD-88--408, EECS Department, University of California, Berkeley, http://www.eecs.berkeley.edu/Pubs/TechRpts/1988/CSD-88--408.pdf, March 1988.
28. C. Kern and M. Greenstreet. Formal verification in hardware design: A survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2):123--193, 1999.
29. L. Lamport. The "Hoare Logic" of concurrent programs. Acta Informatica, 14:21--37, 1980.
30. L. Lamport and F. Schneider. The "Hoare" logic CSP, and all that. ACM Transactions on Programming Languages and Systems (TOPLAS), 6(2):281--296, April 1984.
31. A. Martin and J. Tucker. The concurrent assignment representation of synchronous systems. Parallel Computing, 9(2):227--256, 1989.
32. P. Metaxas. Thinking and programming in parallel, 1997. Lecture Notes.
33. H. Mills. The new math of computer programming. Communications of the ACM (CACM), 18(1):43--48, January 1975.
34. Nvidia Corporation. NVIDIA CUDA Compute Unified Device Architecture -- Programming Guide. Nvidia Corporation, 2008.
35. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319--340, 1976.
36. S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM (CACM), 19(5):279--284, 1976.
37. S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 4(3):455--495, July 1982.
38. D. Potop-Butucaru, S. Edwards, and G. Berry. Compiling Esterel. Springer, 2007.
39. K. Schneider. The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, December 2009.
40. K. Schneider and J. Brandt. Performing causality analysis by bounded model checking. In Application of Concurrency to System Design (ACSD), pages 78--87, Xi'an, China, 2008. IEEE Computer Society.
41. K. Schneider, J. Brandt, and T. Schuele. A verified compiler for synchronous programs with local declarations. Electronic Notes in Theoretical Computer Science (ENTCS), 153(4):71--97, 2006.
42. K. Schneider, J. Brandt, T. Schuele, and T. Tuerk. Maximal causality analysis. In J. Desel and Y. Watanabe, editors, Application of Concurrency to System Design (ACSD), pages 106--115, St. Malo, France, 2005. IEEE Computer Society.
43. L. Seiler, D. Carmean, E. Sprangle, T. Forsyth, M. Abrash, P. Dubey, S. Junkins, A. Lake, J. Sugerman, R. Cavin, R. Espasa, E. Grochowski, T. Juan, and P. Hanrahan. Larrabee: A many-core x86 architecture for visual computing. ACM Transactions on Graphics (TOG), 27(3):18, August 2008.
44. C. Stirling. A generalization of Owicki-Gries's Hoare logic for a concurrent while language. Theoretical Computer Science (TCS), 58(1--3):347--359, June 1988.
45. M. Stokelya, S. Chakia, and J. Ouaknine. Parallel assignments in software model checking. Electronic Notes in Theoretical Computer Science (ENTCS), 157:77--94, 2006.
46. S. Tini. An axiomatic semantics for Esterel. Theoretical Computer Science (TCS), 269(1--2):231--282, October 2001.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Pre- and post-conditions