| |
| 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.
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.
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
- existing support for synchronization and coherence in
both the multiprocessor and distributed memory world;
- consistency models and their effect on language design; and
- emerging support for transactional memory and how it might be
incorporated into language design and implementation.
Lecture Slides:
|
|
