1	Structured concurrent programming Tony Hoare Redmond July 2001
2	Summary Concurrency is a program structure Concurrent programs are testable Finite state machines define their behaviour.
3	Structured programming Sequential composition P ; Q ; R … Conditional choice { b ? Q : R } Repetition while b do { P } where P, Q, R stand for (parts of) programs
4	Single entry single exit
5	Implementation {b ? P : Q} { goto start ; thenclause : { P } ; goto done ; elseclause : { Q } ; goto done ; start : if ( b ) goto thenclause ; else goto elseclause ; done : ; }
6	Assertions If assert(b&pre) ; P ; assert(post) and assert((!b)&pre) ; Q ; assert(post) are both correctly asserted , then so is assert(pre) ; { b ? P : Q } ; assert(post)
7	Algebra The operator ; associates { P ; Q } ; R = P ; {Q ; R } And distributes back through conditional { b ? P : Q } ; R = { b ? {P ; R} : {Q ; R} } Unfolding while while b do {P} = { b ? {P ; while b do {P}} :}
8	Concurrent program structures P first Q run whichever starts first, the other is ignored P both Q run them concurrently, starting together, ending together P any Q run either of them, non-deterministic choice where P and Q stand for (parts of) programs
9	Example {Scanf (“%d”, &X ) both WaitForSingleObject (p, 3*seconds) both MatrixInvert (M, N)}
10	Implementation of P both Q {HANDLE temp [2] ; static void Pfunc( ) {P} ; static void Qfunc( ) {Q} ; temp [0] = CreateThread(NULL, 0, (LPTHREAD_START_ROUTINE)Pfunc, NULL, 0, NULL) ; temp[1] = CreateThread(NULL, 0, (LPTHREAD_START_ROUTINE)Qfunc,NULL, 0, NULL) ; WaitForMultipleObjects(2,temp,TRUE,INFINITE) ;}
11	Pipeline server { P both Q } ; R ACTIONS PCLASS::Pfunc (void) {P ; return Complete( ) ;} ; ACTIONS QCLASS::Qfunc (void) {Q ; return Complete ( ) ;} ; ACTIONS RCLASS::Rfunc (void) {R ; return Complete ( ) ;} ; // the program starts here new PCLASS::Pfunc ; new QCLASS::Qfunc; return (WaitForChildren (Rfunc) ) ;
12	Other implementations On separate processors, communicating over the web. Transformed to a sequential process on a single processor. Decision can be postponed to load time, or even to run time (VULCAN).
13	Process algebra All three operators associate and commute They all distribute through any, which distributes through first .
14	A process is a program part that interacts with other program parts and with its environment by a sequence of synchronised events. Examples: a thread, an object, a COM component, a monitor, a fiber, an integer variable, a Finite State Machine (FSM) … Let P, Q, R, … stand for processes.
15	An event is an atomic action that either succeeds or has no effect. For example: an input, an output, a lock acquisition or release, a button click, a variable access or update, … Let A, B, C,… stand for events.
16	The alphabet of a process is the set of shared events (eg. channels, ports, locks, …), through which it interacts with its environment. In the simple case, each event (channel) is shared by just two processes: one signals (sends), the other waits (receives). Sending and receiving occur simultaneously
17	The trace of a process is a sequence recording all its interactions with its environment, e.g., trace = <console_input (3), output (7),…> assertions describe the trace, e.g., scanf ( “%d” , &X ) ; assert ( last_of (trace) == console_input ( X ) ) ;
18	System structure Alphabet ( Proc1) = { B, C }
19	Finite State Machines describe behaviour of a process
20	The first transition
21	The next transition
22	Its text alphabet = { A, B } ABstar = do { A ; B } while true ; Abstar = A ; B ; ABstar
23	Its invariant assertion inv_assert ( trace = < A, B, A, …, A > or trace = < A, B, A, …, B> or trace = <>) ; More briefly, inv_assert ( #A – 1 < #B < #A )
24	A then B then P
25	{A then P} first {C then Q}
26	P any Q
27	{A both D} then P
28	P both Q Events in both their alphabets happen when they both are ready. Events in the alphabet of only one of them happen when that one is ready. The resulting alphabet includes all the events in either alphabet.
29	Another State Machine
30	ABstar both BCstar
31	The assertion rule for both If {P} inv_assert (Pspec) and {Q} inv_assert (Qspec) are both correctly asserted, then so is {P both Q} inv_assert (Pspec & Qspec) … (under certain conditions) …
32	The concurrent behaviour {ABstar both BCstar} inv_assert ( #A – 1 < #B < #A & #B – 1 < #C < #B ) ; from which it follows that inv_assert ( #A – 2 < #C < #A )
33	Conclusion Structured concurrent programming promises benefits similar to those of structured sequential programming. The benefits will be increased by building the relevant theory into programmer productivity tools.
34	Acknowledgements Robin Milner, Bill Roscoe; Michael Parkes; Luca Cardelli, Andy Gordon, Cedric Fournet; Jakob Rehof, Sriram Rajamani, Tom Ball; Greg Meredith, Andrew Herbert, Ralph Becket, …