Introduction and Foundational Theory

Introduction: Formal Methods in Concurrent and Distributed Computing Dan Grossman

Type-Safe and Version-Safe Distributed Programming Peter Sewell
These lectures will discuss the main programming language design issues addressed in the Acute language, which supports type-safe and abstraction-safe communication, rebinding to local resources, version change, and computation mobility. Acute is an extension of an OCaml core, and the implementation of Acute has proven expressive enough for a wide variety of distributed applications. These lectures will begin with an introduction to the pi-calculus and the type theory underlying ML-style module systems, both of which form the basis of the Acute language.

Language-Based Techniques for Distributed Systems Robert Harper
Large-scale distributed computing is an appealing approach for making more effective use of computational resources attached to the Internet. Making effective use of resources distributed in this setting, however, requires overcoming significant technical hurdles. In these talks, we will investigate language-based techniques for disseminating distributed computations. We will look at the problem of trust, and show how certified compilation can enforce safety and security and thereby enable trustless grid computing. We will also investigate the foundations of distributed programming, and show how an intuitionistic modal logic can model portability of code, locality of resources, and distributed control flow.

Architectural Support for Concurrency Sandhya Dwarkadas
Traditional support for concurrency has involved either message-based communication or cache-coherent shared memory. The latter is generally considered easier to program, but traditionally comes with the conceptual difficulties of lock-based synchronization — ensuring maximum concurrency while avoiding correctness issues. One emerging alternative is support for transactional memory (borrowing from the database world). The goal of these lectures is to foster discussion between the programming language and architecture communities in order to enhance support for concurrency.
We will describe

  1. existing support for synchronization and coherence in both the multiprocessor and distributed memory world;
  2. consistency models and their effect on language design; and
  3. emerging support for transactional memory and how it might be incorporated into language design and implementation.
Lecture Slides:


This page is the property of the University of Oregon