Lochbihler A. A machine-checked, type-safe model of Java concurrency

Karlsruhe: KIT Scientific Publishing, 2012. — 440 p.Java concurrency
Historical overview
Contributions
Isabelle/HOLLocales
Induction and coinduction
Source code
Abstract syntax
Type system
Native methods
Well-formedness
Dynamic semantics
Type safety
The JinjaThreads virtual machine
The bytecode language
Semantics
Well-typings
Type safety
Comparison with Jinja, Bali, and muJava
Interleaving semantics
Framework for interleaving semantics
The multithreaded state
Thread actions
Interleaving semantics
Infrastructure for well-formedness constraints
Native methods for synchronisation
Source code
Bytecode
Deadlock and type safety
Deadlock as a state property
Deadlock for threads
Progress up to deadlock
Type safety for source code
Type safety for bytecode
Formalisations of Java and Java bytecode
Type safety proofs and deadlocks
Large-scale programming language formalisations
Memory models
The heap as a module
Abstract operations and their properties
Adaptations to semantics and proofs
Design considerations
Sequential consistency
Java memory model
Informal explanation
Formal definition
The data race freedom guarantee
Consistency
Type safety
Discussion
Memory models and data race freedom
Abstract heap modules
Modular formalisations
Compiler
Semantic preservation
Simulation properties
Lifting simulations in the interleaving framework
Semantic preservation for the Java memory model
Explicit call stacks for source code
State and semantics
Semantic equivalence
Intermediate language J
Compilation stage
Preservation of well-formedness
Semantic preservation
Compilation stage
Preservation of well-formedness
Semantic preservation
Complete compiler
Discussion
Related work
JinjaThreads as a Java interpreter
Isabelle code extraction facilities
The code generator
The predicate compiler
Data structures
Locales and code extraction
Generic well-formedness
The bytecode verifier
Type inference for source code
The single-threaded semantics
Schedulers
Tabulation
Efficiency of the interpreter
Guidelines for executable formalisations
The translator JavaJinja
The translation
Validation
Related Work
Efforts and rewards of a machine-checked formalisation
Experience: Working with Isabelle/HOL
From Java light to JinjaThreads
Comparison between Java and JinjaThreads
Future workProducer-consumer example
Declarations and lookup functions
Binary operators
Sequential consistency
The Java memory model
Signatures
Semantics of method clone
Semantics of native methods
Generic well-formedness
Typing rules for expressions
Definite Assignment
Small-step semantics
Observability
Applicability and effect
The virtual machine
Observability
The Java memory model
Compilation stage
Compilation stage
Preprocessor