Skip to main content
SpringerLink
Log in

On Determinism

  • Chapter
  • First Online:
Principles of Modeling

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10760))

Abstract

The notion of deterministic execution of concurrent systems has appeared in many guises throughout Edward A. Lee’s œuvre, but few really grasp how powerful, important, subtle, and flexible the concept really is. Determinism can be thought of as an abstraction boundary that delineates where control is passed from a system designer to the implementation. This paper surveys some of the many forms of determinism available in the models of computation Lee and others have proposed.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    At least I do; ignoring people is more-or-less why I entered engineering. That hasn’t worked out too well.

  2. 2.

    A quasi-formalism because the notions of these sets are far too abstract to be a proper formalism. In particular, the sets E and B are difficult to define because they are meant to represent “everything else,” but this requires a careful definition of the universal set, which is not obvious.

  3. 3.

    I am sidestepping all the fussy bookkeeping necessary to deal with reused variable names because it is ultimately bland, mathematically speaking. See, e.g., Peyton Jones [29, Chap. 2].

References

  1. Banach, S.: Sur les opérations dans les ensembles abstraits et leur application aux équations intégrales. Fundamenta Mathematicae 3(1), 133–181 (1922)

    Article  Google Scholar 

  2. Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103, Revised ed, North-Holland (1984)

    Google Scholar 

  3. Bekić, H.: Definable operations in general algebras, and the theory of automata and flowcharts. In: Jones, C.B. (ed.) Programming Languages and Their Definition. LNCS, vol. 177, pp. 30–55. Springer, Heidelberg (1984). https://doi.org/10.1007/BFb0048939

    Chapter  MATH  Google Scholar 

  4. Berry, G.: The constructive semantics of pure Esterel. Draft book (1999)

    Google Scholar 

  5. Berry, G.: The foundations of Esterel. In: Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press (2000)

    Google Scholar 

  6. Berry, G., Gonthier, G.: The esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87–152 (1992)

    Article  Google Scholar 

  7. Bhattacharyya, S.S., Murthy, P.K., Lee, E.A.: Synthesis of embedded software from synchronous dataflow specifications. J. VLSI Sig. Process. Syst. 21(2), 151–166 (1999)

    Article  Google Scholar 

  8. Bilsen, G., Engels, M., Lauwereins, R., Peperstraete, J.A.: Cycle-static dataflow. IEEE Trans. Signal Process. 44(2), 397–408 (1996)

    Article  Google Scholar 

  9. Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications: International Conference Proceedings. LNCS, vol. 735. Springer, Heidelberg (1993). https://doi.org/10.1007/BFb0039704

    Chapter  Google Scholar 

  10. Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_5

    Chapter  Google Scholar 

  11. Bryant, R.E.: Boolean analysis of MOS circuits. IEEE Trans. Comput.- Aided Des. Integr. Circ. Syst. CAD 6(4), 634–649 (1987)

    Article  Google Scholar 

  12. Brzozowski, J.A., Seger, C.-J.H.: Asynchronous Circuits. Springer, New York (1995). https://doi.org/10.1007/978-1-4612-4210-9

    Book  MATH  Google Scholar 

  13. Brzozowski, J.A., Yoeli, M.: On a ternary model of gate networks. IEEE Trans. Comput. C–28(3), 178–184 (1979)

    Article  MathSciNet  Google Scholar 

  14. Buck, J.T.: Static scheduling and code generation from dynamic dataflow graphs with integer-valued control streams. In: Proceedings of the Asilomar Conference on Signals, Systems and Computers, Pacific Grove, California, pp. 508–513, October 1994

    Google Scholar 

  15. Cataldo, A., Lee, E., Liu, X., Matsikoudis, E., Zheng, H.: Discrete-event systems: generalizing metric spaces and fixed point semantics. Technical report UCB/ERL M05/12, University of California, Berkeley, April 2005

    Google Scholar 

  16. Cataldo, A., Lee, E., Liu, X., Matsikoudis, E., Zheng, H.: A constructive fixed-point theorem and the feedback semantics of timed systems. In: Workshop on Discrete Event Systems, 10–12 July 2006

    Google Scholar 

  17. Church, A.: A set of postulates for the foundation of logic. Ann. Math. 33(2), 346–366 (1932)

    Article  MathSciNet  Google Scholar 

  18. Church, A.: The Calculi of Lambda-Conversion. Princeton University Press, Princeton (1941)

    MATH  Google Scholar 

  19. Church, A., Rosser, J.B.: Some properties of conversion. Trans. Am. Math. Soc. 39(3), 472–482 (1936)

    Article  MathSciNet  Google Scholar 

  20. Cousot, P.: Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Rapport de Recherche IMAG-RR-88, Laboratoire d’Informatique, Université Scientifique et Médicale de Grenoble, Grenoble, France, September 1977

    Google Scholar 

  21. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)

    MATH  Google Scholar 

  22. Edwards, S.A.: Concurrency and communication: lessons from the SHIM project. In: Lee, S., Narasimhan, P. (eds.) SEUS. LNCS, vol. 5860, pp. 276–287. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10265-3_25

    Chapter  Google Scholar 

  23. Edwards, S.A., Lee, E.A.: The semantics and execution of a synchronous block-diagram language. Sci. Comput. Program. 48(1), 21–42 (2003)

    Article  MathSciNet  Google Scholar 

  24. Edwards, S.A., Tardieu, O.: SHIM: A deterministic model for heterogeneous embedded systems. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 14(8), 854–867 (2006)

    Article  Google Scholar 

  25. Edwards, S.A., Townsend, R., Kim, M.A.: Compositional dataflow circuits. In: Proceedings of the International Conference on Formal Methods and Models for Codesign (MEMOCODE), Vienna, Austria, September 2017

    Google Scholar 

  26. Eichelberger, E.B.: Hazard detection in combinational and sequential switching circuits. IBM J. Res. Dev. 9(2), 90–99 (1965)

    Article  Google Scholar 

  27. Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979). https://doi.org/10.1007/3-540-09724-4

    Book  MATH  Google Scholar 

  28. Hudak, P., Jones, S.P., Wadler, P.: Report on the programming language Haskell: a non-strict purely functional language (version 1.2). ACM SIGPLAN Not. 27(5), 1–164 (1992)

    Google Scholar 

  29. Jones, S.P.: The Implementation of Functional Programming Languages. Prentice Hall, New Jersey (1987)

    MATH  Google Scholar 

  30. Gilles, K.: The semantics of a simple language for parallel programming. In: Information Processing 74: Proceedings of IFIP Congress 74, Stockholm, Sweden, pp. 471–475, August 1974

    Google Scholar 

  31. Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 21(12), 1377–1394 (2002)

    Article  Google Scholar 

  32. Jean-Louis, J.-L., Nguyen, V.L., Sonnenberg, E.A.: Fixed point theorems and semantics: a folk tale. Inf. Process. Lett. 14(3), 112–116 (1982)

    Article  MathSciNet  Google Scholar 

  33. Lee, E.A.: Modeling concurrent real-time processes using discrete events. Ann. Softw. Eng. 7, 25–45 (1999)

    Article  Google Scholar 

  34. Lee, E.A., Matsikoudis, E.: The semantics of dataflow with firing. In: From Semantics to Computer Science: Essays in Memory of Gilles Kahn, Chap. 4, pp. 71–94. Cambridge University Press, Cambridge (2008)

    Google Scholar 

  35. Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proc. IEEE 75(9), 1235–1245 (1987)

    Article  Google Scholar 

  36. Lee, E.A., Parks, T.M.: Dataflow process networks. Proc. IEEE 83(5), 773–801 (1995)

    Article  Google Scholar 

  37. Lee, E.A., Sangiovanni-Vincentelli, A.: A framework for comparing models of computation. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 17(12), 1217–1229 (1998)

    Article  Google Scholar 

  38. Lee, E., Varaiya, P.: Structure and Interpretation of Signals and Systems. Addison-Wesley, Reading (2003)

    Google Scholar 

  39. Lee, E.A., Zheng, H.: Leveraging synchronous language principles for heterogeneous modeling and design of embedded systems. In: Proceedings of the International Conference on Embedded Software (EMSOFT), Austria, pp. 114–123, September 2007

    Google Scholar 

  40. Malik, S.: Analysis of cyclic combinational circuits. In: Proceedings of the International Conference on Computer Aided Design (ICCAD), Santa Clara, California, pp. 618–625, November 1993

    Google Scholar 

  41. McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, part I. Commun. ACM 3(4), 184–195 (1960)

    Article  Google Scholar 

  42. Mendler, M., Shiple, T.R., Berry, G.: Constructive Boolean circuits and the exactness of timed ternary simulation. J. Formal Methods Syst. Des. 40(3), 283–329 (2012)

    Article  Google Scholar 

  43. Muller, D.E.: Treatment of transition signals in electronic switching circuits by algebraic methods. IRE Trans. Electron. Comput. EC–8(3), 401 (1959)

    Article  Google Scholar 

  44. Penry, D.A., August, D.I.: Optimizations for a simulator construction system supporting reusable components. In: Proceedings of the 40th Design Automation Conference, Anaheim, California, pp. 926–931, June 2003

    Google Scholar 

  45. Pollack, R.: Polishing up the Tait-Martin-Löf proof of the Church-Rosser theorem. In: Proceedings De Wintermöte, Göteborg, Sweden. Department of Computing Science, Chalmers University, January 1995

    Google Scholar 

  46. Scott, D.: Continuous lattices. In: Lawvere, F.W. (ed.) Toposes, Algebraic Geometry and Logic. LNM, vol. 274, pp. 97–136. Springer, Heidelberg (1972). https://doi.org/10.1007/BFb0073967

    Chapter  Google Scholar 

  47. Scott, D.: Data types as lattices. SIAM J. Comput. 5(3), 522–587 (1976)

    Article  MathSciNet  Google Scholar 

  48. Shiple, T.R., Berry, G., Touati, H.: Constructive analysis of cyclic circuits. In: Proceedings of the European Design and Test Conference, Paris, France, pp. 328–333, March 1996

    Google Scholar 

  49. Stoy, J.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1977)

    MATH  Google Scholar 

  50. Sussman, G.J., Steele Jr., G.L.: Scheme: an interpreter for extended lambda calculus. Technical report AIM-349, MIT AI Lab, Cambridge, Massachusetts (1975)

    Google Scholar 

  51. Takahashi, M.: Parallel reductions in \(\lambda \)-calculus. J. Symb. Comput. 7(2), 113–123 (1989)

    Article  MathSciNet  Google Scholar 

  52. Takahashi, M.: Parallel reductions in \(\lambda \)-calculus. Inf. Comput. 118(1), 120–127 (1995)

    Article  MathSciNet  Google Scholar 

  53. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)

    Article  MathSciNet  Google Scholar 

  54. Turing, A.M.: Computability and \(\lambda \)-definability. J. Symb. Logic 2(4), 153–163 (1937)

    Article  Google Scholar 

  55. Wei, J.: Parallel asynchronous iterations of least fixed points. Parallel Comput. 19(8), 886–895 (1993)

    Article  MathSciNet  Google Scholar 

  56. Winskel, G.: The Formal Semantics of Programming Languages: An Introduction Foundations of Computing. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

Download references

Acknowledgements

The National Science Foundation funded this work (CCF-1162124); the suggestions of two anonymous reviewers definitely improved this paper.

Author information

Authors and Affiliations

  1. Columbia University, New York, USA

    Stephen A. Edwards

Authors
  1. Stephen A. Edwards
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stephen A. Edwards .

Editor information

Editors and Affiliations

  1. University of California, Berkeley, Berkeley, California, USA

    Marten Lohstroh

  2. National Instruments, Berkeley, California, USA

    Patricia Derler

  3. Mälardalen University, Västerås, Sweden, Reykjavík University, Reykjavik, Iceland

    Marjan Sirjani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Edwards, S.A. (2018). On Determinism. In: Lohstroh, M., Derler, P., Sirjani, M. (eds) Principles of Modeling. Lecture Notes in Computer Science(), vol 10760. Springer, Cham. https://doi.org/10.1007/978-3-319-95246-8_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95246-8_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95245-1

  • Online ISBN: 978-3-319-95246-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation