Type-safe multithreading in cyclone

We extend Cyclone, a type-safe polymorphic language at vel of abstraction, with threads and locks. Data races can violate type safety in Cyclone. An extended type system statically guarantees their absence by enforcing that thread-shared data is protected via locking and that threadlocal data does not escape the thread that creates it. The extensions interact smoothly with parametric polymorphism and region-based memory management. We present a forract machine that models the need to prevent races, a polymorphic type system for the machine that supports thread-local data, and a corresponding type-safety result. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features—concurrent programming structures, polymorphism; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—operational semantics General Terms Languages Keywords data races, types, Cyclone

• Type: Conference
• Year: 2003
• Where: TLDI
• Authors: Dan Grossman
• Keywords: Data Races, Formal Methods, Languages Keywords Data, TLDI 2003, Type-safe Polymorphic Language