Concurrency: 2009-2010
Information
|
Lecturer |
|
|
Practical Coordinator |
|
|
Degrees |
Part A Core — Computer Science Part A — Mathematics and Computer Science Schedule A — MSc in Computer Science |
|
Term |
Hilary Term 2010 (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.
- 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 at the Department of Computer Science
|
Activities |