Jinja with threads: We extend the Jinja source code semantics by Klein and Nipkow with Java-style arrays and threads. Concurrency is captured in a generic framework semantics for adding concurrency through interleaving to a sequential semantics, which features dynamic thread creation, inter-thread communication via shared memory, lock synchronisation and joins. Also, threads can suspend themselves and be notified by others. We instantiate the framework with the adapted versions of both Jinja source and byte code and show type safety for the multithreaded case. Equally, the compiler from source to byte code is extended, for which we prove weak bisimilarity between the source code small step semantics and the defensive Jinja virtual machine. On top of this, we formalise the JMM and show the DRF guarantee and consistency. For description of the different parts, see Lochbihler’s papers at FOOL 2008, ESOP 2010, ITP 2011, and ESOP 2012.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Mansky, Susannah; Gunter, Elsa L.: Safety of a smart classes-used regression test selection algorithm (2020)
- Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
- Moser, Georg; Schaper, Michael: From Jinja bytecode to term rewriting: a complexity reflecting transformation (2018)
- Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy: Foundational (co)datatypes and (co)recursion for higher-order logic (2017)
- Lochbihler, Andreas: Java and the Java memory model -- a unified, machine-checked formalisation (2012)
- Lochbihler, Andreas; Bulwahn, Lukas: Animating the formalised semantics of a Java-like language (2011)
- Nipkow, Tobias: Verified efficient enumeration of plane graphs modulo isomorphism (2011)
- Lochbihler, Andreas: Verifying a compiler for Java threads (2010)
- Lochbihler, Andreas: Formalising FinFuns -- generating code for functions as data from Isabelle/HOL (2009)