Type-safe multithreading in cyclone

9 years 4 months ago
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
Dan Grossman
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where TLDI
Authors Dan Grossman
Comments (0)