Disentanglement is a run-time property of parallel programs ensuring that a thread does not use (read or write) any memory objects allocated by another concurrently executing thread. Disentanglement enables important efficiency and scalability benefits, in particular for parallel allocation and reclamation (garbage collection) of memory. Whereas disentanglement holds naturally in purely functional programs, it can be destroyed by shared memory mutation.
In this talk, I will present ongoing work on the development of a type system for an eager functional programming language with references that ensures disentanglement for well-typed programs. The type system introduces the notion of a time as the static abstraction of a thread. Types and typing judgments are extended with times, akin to modal worlds, indicating the allocating and executing thread, respectively. To ensure disentanglement, the type system imposes an order on times, reflecting the fork-join structure of the program, and restricts mutations to be consistent with this order. I will discuss the main ideas of the type system, including the new features of a J conversion and polychronic function. The former allows times to be reinterpreted at join points, the latter allows a function to be polymorphic in the (time of the) invoking thread.
Joint work with Sam Westrick and Umut Acar.
Stephanie Balzer is a research faculty in the Principles of Programming group in the Computer Science Department at Carnegie Mellon University. Stephanie’s current work focuses on the development of type systems and logics for verifying properties of concurrent programs.
Faculty Host: Jan Hoffmann
Zoom Participation. See announcement.