Concurrent Processes

Module aims

The course is motivated by the increasing need for a theory of concurrent process in real systems and languages. Classroom sessions will include traditional lectures and some supervised problem solving, which are designed to illustrate the principles. The lab sessions will use one of the main stream programming languages for distributed communications and protocol description languages. 

The course provides the theories and techniques to analyse concurrent computations based on the basic mathematics behind process algebra and their type systems. The course will look at principles of concurrent message passing programming and software, addressing specification and design of message passing languages and distributed protocols. You will learn the application areas of concurrent processes and their type systems, including actor-based programs (such as Scala), channel-based programs (such as Go), network protocols (such as SMTP/HTTP), robotics programming and microservices.

More specifically students will:
1. Gain familiarity with the operational semantics and theory of concurrent processes
2. Learn the principles to evaluate various process calculi in the literature and examine their expressiveness
3. Learn a type theory of concurrency and communications in order to specify and verify message-passing communications
4. Practise  concurrent  processes  and  type theory via several  applications  --  network  protocols,  program  analysis, and concurrent robotics.

5. Be able to apply the taught techniques of concurrency theories to ensure correctness of concurrent applications such as deadlock-freedom and type/communication safety. 

Learning outcomes

After the course, students should be able to:

  1. specify message-passing controls using concurrent processes
  2. evaluate expressiveness of concurrent processes
  3. apply a basic type theory for concurrency and communications
  4. create specifications to verify concurrent programs and distributed protocols
  5. apply concurrent process theory and types to guide design and prove  behavioural correctness (deadlock and liveness)
  6. create specifications for network protocols which ensure deadlock-freedom and type safety and implement the protocols 

Module syllabus

1. Core process calculi (the pi-calculus)

a.    asynchrony/synchrony
b.    syntax/operational semantics/example

2.    Evaluation of Expressiveness

a.    synchronous pi-calculus
b.    polyadic pi-calculus
c.    recursive agents
d.    higher-order processes

3.    Session types and processes

a.    session processes syntax/semantics
b.    session type specifications
c.    session typing system
d.    type -safety

4.    Multiparty session types 

a.    multiparty session protocols
b.    multiparty session typing system
c.    a domain specific language for protocols 

5.    Applications (b--e) will be selected depending on the students

a.    Network protocols (in Java)
b.    Scala/Dotty   
c.    Go programming language 
d.    F#
e.    Robotics programming

Teaching methods

  • 7 weeks of 2 hours of lecture + 2 hour of tutorial or lab
  • 1 revision lecture (one hour) at the end of the course

Assessments

1. a basic process calculus (syntax and semantics of the pi-calculus)  (1,2 in ILOs)
2. session types (typing systems, semantics and type derivations of the session pi-calculus) (3,4,5,6 in ILOs)

Both are theoretical courseworks. 

Students will submit their coursework electronically and TAs and I will mark and return (standard marking for theoretical courseworks).

There will be the detailed feedback which will include (1) written feedback on the submissions; and (2) class-wide feedback explaining common pitfalls and suggestions for improvement.

Reading list

Core

Supplementary

Module leaders

Professor Nobuko Yoshida