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

Introduction......Page 27
Java concurrency......Page 28
Historical overview......Page 33
Contributions......Page 34
Isabelle/HOL......Page 39
Notation......Page 40
Locales......Page 43
Induction and coinduction......Page 45
Source code......Page 49
Abstract syntax......Page 50
Type system......Page 55
Native methods......Page 60
Well-formedness......Page 61
Dynamic semantics......Page 63
Type safety......Page 68
The JinjaThreads virtual machine......Page 69
The bytecode language......Page 70
Semantics......Page 72
Well-typings......Page 76
Type safety......Page 80
Comparison with Jinja, Bali, and muJava......Page 81
Interleaving semantics......Page 85
Framework for interleaving semantics......Page 86
The multithreaded state......Page 87
Thread actions......Page 92
Interleaving semantics......Page 101
Infrastructure for well-formedness constraints......Page 104
Native methods for synchronisation......Page 108
Source code......Page 117
Bytecode......Page 122
Deadlock and type safety......Page 126
Deadlock as a state property......Page 127
Deadlock for threads......Page 131
Progress up to deadlock......Page 135
Type safety for source code......Page 138
Type safety for bytecode......Page 148
Formalisations of Java and Java bytecode......Page 153
Type safety proofs and deadlocks......Page 155
Large-scale programming language formalisations......Page 156
Memory models......Page 157
The heap as a module......Page 158
Abstract operations and their properties......Page 159
Adaptations to semantics and proofs......Page 162
Design considerations......Page 166
Sequential consistency......Page 167
Java memory model......Page 168
Informal explanation......Page 169
Formal definition......Page 174
The data race freedom guarantee......Page 190
Consistency......Page 211
Type safety......Page 214
Discussion......Page 218
Memory models and data race freedom......Page 227
Abstract heap modules......Page 229
Modular formalisations......Page 230
Compiler......Page 231
Semantic preservation......Page 234
Simulation properties......Page 236
Lifting simulations in the interleaving framework......Page 244
Semantic preservation for the Java memory model......Page 251
Explicit call stacks for source code......Page 252
State and semantics......Page 253
Semantic equivalence......Page 258
Intermediate language J1......Page 262
Compilation stage 1......Page 268
Preservation of well-formedness......Page 269
Semantic preservation......Page 270
Compilation stage 2......Page 276
Preservation of well-formedness......Page 277
Semantic preservation......Page 278
Complete compiler......Page 281
Discussion......Page 283
Related work......Page 285
JinjaThreads as a Java interpreter......Page 287
Isabelle code extraction facilities......Page 288
The code generator......Page 289
The predicate compiler......Page 291
Data structures......Page 292
Locales and code extraction......Page 293
Generic well-formedness......Page 294
The bytecode verifier......Page 295
Type inference for source code......Page 297
The single-threaded semantics......Page 298
Schedulers......Page 300
Tabulation......Page 302
Efficiency of the interpreter......Page 303
Guidelines for executable formalisations......Page 306
The translator Java2Jinja......Page 308
The translation......Page 310
Validation......Page 313
Related Work......Page 315
Efforts and rewards of a machine-checked formalisation......Page 317
Experience: Working with Isabelle/HOL......Page 320
From Java light to JinjaThreads......Page 325
Comparison between Java and JinjaThreads......Page 327
Future work......Page 331
Conclusion......Page 333
Producer-consumer example......Page 337
Declarations and lookup functions......Page 341
Binary operators......Page 343
Sequential consistency......Page 345
The Java memory model......Page 347
Signatures......Page 348
Semantics of method clone......Page 349
Semantics of native methods......Page 350
Generic well-formedness......Page 353
Typing rules for expressions......Page 354
Definite Assignment......Page 356
Small-step semantics......Page 358
Observability......Page 364
Applicability and effect......Page 365
The virtual machine......Page 369
Observability......Page 374
The Java memory model......Page 375
Compilation stage 1......Page 378
Compilation stage 2......Page 379
Preprocessor......Page 383
List of Figures......Page 387
List of Tables......Page 391
Bibliography......Page 393
Index......Page 415