| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
project summary
Jinja with Threads
| Title: | Jinja with Threads |
| Author: | Andreas Lochbihler |
| Submission date: | 2007-12-03 |
| Abstract: | 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. For explanations on the framework semantics and the source code instantiation, see the FOOL 2008 paper by A. Lochbihler. |
| Change history: |
[2008-04-23]:
added bytecode formalisation with arrays and threads, added thread joins
(revision f74a8be156a7) [2009-04-27]: added verified compiler from source code to bytecode; encapsulate native methods in separate semantics (revision e4f26541e58a) [2009-11-30]: extended compiler correctness proof to infinite and deadlocking computations (revision e50282397435) [2010-06-08]: added thread interruption; new abstract memory model with sequential consistency as implementation (revision 0cb9e8dbd78d) [2010-06-28]: new thread interruption model (revision c0440d0a1177) [2010-10-15]: preliminary version of the Java memory model for source code (revision 02fee0ef3ca2) [2010-12-16]: improved version of the Java memory model, also for bytecode executable scheduler for source code semantics (revision 1f41c1842f5a) [2011-02-02]: simplified code generator setup new random scheduler (revision 3059dafd013f) [2011-07-21]: new interruption model, generalized JMM proof of DRF guarantee, allow class Object to declare methods and fields, simplified subtyping relation, corrected division and modulo implementation (revision 46e4181ed142) |
| License: | BSD License |
| Depends on: | Collections, Coinductive, FinFun |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|