### 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. 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.

### License

BSD License

### History

October 20, 2017
  add an atomic compare-and-swap operation for volatile fields (revision a6189b1d6b30)
May 16, 2013
  support for non-deterministic memory allocators (revision cc3344a49ced)
November 21, 2012
  type safety proof for the Java memory model, allow spurious wake-ups (revision 76063d860ae0)
February 16, 2012
  added example programs (revision bf0b06c8913d)
July 21, 2011
  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)
February 2, 2011
  simplified code generator setup new random scheduler (revision 3059dafd013f)
December 16, 2010
  improved version of the Java memory model, also for bytecode executable scheduler for source code semantics (revision 1f41c1842f5a)
October 15, 2010
  preliminary version of the Java memory model for source code (revision 02fee0ef3ca2)
June 28, 2010
  new thread interruption model (revision c0440d0a1177)
June 8, 2010
  added thread interruption; new abstract memory model with sequential consistency as implementation (revision 0cb9e8dbd78d)
November 30, 2009
  extended compiler correctness proof to infinite and deadlocking computations (revision e50282397435)
April 27, 2009
  added verified compiler from source code to bytecode; encapsulate native methods in separate semantics (revision e4f26541e58a)
April 23, 2008
  added bytecode formalisation with arrays and threads, added thread joins (revision f74a8be156a7)

### Topics

- Computer science/Programming languages/Language definitions

### Session JinjaThreads

- Set_without_equal
- Set_Monad
- JT_ICF
- Auxiliary
- Basic_Main
- FWState
- FWLock
- FWLocking
- FWThread
- FWWait
- FWCondAction
- FWWellform
- FWLockingThread
- FWInterrupt
- FWSemantics
- FWProgressAux
- FWDeadlock
- FWProgress
- FWLifting
- LTS
- FWLTS
- Bisimulation
- FWBisimulation
- FWBisimDeadlock
- FWLiftingSem
- FWInitFinLift
- FWBisimLift
- Semilat
- Err
- Opt
- Product
- Listn
- Semilattices
- Typing_Framework
- SemilatAlg
- Typing_Framework_err
- Kildall
- LBVSpec
- LBVCorrect
- LBVComplete
- Abstract_BV
- Type
- Decl
- TypeRel
- Value
- Exceptions
- SystemClasses
- Heap
- Observable_Events
- StartConfig
- Conform
- ExternalCall
- WellForm
- ExternalCallWF
- ConformThreaded
- BinOp
- SemiType
- Common_Main
- State
- Expr
- JHeap
- SmallStep
- WWellForm
- WellType
- DefAss
- JWellForm
- Threaded
- WellTypeRT
- Progress
- DefAssPreservation
- TypeSafe
- ProgressThreaded
- Deadlocked
- Annotate
- J_Main
- JVMState
- JVMInstructions
- JVMHeap
- JVMExecInstr
- JVMExceptions
- JVMExec
- JVMDefensive
- JVMThreaded
- JVM_Main
- JVM_SemiType
- Effect
- BVSpec
- BVConform
- BVSpecTypeSafe
- BVNoTypeError
- BVProgressThreaded
- JVMDeadlocked
- EffectMono
- TF_JVM
- LBVJVM
- BVExec
- BCVExec
- BV_Main
- CallExpr
- J0
- J0Bisim
- J1State
- J1Heap
- J1
- J1Deadlock
- PCompiler
- Compiler2
- Exception_Tables
- J1WellType
- J1WellForm
- TypeComp
- JVMTau
- Execs
- J1JVMBisim
- J1JVM
- JVMJ1
- Correctness2
- ListIndex
- Compiler1
- J0J1Bisim
- Correctness1Threaded
- Correctness1
- JJ1WellForm
- Compiler
- Correctness
- Preprocessor
- Compiler_Main
- MM
- SC
- SC_Interp
- SC_Collections
- Orders
- JMM_Spec
- JMM_DRF
- SC_Legal
- Non_Speculative
- SC_Completion
- HB_Completion
- JMM_Heap
- JMM_Framework
- JMM_Typesafe
- JMM_Common
- JMM_J
- DRF_J
- JMM_JVM
- DRF_JVM
- JMM_Type
- JMM_Compiler
- JMM_Type2
- JMM_Interp
- JMM_Typesafe2
- JMM_J_Typesafe
- JMM_JVM_Typesafe
- JMM_Compiler_Type2
- JMM
- MM_Main
- State_Refinement
- Scheduler
- Random_Scheduler
- Round_Robin
- SC_Schedulers
- TypeRelRefine
- PCompilerRefine
- J_Execute
- ExternalCall_Execute
- JVMExec_Execute2
- JVM_Execute2
- Code_Generation
- JVMExec_Execute
- JVM_Execute
- ToString
- Java2Jinja
- Execute_Main
- ApprenticeChallenge
- BufferExample
- Examples_Main
- JinjaThreads

### Depends on

- Automatic Data Refinement
- Binomial Heaps and Skew Binomial Heaps
- Coinductive
- Collections Framework
- Code Generation for Functions as Data
- Finger Trees
- Native Word
- Refinement for Monadic Programs
- Trie

## Cite

×

JinjaThreads-AFP

    @article{JinjaThreads-AFP,
      author  = {Andreas Lochbihler},
      title   = {Jinja with Threads},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2007},
      note    = {\url{https://isa-afp.org/entries/JinjaThreads.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 17, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 26, 2012 : Isabelle2012
- Oct 12, 2011 : Isabelle2011-1
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 2, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Apr 30, 2009 : Isabelle2009
- Apr 29, 2009 : Isabelle2009
- Jun 10, 2008 : Isabelle2008
- Dec 3, 2007 : Isabelle2007