Concurrent Programming from pseuCo to Petri
The growing importance of concurrent programming has made practical concurrent software development become a cornerstone of many computer science curricula. Since a few years, a sound bridge from concurrency theory to concurrence practice is available in the form of pseuCo, a light-weight programming language featuring both message passing and shared memory concurrency. That language is at the core of an award-winning lecture at Saarland Informatics Campus. This paper presents a novel two-step semantic mapping from pseuCo programs to colored Petri nets, developed for the sake of further strengthening the educational concept behind pseuCo. The approach is fully integrated in Open image in new window , our open-source teaching tool for pseuCo, empowering students to interact with the Petri-net-based semantics of pseuCo. In addition, we present a source-level exploration tool for pseuCo, also based on this semantics, that gives users an IDE-like debugging experience while enabling full control over the nondeterminism inherent in their programs. The debugger is also part of Open image in new window , allowing students to access it without any set-up.
KeywordsConcurrency Education Colored Petri nets Programming Semantics
We would like to thank Bernd Finkbeiner for supervising an earlier phase of this project. Michaela Klauck provided helpful feedback during development of the debugging feature of Open image in new window . This work was partially supported by the ERC Advanced Investigators Grant 695614 (POWVER) and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 389792660 – TRR 248 (see https://perspicuous-computing.science).
- 4.Biewer, S., Freiberger, F., Held, P.L., Hermanns, H.: Teaching academic concurrency to amazing students. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 170–195. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_9CrossRefGoogle Scholar
- 6.ECMA International: ECMAScript\(\copyright \) 2015 Language Specification, 6th edn., June 2015. Standard ECMA-262Google Scholar
- 9.Garavel, H.: Nested-unit Petri nets. J. Log. Algebr. Methods Program. 104, 60–85 (2019). https://doi.org/10.1016/j.jlamp.2018.11.005, http://www.sciencedirect.com/science/article/pii/S2352220817302018MathSciNetCrossRefGoogle Scholar
- 10.The Go Programming Language Specification. http://golang.org/ref/spec
- 11.Holzmann, G.: The Spin Model Checker – Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)Google Scholar
- 14.Kristensen, L.M., Christensen, S.: Implementing coloured Petri nets using a functional programming language. High. Order Symb. Comput. 17(3), 207–243 (2004). https://doi.org/10.1023/B:LISP.0000029445.29210.caCrossRefzbMATHGoogle Scholar