Concurrency: 2008-2009

Lecturer

James Worrell

Degrees

Part A Core — Computer Science

Part A — Mathematics and Computer Science

ECS Part I — MEng Engineering and Computing Science

Schedule A — MSc in Advanced Computer Science

MSc by Research

MSc in Mathematics and Foundations of Computer Science

Term

Michaelmas Term 2008 (16 lectures)

Overview

Computer networks, multiprocessors and parallel algorithms, though radically different, all provide examples of processes acting in parallel to achieve some goal. All benefit from the efficiency of concurrency yet require careful design to ensure that they function correctly. The concurrency course introduces the fundamental concepts of concurrency using the notation of Communicating Sequential Processes. By introducing communication, parallelism, deadlock, live-lock, etc., it shows how CSP represents, and can be used to reason about, concurrent systems. Students are taught how to design interactive processes and how to modularise them using synchronisation. One important feature of the module is its use of both algebraic laws and semantic models to reason about reactive and concurrent designs. Another is its use of FDR to animate designs and verify that they meet their specifications

Learning outcomes

At the end of the course the student should:

understand some of the issues and difficulties involved in Concurrency
be able to specify and model concuurent systems using CSP
be able to reason about CSP models of systems using both algebraic laws and semantic models
be able to analyse CSP models of systems using the model checker FDR

Synopsis

Processes and observations of processes; point synchronisation, events, alphabets. Sequential processes: prefixing, choice, nondeterminism. Operational semantics; traces; algebraic laws. [3]
Recursion. Complete partial orders and fixed points as a means of explaining recursion; approximation, limits, least fixed points; guardedness and unique fixed points. [1]
Concurrency. Hiding. Renaming. [3]
Non-deterministic behaviours, refusals, failures; the determinism ordering. [2]
Hiding and divergence, the failures-divergences model. [1]
Specification and correctness. [2]
Communication, pipes, buffers. Sequential composition. [2]
Case study. [2]

Syllabus

Deterministic processes: traces, operational semantics; prefixing, choice, concurrency and communication. Nondeterminism: failures and divergences; nondeterministic choice, hiding and interleaving. Further operators: pipes and (time permitting) sequential composition. Refinement, specification and proof. Process algebra: equational and inequational reasoning.

Reading list

Course Text

A. W. Roscoe, The Theory and Practice of Concurrency, Chapters 1-7, Prentice-Hall International, 1997.

Alternatives:

C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall International, 1985, http://www.usingcsp.com.
S. A. Schneider, Concurrent and Real-time Systems, Chapters 1-8, Wiley, 2000.

Related research

Activities

Concurrency

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.