cours.4

Informations

• Publié par: Uprou
• Nombre de lectures: 9
• Langue: English

Extrait

Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
Outline
Concurrency 3
CCS - Syntax and transitions, Equivalences
1 Introduction
Motivations
Catuscia Palamidessi
Principles in CCS design
INRIA Futurs and LIX - Ecole Polytechnique
The other lecturers for this course: 2 Syntax and Operational Semantics of CCS
Syntax
Jean-Jacques Lévy (INRIA Rocquencourt) Labeled transition System
James Leifer (INRIAt) What equivalence for CCS?
Eric Goubault (CEA)
http://pauillac.inria.fr/˜leifer/teaching/mpri-concurrency-2005/
1 2
Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
Motivations Motivations
Why a Calculus for Concurrency? Inadequacy of standard models of computations
The Calculus for Communicating Systems (CCS) was
developed by R. Milner around the 80’s.
The! calculus, the Turing machines, etc. are computationally
Other Process Calculi were proposed at about the same complete, yet do not capture the features of concurrent
time: the Theory of Communicating Sequential Processes computations like
by T. Hoare and the Algebra of Communicating
Interaction and communicationby J. Bergstra and J.W. Klop.
Inadequacy of functional denotationResearchers were looking for a calculus with few,
Nondeterminismorthogonal mechanisms, able to represent all the relevant
concepts of concurrent computations. More complex Note: nondeterminism in concurrency is different from the
mechanisms should be built by using the basic ones. nondeterminism used in Formal Languages, like for instance
the Nondeterministic Turing Machines.To help understanding / reasoning about / developing
formal tools for concurrency.
To play a role, for concurrency, like that of the!-calculus for
sequential computation.
3 4Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
Motivations Motivations
A few words about nondeterminism A few words about nondeterminism
0
In standard computation In standard computation
theory, if we want to compute theory, if we want to compute0 fail
the partial function f s.t. the partial function f s.t.
1f(0) = 1, a Turing Machine f(0) = 1, a Turing Machine success
like this one is considered ok
fail like this one is considered ok
1
However, we would not be
success However, we would not be coin coin
happy with a coffee machine happy with a coffee machine
that behaves in the same that behaves in the same
fail coffeeway way
success
5 6
Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
Motivations Motivations
Nondeterminism in sequential models Nondeterminism in concurrent models
Nondeterminism may arise because of interaction between
Convenient tool for solving certain problems in an easy processes.
way or for characterizing complexity classes (examples:
search for a path in a graph, search for a proof etc.) The characteristics of nondeterminism in this setting:
It cannot be avoided. At least, not without loosing essentialExamples of nondeterministic formalisms:
parts of expressive power. All interesting models ofThe nondeterminismistic Turing machines
concurrency cope with nondeterminism.Logic languages like Prolog and! Prolog Failures do matter. Chosing the wrong branch might bring
to an "undesirable situation". Backtracking is usually notThe characteristics of nondeterminism in this setting:
applicable (or very costly), because the control isIt can be eliminated without loss of computational power by distributed: we should restart not one but severalusing backtracking. processes.
Failures don’t matter: all what we are interested on is the
existence of succesful computations. A failure is reported Hence controlling nondeterminism is very important. In
only if all possible alternatives fail. sequential programming is just a matter of efficiency, here is a
matter of avoiding getting stuck in a wrong situation.
7 8Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
Principles in CCS design Principles in CCS design
The basic kind of interaction (1/2) The basic kind of interaction (2/2)
A calculus should contain only the primary constructs. For
instance, the primary form of interaction. But what is the primary
In CCS, the fundamental model of interaction is synchronous andform of interaction?
symmetric, i.e. the partners act at the same time performing
complementary actions.In general, concurrent languages can offer various kinds of
communication. For instance: This kind of interaction is called handshaking: the partners agree
simoultaneously on performing the two (complementary) actions.Communications via shared memory.unication via channels.
In Java there is a separation between active objects (threads) andComm via broadcasting.
passive objects (resources). CCS avoids this separation: Every
and we could make even more distinctions (non-elementary) entity is a process.
one-to-one / one-to-many For instance, consider two proceesses P and Q communicating via a
Ordered / unordered (i.e. queues / bags) buffer B. in CCS also B is a process and the communication is between
Bounded / unbounded. P and B, and between Q and B.
So what is the basic kind of communication?
For CCS the answer was: none of the above!
9 10
Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
Principles in CCS design Syntax
Example: P and Q communicating via a buffer B Syntax of CCS
ports (or channels) (channel, port) names: a,b,c, . . .
¯ ¯¯ ¯co-names: a,b,c, . . . Note: a = a
a b silent action: !
P B Q
¯actions, prefixes: µ ::= a | a | !
processes: P,Q ::= 0 inaction
| µ.P prefix
let B = a(x).b(x).B , P = a(d).P' , Q = b(y).Q'[y] | P | Q parallel
| P + Q (external) choice
in P | B | Q | ("a)P restriction
| rec P process P with definition K = PK
| K (defined) process nameco-actions
parallel operator sequential operator
11 12"
Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
Labeled transition System Labeled transition System
Labeled transition system Structural operational semantics
The transitions of CCS are defined by a set of inductive rules.
The system is also called structural semantics because the
evolution of a process is defined in terms of the evolution of its
The semantics of CCS is defined by in terms of a labeled components.
transition system, which is a set of triples of the form
µ !P! P µ=a,aµ [Act] [Res]µ µ !P ! Q µ.P! P (!a)P! (!a)P
µ µ! !P! P Q! QMeaning: P evolves into Q by making the action µ. [Sum1] [Sum2]µ µ! !P+Q! P P+Q! Q
The presence of the label µ allows us to keep track of the
µ µ! !P! P Q! Qinteraction capabilities with the environment. [Par1] [Par2]µ µ! !P|Q! P |Q P|Q! P|Q
µa a !! ! P[rec P/K]! PP! P Q! Q K[Com] [Rec]! µ! ! !P|Q! P |Q rec P! PK
13 14
Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
Labeled transition System What equivalence for CCS?
Some examples Motivation
a.0 | a.0 (v a) (a.0 | a.0)
The restriction can be
a a used to enforce
It is important to define formally when two system can besynchronization0 | a.0 t a.0 | 0 t
considered equivalent
a a
The parallel operator There may be various "interesting" notion of equivalence, it
0 | 0 (va) (0 | 0) may cause infinitely depends on what we want (which observables we want to
many different states preserve)
rec a.k | a.k
k A good notion of equivalence should be a congruence, soThe fragment of therec a.k + b.0
krec a.k a ak to allow modular verificationcalculus without parallel
b
operator generates onlya a
a aa finite automata / regular
trees
15 16Introduction Syntax and Operational Semantics of CCS Introduction Syntax and Operational Semantics of CCS
What equivalence for CCS? What equivalence for CCS?
Examples: possible definitions of a coffee machine Exercises
rec coin.(coffee.ccup.K + tea.tcup.K)K
coin.rec (coffee.ccup.coin.K + tea.tcup.coin.K) Define in CCS a semaphore with initial value nK
Show that maximal trace equivalence is not a congruencerec (coin.coffee.ccup.K + coin.tea.tcup.K)K in CCS. By traces here we mean the traces of all
possible (finite or infinite) maximal runs.Question: which of these machines can we safely consider
equivalent?
Note that these machines have all the same traces.
17 18