A Deadlock-Free Semantics for Shared Memory Concurrency

Abstract. We design a deadlock-free semantics for a concurrent, functional and imperative programming language where locks are implicitly and univocally associated with pointers. The semantics avoids unsafe states by relying on a static analysis of programs, by means of a type and effect system. The system uses singleton reference types, which allow us to have a precise information about the pointers that are anticipated to be locked by an expression.

• Type: Conference
• Year: 2009
• Where: ICTAC
• Authors: Gérard Boudol
• Keywords: Applied Computing, Avoids Unsafe States, Deadlock-free Semantics, ICTAC 2009, Imperative Programming Language