concur-cours

Lectures on Determinacy and Synchrony2008-2009MPRI C-2-3- Concurrence - Lectures 9-12Roberto AmadioUniversite Paris Diderot (Paris 7)Laboratoire Preuves, Programmes et Systemes1Programme of these lecturesWe will cover the notions of: Determinacy, Con uence, and Linearity. Synchrony and Time.In the framework of process calculi (speci cally, CCS, -calculus,and variations thereof).2Determinacy3What is a deterministic system?In automata theory, one can consider various de nitions. Forinstance, look at nite automata :Def 1 There is no word w that admits two computation paths inthe graph such that one leads to an accepting state and theother to a non-accepting state.Def 2 Each reachable con guration admits at most one successor.Def 3 For each state: either there is exactly one outgoing transition labelled with, or all outgoing transitions are labelled with distinct symbolsof the input alphabet.Thus one can go from ‘extensional’ conditions (intuitive but hardto verify) to ‘syntactic’ conditions (veri able but not as general).4Why did we allow non-determinism?Race conditions Two clients request the same service.a (a.P |a.P |a)1 2General speci cation and portability We do not want tocommit on a particular behaviour. For instance, considera,b (.a.b.c | a.b.d | b)Depending on the compilation, the design of the virtualmachine, the processors timing,... we might always run drather than c (or the other way around).5Why is determinism ...