Document Open Access Logo

Non-Deterministic Abstract Machines

Authors Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2022.7.pdf
  • Filesize: 0.77 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Abstract machines
Keywords
  • Abstract machines
  • non-determinism
  • lambda-calculus
  • process calculi

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present a generic design of abstract machines for non-deterministic programming languages, such as process calculi or concurrent lambda calculi, that provides a simple way to implement them. Such a machine traverses a term in the search for a redex, making non-deterministic choices when several paths are possible and backtracking when it reaches a dead end, i.e., an irreducible subterm. The search is guaranteed to terminate thanks to term annotations the machine introduces along the way.
We show how to automatically derive a non-deterministic abstract machine from a zipper semantics - a form of structural operational semantics in which the decomposition process of a term into a context and a redex is made explicit. The derivation method ensures the soundness and completeness of the machines w.r.t. the zipper semantics.

Cite As Get BibTex

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Non-Deterministic Abstract Machines. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.7

Author Details

Małgorzata Biernacka
  • Institute of Computer Science, University of Wrocław, Poland
Dariusz Biernacki
  • Institute of Computer Science, University of Wrocław, Poland
Sergueï Lenglet
  • Université de Lorraine, Nancy, France
Alan Schmitt
  • INRIA, Rennes, France

Funding

This work is partially funded by PHC Polonium and by the National Science Centre of Poland under grant no. 2019/33/B/ST6/00289.

Acknowledgements

We thank the anonymous reviewers for their comments.

References

  1. Beniamino Accattoli and Giulio Guerrieri. Abstract machines for open call-by-value. Sci. Comput. Program., 184, 2019. Google Scholar
  2. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden, pages 8-19. ACM, 2003. Google Scholar
  3. Federico Aschieri, Agata Ciabattoni, and Francesco A. Genco. On the concurrent computational content of intermediate logics. Theor. Comput. Sci., 813:375-409, 2020. URL: https://doi.org/10.1016/j.tcs.2020.01.022.
  4. Philippe Bidinger, Alan Schmitt, and Jean-Bernard Stefani. An abstract machine for the kell calculus. In Martin Steffen and Gianluigi Zavattaro, editors, Formal Methods for Open Object-Based Distributed Systems, 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005, Proceedings, volume 3535 of Lecture Notes in Computer Science, pages 31-46. Springer, 2005. Google Scholar
  5. Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Non-deterministic abstract machines. Implementation available at URL: https://gitlab.inria.fr/skeletons/ndam/.
  6. Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Non-deterministic abstract machines. Technical Report 9475, Inria, 2022. available at URL: https://hal.inria.fr/hal-03545768.
  7. Malgorzata Biernacka, Witold Charatonik, and Klara Zielinska. Generalized refocusing: From hybrid strategies to abstract machines. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs, pages 10:1-10:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  8. Malgorzata Biernacka and Olivier Danvy. A concrete framework for environment machines. ACM Trans. Comput. Log., 9(1):6, 2007. Google Scholar
  9. Vincent Danos and Jean Krivine. Reversible communicating systems. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 292-307. Springer, 2004. Google Scholar
  10. Olivier Danvy. From reduction-based to reduction-free normalization. In Pieter W. M. Koopman, Rinus Plasmeijer, and S. Doaitse Swierstra, editors, Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures, volume 5832 of Lecture Notes in Computer Science, pages 66-164. Springer, 2008. Google Scholar
  11. Olivier Danvy and Lasse R. Nielsen. Syntactic theories in practice. Electron. Notes Theor. Comput. Sci., 59(4):358-374, 2001. Google Scholar
  12. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. The MIT Press, 2009. Google Scholar
  13. Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD-machine, and the λ-calculus. In Martin Wirsing, editor, Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986, pages 193-222. North-Holland, 1987. Google Scholar
  14. Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103(2):235-271, 1992. Google Scholar
  15. Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103(2):235-271, 1992. Google Scholar
  16. Fabrice Le Fessant. JoCaml: conception et implémentation d'un langage à agents mobiles. PhD thesis, École polytechnique, 2001. Google Scholar
  17. Cormac Flanagan and Matthias Felleisen. The semantics of future and an application. J. Funct. Program., 9(1):1-31, 1999. URL: https://doi.org/10.1017/s0956796899003329.
  18. Cédric Fournet and Georges Gonthier. The reflexive CHAM and the join-calculus. In Hans-Juergen Boehm and Guy L. Steele Jr., editors, Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, pages 372-385. ACM Press, 1996. Google Scholar
  19. Philippa Gardner, Cosimo Laneve, and Lucian Wischik. The fusion machine. In Lubos Brim, Petr Jancar, Mojmír Kretínský, and Antonín Kucera, editors, CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, volume 2421 of Lecture Notes in Computer Science, pages 418-433. Springer, 2002. Google Scholar
  20. Florence Germain, Marc Lacoste, and Jean-Bernard Stefani. An abstract machine for a higher-order distributed process calculus. Electron. Notes Theor. Comput. Sci., 66(3):145-169, 2002. Google Scholar
  21. Paola Giannini, Davide Sangiorgi, and Andrea Valente. Safe ambients: Abstract machine and distributed implementation. Sci. Comput. Program., 59(3):209-249, 2006. Google Scholar
  22. Jan Friso Groote and Frits W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Inf. Comput., 100(2):202-260, 1992. Google Scholar
  23. John Hannan and Dale Miller. From operational semantics for abstract machines. Math. Struct. Comput. Sci., 2(4):415-459, 1992. Google Scholar
  24. Daniel Hirschkoff, Damien Pous, and Davide Sangiorgi. An efficient abstract machine for safe ambients. J. Log. Algebraic Methods Program., 71(2):114-149, 2007. Google Scholar
  25. Gérard P. Huet. The zipper. J. Funct. Program., 7(5):549-554, 1997. Google Scholar
  26. Simon L. Peyton Jones. Implementing lazy functional languages on stock hardware: The spineless tagless G-machine. J. Funct. Program., 2(2):127-202, 1992. Google Scholar
  27. Claude Kirchner, Radu Kopetz, and Pierre-Etienne Moreau. Anti-pattern matching. In Rocco De Nicola, editor, Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4421 of Lecture Notes in Computer Science, pages 110-124. Springer, 2007. Google Scholar
  28. Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, 20(3):199-207, 2007. Google Scholar
  29. Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308-320, 1964. Google Scholar
  30. Ivan Lanese and Doriana Medic. A general approach to derive uncontrolled reversible semantics. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 33:1-33:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  31. Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi, and Alan Schmitt. On the expressiveness and decidability of higher-order process calculi. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 145-155. IEEE Computer Society, 2008. Google Scholar
  32. Sergueï Lenglet, Alan Schmitt, and Jean-Bernard Stefani. Characterizing contextual equivalence in calculi with passivation. Inf. Comput., 209(11):1390-1433, 2011. Google Scholar
  33. Xavier Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990. Google Scholar
  34. Luís M. B. Lopes, Fernando M. A. Silva, and Vasco Thudichum Vasconcelos. A virtual machine for a process calculus. In Gopalan Nadathur, editor, Principles and Practice of Declarative Programming, International Conference PPDP'99, Paris, France, September 29 - October 1, 1999, Proceedings, volume 1702 of Lecture Notes in Computer Science, pages 244-260. Springer, 1999. Google Scholar
  35. Urmi Majumder and John H. Reif. Design of a biomolecular device that executes process algebra. Nat. Comput., 10(1):447-466, 2011. Google Scholar
  36. Joachim Niehren, Jan Schwinghammer, and Gert Smolka. A concurrent lambda calculus with futures. Theor. Comput. Sci., 364(3):338-356, 2006. URL: https://doi.org/10.1016/j.tcs.2006.08.016.
  37. Andrew Phillips and Luca Cardelli. A correct abstract machine for the stochastic pi-calculus. In Concurrent Models in Molecular Biology, 2004. Google Scholar
  38. Andrew Phillips, Nobuko Yoshida, and Susan Eisenbach. A distributed abstract machine for boxed ambient calculi. In David A. Schmidt, editor, Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, volume 2986 of Lecture Notes in Computer Science, pages 155-170. Springer, 2004. Google Scholar
  39. Iain C. C. Phillips and Irek Ulidowski. Reversing algebraic process calculi. J. Log. Algebraic Methods Program., 73(1-2):70-96, 2007. Google Scholar
  40. Gordon D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark, September 1981. Google Scholar
  41. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239:340-355, 2014. Google Scholar
  42. Davide Sangiorgi. Bisimulation in higher-order process calculi. In Ernst-Rüdiger Olderog, editor, Programming Concepts, Methods and Calculi, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET '94) San Miniato, Italy, 6-10 June, 1994, volume A-56 of IFIP Transactions, pages 207-224. North-Holland, 1994. Google Scholar
  43. Davide Sangiorgi and David Walker. The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  44. Filip Sieczkowski, Malgorzata Biernacka, and Dariusz Biernacki. Automating derivations of abstract machines from reduction semantics: - A generic formalization of refocusing in Coq. In Jurriaan Hage and Marco T. Morazán, editors, Implementation and Application of Functional Languages - 22nd International Symposium, IFL 2010, Alphen aan den Rijn, The Netherlands, September 1-3, 2010, Revised Selected Papers, volume 6647 of Lecture Notes in Computer Science, pages 72-88. Springer, 2010. Google Scholar
  45. Prasanna Thati, Koushik Sen, and Narciso Martí-Oliet. An executable specification of asynchronous pi-calculus semantics and may testing in maude 2.0. Electron. Notes Theor. Comput. Sci., 71:261-281, 2002. Google Scholar
  46. David Turner. The Polymorphic Pi-calculus:Theory and Implementation. PhD thesis, University of Edinburgh, 1995. Google Scholar
  47. Irek Ulidowski, Ivan Lanese, Ulrik Pagh Schultz, and Carla Ferreira, editors. Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC1405, volume 12070 of Lecture Notes in Computer Science. Springer, 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact