Please note: This seminar will take place in DC 2314.
Philipp
Haller,
Associate
Professor
KTH
Royal
Institute
of
Technology
Concurrent programming is notorious for hazards such as data races and deadlocks. At the same time, program executions are difficult to reproduce due to various sources of nondeterminism, complicating the debugging of concurrent programs. These challenges have motivated work on ensuring safety statically using type systems. Type-based prevention of data races is a major challenge in the context of object-oriented programming languages due to pervasive mutation and aliasing. In addition, extending the type systems of existing languages is a challenge, preventing recent advances from practical use.
This talk presents LaCasa, a language and type system extending Scala with uniqueness typing and heap isolation. Goals of the language extension include (a) integrating with the full Scala language, (b) minimizing the overhead of type annotations, and (c) enabling the reuse of existing code without source code changes. We show how LaCasa prevents data races in concurrent programs based on the actor model. We then present a variant, Parallel LaCasa, which extends data-race safety to the Async-Finish model. Finally, we discuss the relation to deterministic concurrent programming models.