概要

シラバス 並行計算の概念および体系について修得する。特に、通信プロセス計算モデルの表現と意味論について講義し、従来の逐次計算モデルと比較して、並行計算によって生じる問題について、体系的な意味づけとその対処方法について学ぶ。ネットワークを介した情報システムにおける並行計算の具体的イメージを通して信頼性の高い並行ソフトウェアの構築、時間を含むシステムの振舞い、さらに、具体的な信頼性向上のための形式手法としてモデル検査について述べる。

並行分散計算特論
Shoji Yuen

2011/10/4

キーワード 並行計算モデル、プロセス計算、時間オートマトン、モデル検査、様相論理

H23 並行分散計算特論

2011/10/4

1/18

H23 並行分散計算特論

2011/10/4

2/18

Formal semantics for working programmers

講義予定
1. 概論

• Rigorous mathematical model

2. 並行計算モデル

P = Q, P ≤ Q, Γ, prop |= P, Γ  p : prop

3. ラベルつき遷移系• Correct Design Principle• Compositionality

4. 双模倣関係と等価性
5. 双模倣に基づく意味論

Sometimes “over rigorous”• Obstacles and limitations:

6. プロセス計算
7. 時間オートマトン• Computability• Full–abstractness• Complexity• Scaleability

8. モデル検査
9. 様相論理による振舞の表現
資料は英語でつくる予定。
教科書については入手困難なものはホームページからダウンロー
ド (パスワードつき)
H23 並行分散計算特論

2011/10/4

Cost/eﬀectiveness ratio

3/18

H23 並行分散計算特論

2011/10/4

4/18

Communicating Processes

Communicating Processes

Parallel compositon of transition systems

Parallel compositon of transition systems

bacbb

Synchronization by label matchingacb

Synchronization by label matching
without synchronization: (ab)∗ ||(bc)∗with synchronization: a(b(a|c))∗

H23 並行分散計算特論

2011/10/4

5/18

Communication structure

2011/10/4

2011/10/4

5/18

Communication structure• Basic Mechanism• Handshake (synchronous)• Mailbox (asynchronous)• Conﬁguration• Fixed (static structure)• Variable (dynamic structure)

H23 並行分散計算特論

H23 並行分散計算特論• Basic Mechanism• Handshake (synchronous)• Mailbox (asynchronous)• Conﬁguration• Fixed (static structure)• Variable (dynamic structure)

6/18

H23 並行分散計算特論

2011/10/4

6/18

Behavioral semantics

Algebraic Approach
Algebraic Characterization
Based on CCS (Milner:1980,1989)• Semantics of a program (Continuous) Function f (x)Behavior is an equivalence over terms

Classical I/O system⇒ An algebra of behavior• Input = parameters• Output = evaluated value

Communicating system

P=Q??Appropriate I/O correspondence??

For all operations F in the calculus:
F (P) = F (Q) when P = Q

Domains of ’interactional behaviors?
A program be a function over the behavior domain“P behaves exactly like Q”

Process algebra (P, =): P:Set of process terms
Processes = communicating (concurrent) programs

H23 並行分散計算特論

2011/10/4

7/18

H23 並行分散計算特論

Semantics of Programs

The (classical) theory of automata

Equivalence relation ∼ over program terms

Deﬁnition
Automaton
Given a set of actions Act:A = Q, q0 , F, T 

P∼Q• Q:Set of states;

Finest algebra:term algebra(all programs are distinguished if any syntactic diﬀerence.)• q0 ∈ Q:the start state;• F ⊆ Q:the accepting states; andUsuallyunacceptable• T ⊆ Q × Act × Q:the transtionsa(q, a, q  ) ∈ T is written as q → q  . A is ﬁnite if |Q| is ﬁnite. A isadeterministic if |{q  | q → q  }| = 1 for all q, a.

?Appropirate Equivalence (or preorder)?
Coarsest algebra = singleton
all programs are identical.
H23 並行分散計算特論

2011/10/4

8/18

Behavior of automata

Formal semantics=a mathematical structure corresponding to programs

1 + 1 = 2

2011/10/4

9/18

H23 並行分散計算特論

2011/10/4

10/18

Transition graph

Semantics of automata

A ﬁnite automata A0 over {a, b, c}
a,b,cb,cq0

q3

Deﬁnition

a,bAn automaton: A = Q, q0 , F, T wÂ = {w |q0 → q, q ∈ F}
waaq2a aac→=→1 →2 · · · →2 where w = a1 , . . . , an
A1 ∼ A2 if Aˆ1 = Aˆ2bq1

A pair of automata are equal if they accept the same language.

c

H23 並行分散計算特論

2011/10/4

11/18

H23 並行分散計算特論

Regular sets

2011/10/4

12/18

Arden’s Rule

Operation over sets

Proposition

S1 ∪ S2 (Union)
S1 · S2 = {w1 · w2 |w1 ∈ S1 , w2 ∈ S2 }S ∗ = {ε} ∪ S ∪ S · S ∪ S · S · S ∪ · · ·For any sets of strings S and T :X = S · X + T has X = S ∗ · T as a solution. Moreover, thissolution is unique if ε ∈/SRegular setDeﬁnition

X0 = aX1 + bX3 + cX3

A set of strings over Act is regular if it is constructed applying
following rules:

X1 = aX3 + bX2 + cX0 + ε
X2 = aX3 + bX3 + cX0• ∅, {a} are regular;

X3 = aX3 + bX3 + cX3• S1 ∪ S2 is regular if both S1 and S2 are regular;• S1 · S2 is regular if both S1 and S2 are regular;

Using the Arden’s rule:Aˆ0 = a((bc + c)a)∗• S ∗ is regular if S is regular
H23 並行分散計算特論

2011/10/4

13/18

H23 並行分散計算特論

2011/10/4

14/18

DFA and NFA

VM1

A1cr2r0acoin
coin
r2bbacccar1

VM2

juice
buttoncoinr1

To get a juice:
Put one coin and push button
To get a beer:
Put two coinsCorrectness:
one coin for juice
two coins for beer

beer

r1
Aˆ1 = Aˆ2

juice
buttonA2cr0

Vending Machine

Cold Juiceand Beer!

coincoinbeer

H23 並行分散計算特論

VM1

15/18

Vending Machine
juice
buttoncoin
coin

VM1

To get a juice:
Put one coin and push button
To get a beer:
Put two coinscoin

To get a juice:
Put one coin and push button
To get a beer:
Put two coinsjuice
coin

Cold Juiceand Beer!

16/18

Correctness:
one coin for juice
two coins for beer

beer

button

coin

juice
coin

VM2

2011/10/4

Vending Machine
buttonjuice
coin

H23 並行分散計算特論

Correctness:
one coin for juice
two coins for beer

beer
VM2

2011/10/4

buttonCold Juiceand Beer!

coin

coin

coin

beerbeer
H23 並行分散計算特論

2011/10/4

16/18

H23 並行分散計算特論

2011/10/4

16/18

VM1

Vending Machine
juice
buttoncoin
coin

To get a juice:
Put one coin and push button
To get a beer:
Put two coins

coinbuttonjuice
buttoncoin

Cold Juiceand Beer!

coin
juice

beer

VM1

button
coin
coin

16/18

VM1

To get a juice:
Put one coin and push button
To get a beer:
Put two coins

coinbuttonCold Juiceand Beer!

coin

coin

coin
beer

beer
H23 並行分散計算特論

To get a juice:
Put one coin and push button
To get a beer:
Put two coins

juice
coin

Cold Juiceand Beer!

16/18

Correctness:
one coin for juice
two coins for beer

beer

button

coin

juice
coin

VM2

2011/10/4

Vending Machine
buttonjuice
coin

H23 並行分散計算特論

Correctness:
one coin for juice
two coins for beer

beer
VM2

2011/10/4

beer

Vending Machine
juice

Cold Juiceand Beer!

coin

coin

H23 並行分散計算特論

To get a juice:
Put one coin and push button
To get a beer:
Put two coins
Correctness:
one coin for juice
two coins for beer

beer
VM2

coin

juice
coin

juice
coin

Vending Machine
buttonCorrectness:
one coin for juice
two coins for beer

beer
VM2

VM1

2011/10/4beer
16/18

H23 並行分散計算特論

2011/10/4

16/18

VM1

Vending Machine
juice
buttoncoin
coin

To get a juice:
Put one coin and push button
To get a beer:
Put two coins

coinbuttonjuice
buttoncoin

Cold Juiceand Beer!

coin

beer

beer
H23 並行分散計算特論

2011/10/4

16/18

Vending Machine
juice
buttoncoin
coin

VM1To get a juice:
Put one coin and push button
To get a beer:
Put two coins

coinbuttonCold Juiceand Beer!

coin

coin

coin
juice

beer
H23 並行分散計算特論

To get a juice:
Put one coin and push button
To get a beer:
Put two coins

juice
coin

Cold Juiceand Beer!

16/18

Correctness:
one coin for juice
two coins for beer

beer

button

coin

juice
coin

VM2

2011/10/4

Vending Machine
buttonjuice
coin

H23 並行分散計算特論

Correctness:
one coin for juice
two coins for beer

beer
VM2

Cold Juiceand Beer!

coin

coin

VM1

To get a juice:
Put one coin and push button
To get a beer:
Put two coins
Correctness:
one coin for juice
two coins for beerbeer
VM2

coin

juice
coin

juice
coin

Vending Machine
buttonCorrectness:
one coin for juice
two coins for beerbeer
VM2

VM1

2011/10/4

beer
16/18

H23 並行分散計算特論

2011/10/4

16/18

VM1

Vending Machine
juice
buttoncoin
coin

To get a juice:
Put one coin and push button
To get a beer:
Put two coins

coinbuttonjuice
buttoncoin

Cold Juiceand Beer!

coin

beer
2011/10/4

16/18

Vending Machine
juice
buttoncoin
coin

H23 並行分散計算特論

VM1

To get a juice:
Put one coin and push button
To get a beer:
Put two coins

coinbuttonTo get a juice:
Put one coin and push button
To get a beer:
Put two coins

juice
coin

Cold Juiceand Beer!

16/18

Correctness:
one coin for juice
two coins for beer

beer
VM2

coin

juice
coin

juice

2011/10/4

Vending Machine
buttonCorrectness:
one coin for juice
two coins for beer

beer

coin

beer

beer
H23 並行分散計算特論

VM2

Cold Juiceand Beer!

coin

coin

VM1

To get a juice:
Put one coin and push button
To get a beer:
Put two coins
Correctness:
one coin for juice
two coins for beer

beer
VM2

coin

juice
coin

juice
coin

Vending Machine
buttonCorrectness:
one coin for juice
two coins for beer

beer
VM2

VM1

buttonCold Juiceand Beer!

coincoin

coin

beer

beer
H23 並行分散計算特論

2011/10/4

16/18

H23 並行分散計算特論

2011/10/4

16/18

Correct vending machine?

Correct vending machine?

Intuitively VM1 is correct and VM2 is broken.

Intuitively VM1 is correct and VM2 is broken.

Why?

H23 並行分散計算特論

2011/10/4

17/18

H23 並行分散計算特論

Correct vending machine?

A reactive system behavior is not fully characterized by languages!
Necessary to have an alternative equivalence notion to distinguish:

Why?

p1ap0

A customer has control in VM1 , but a machine has control in VM2 .
PDiﬀernce is recognized during the interaction.

2011/10/4

17/18

Reactive system

Intuitively VM1 is correct and VM2 is broken.

H23 並行分散計算特論

2011/10/4

17/18

bp2q0ap3cp4

H23 並行分散計算特論

q2bQ

2011/10/4

aq1cq3

18/18