Introduction Summary

Concurrency 1

Shared Memory

Catuscia Palamidessi

INRIA Futurs and LIX - Ecole Polytechnique

The other lecturers for this course:

Jean-Jacques Lévy (PPS) James Leifer (INRIA - Rocq)

Eric Goubault (CEA)

http://pauillac.inria.fr/˜ leifer/teaching/mpri-concurrency-2004/

Introduction Summary

Outline

1 Introduction

First Subsection Name Second Subsection Name

Introduction Summary Short First Subsection Name (Optional) Second Subsection Name

Motivation

Why Concurrency?

Programs for multi-processors Drivers for slow devices Human users are concurrent Distributed systems with multiple clients Reduce latency Increase efficiency, but Amdahl’s law

S = \frac{N}{b ∗ N + (1 − b)}

(S = speedup , b = sequential part, N processors)

Catuscia Palamidessi  Concurrency 1

Overview of the course

09-28  CP  Shared memory: atomicity
10-05  CP/JJL  Shared memory: verification, report on Ariane 501
10-12  CP  CCS: syntax and transitions, coinduction
10-19  CP  CCS: weak and strong bisimulations, axiomatization
10-26  CP  CCS: examples, Hennessy-Milner logic
11-02  JL  π-calculus: syntax; reduction, transitions, strong bisimulation
11-09  JL  π-calculus: sum, abstrations, data structures, bisimulation proofs
11-16  JL  π-calculus: bisimulation “up to”, congruence, barbed bisimulation
11-23  Review
11-30  MT exam
12-07  JL  π-calculus: comparison between equivalences
12-14  JJL  Expressivity of the pi-calculus and its variants
12-21  vacation
12-28  vacation
01-04  JJL  Distributed pi-calculus
01-11  JJL  Problems with distributed implementation
01-18  EG  True concurrency versus interleaving semantics
01-25  EG  Event structures and Petri nets
02-01  EG  Application to the semantics of CCS
02-08  EG  Comparison of the expressiveness of different models
02-15  Review
02-22  Final exam

Introduction Summary

Non-determinism

Let x be a global variable. Assume that at the beginning x = 0 Consider two simple processes

S = [x := 1; ] T = [x := 2; ]

After the execution of S || T , we have x ∈ {1, 2}

Conclusion:

Result is not unique.

Concurrent programs are not described by functions.

Introduction Summary

Implicit Communication

Let x be a global variable. Assume that at the beginning x = 0 Consider the two processes S = [x := x + 1; x := x + 1 || x := 2 ∗ x] T = [x := x + 1; x := x + 1 || wait(x = 1); x := 2 ∗ x]

After the execution of S, we have x ∈ {2, 3, 4} After the execution of T , we have x ∈ {3, 4} T may be blocked

Conclusion

The parallel subcomponents of a program may interact via their shared variables

Catuscia Palamidessi  Concurrency 1

Make Titles Informative.