HOME | DEUTSCH | IMPRESSUM | KIT

Conference Papers: Type Safe Nondeterminism - A Formal Semantics of Java Threads

[lochbihler08fool]Andreas Lochbihler, Type Safe Nondeterminism - A Formal Semantics of Java Threads, International Workshop on Foundations of Object-Oriented Languages (FOOL 2008), January 2008.

Abstract

We present a generic framework to transform a single-threaded operational semantics into a semantics with interleaved execution of threads. Threads can be dynamically created and use locks for synchronisation. They can suspend themselves, be notified by other threads again, and interact via shared memory. We formalised this in the proof assistant Isabelle/HOL along with theorems to carry type safety proofs for the instantiating semantics (progress and preservation in the style of Wright and Felleisen) over to the multithreaded case, thereby investigating the role of deadlocks and giving an explicit formalisation for them. We apply this framework to the Java thread model using an extension of the Jinja source code semantics to have type safety for multithreaded Java machine-checked. The Java Memory Model is not included.

Download

  [PDF]

BibTeX

Authors at the institute

Former Staff Member
Dr. rer. nat. Andreas Lochbihler

Projects

Project
Quis-Custodiet