process-calculus-basic.ppt

(1)

Ichiro Satoh 国立情報学研究所

佐藤一郎

E-mail: [email protected] Ichiro Satoh 講義資料のPDFを下記のURL

http://research.nii.ac.jp/~ichiro/

から辿れるようにする Ichiro Satoh   物流用コンテナにサーバ格納   コンテナ一個に1000台以上の   コンテナに刺さっているホースは冷水を引き入れと、サーバーの冷却に利用した後の温水の排出 Rackableの工場 Ichiro Satoh •  データセンターの電力消費の？？％は冷却コスト •  データセンターの省電力化 ‒  狭い密閉された空間で熱い空気を冷やす ‒  水冷を使用する •  現在、省電力効率の良いデータセンターはコンテナ形 HPのコンテナ型データセンターのPUEは1.25 Googleのコンテナ型データセンターのPUEは1.19 国内の最新データセンターのPUEは2 (普通は4 5) PUE = データセンタ全体の消費電力／ IT機器による消費電力

(2)

Ichiro Satoh   クラウド・コンピューティング

≒ ユーティリティ・コンピューティング

  ユーティリティ・コンピューティングはNicholas G. Carｒが著書The Big Switchの中でした定義   コンピューティング(計算能力)が集約化し、ユーティリティ(電力･ガス･水道)化した状態を示す。   つなげばいつでも使えるコンピュータ   Finacial TimesやEconomist クラウドコンピューティング特集   一般への認知 Ichiro Satoh   計算能力を対規模に集約したデータセンターから、必要な人に、必要なときだけ計算能力をネットワークを介して提供する。   いまの発電所と家庭・工場との関係モデル   従量課金(初期投資が不要）   規模の経済   データセンターへの莫大な資金の投資   GoogleやMicrosoftが一つのデータセンターに投資する金 額は1500億円   管理の効率化   Microsoftでは一人で5000台のサーバーを管理する。   大規模且つ高効率で運用し計算能力の単価を下げる Ichiro Satoh   コンピューティングをアウトソーシングする形態のひとつ   スケールアウトが容易な大規模分散システム   価格性能比の高い安価なサーバ数千台数十万台で構成   ハードウェア障害を許容し、システム全体でカバークラウドコンピューティングインフラ分散キュー分散アプリケーションサーバ分散ストレージデータベースデータベースデータベースロードバランサー Ichiro Satoh   Software-as-a-Service（SaaS）ではない   SaaSは大規模なスケーラビリティを提供するわけではない（PaaSも同じ）   ユーティリティコンピューティングではない   電気やガスのように必要なだけのサービスを受け、それに応じて代価を払うという利用形態の名称   Grid Computingではない   Grid Computingは相異な組織のコンピュータを連携させて、膨大な計算や データを扱うための方法（あまりクラウドではGCの技術は使っていない） ＳａａＳプロバイダー CRMなどのアプリケーションサードパティのアプリケーションユーザ開発のアプリケーションデータベースインターネットサービスの提供システムの運用・保守をアウトソーシング SaaS

(3)

Ichiro Satoh   HaaS（Hardware as a Service）/ IaaS (Infrastructure as a Service)

  サーバやストレージなどの(仮想)ハードウェアを提供、例：Amazon EC2 (Elastic Compute Cloud)、S3 (Simple Storage Service)

など

  DaaS（Database as a Service）

  データベース機能を提供、例：Amazon.comの

SimpleDB、MicrosoftのSSDS (SQL Server Data Service)など

  PaaS（Platform as a Service）

  アプリケーションをホスティングするプラットフォーム機能を提供、例：

Salesforce.comのForce.comプラットフォーム、Microsoft Azure、GoogleのGoogle App Engineなど

  SaaS（Software as a Service）   アプリケーションの機能を提供、例：Salesforce.comのCRM/SFA他 多数 Ichiro Satoh   Googleの場合   36ヵ所のデータセンター、   各センターには、40サーバ台構成のラックが150以上設置   1クラスタは1800台構成   クラス単体では、一年目で1000件の故障   Googleの障害対策ポリシー   「信頼性の高いハードウェアを1台持つよりも、信頼性はさほ ど高くないハードウェアを2台持った方がいいというのが、Googleの考えだ。その場合、信頼性をソフトウェアレベルで提供する必要がある。1万台のマシンを稼働してい れば、毎日、何かが故障するだろう」   高信頼性ハードウェアよりも高信頼性ソフトウェアに投資 Ichiro Satoh   クラウドコンピューティングはハードウェア障害を前提にしたアーキテクチャ   Googleの場合、1800台単位のクラスタで一年目で1000台で障害 が発生   常にどこが壊れていることを想定   データの高速アクセスのためにデータをオンメモリで管理することも多いが、多重化により一部のコンピュータが停止しても処理が続けられる。   それでも大規模な障害が起きる Ichiro Satoh   Amazon EC2

  Google App Engine   Microsoft Windows Azure

(4)

Ichiro Satoh   Resizable compute capacity in the cloud.

  Obtain and boot new server instances in minutes   Quickly scale capacity, up or down, as your computing

requirements change

  Full root access to a blank Linux machine   Simple Web service management interface   Changes the economics of computing:

  Pay only for capacity that you actually use   a + bc becomes just bc

Ichiro Satoh

Small

Large

Extra Large

Bits

32

64

64 RAM

1.7 GB

7.5 GB

15 GB

Disk

160 GB

850 GB

1690 GB

EC2

Compute

Units

1

4

8 I/O

Performance

Medium

High

Firewall

Yes

Ichiro Satoh

 

Public AMIs: Use pre-configured, template AMIs

to get up and running immediately. Choose from

Fedora, Movable Type, Unbuntu configurations,

and more

 

Private AMIs: Create an Amazon Machine Image

(AMI) containing your applications, libraries, data

and associated configuration settings

 

Paid AMIs: Set a price for your AMI and let others

purchase and use it (Single payment and/or per

hour)

Ichiro Satoh   すでに勝負になっていない   日本にはデータセンターに1000億円を超える投資ができる企業は ない   そのような大規模DCを建設するための人材、技術を持っている企 業は少ない（というかまったくない）   大型のデータセンターの運用ノウハウを持っている企業はない   ネット地政学的にデータセンター向きではない   高価な土地代、高価なエコロジーじゃない電力、高い労働単価、高い気温、地震、水冷用の水の確保が難しい、無駄に厳しい法律日本はユーティリティ・コンピューティングを使うだけの人になりそう

(5)

Ichiro Satoh クラウドコンピューティングの時代では、   システム構築・運用はクラウドコンピューティングインフラに任せ   SI事業者はシステム構築・運用では稼げなくなる   システム構築ではクラウド上の既存サービスを使って新規開発は最小化   ソフトウェア・サービス開発案件が減る   ソフトウェアは買うものから、使うものに変化   サービスのカスタマイズおよびマッシュアップの簡単化   同一インフラ内のサービス連携は容易   ユーザによるシステム開発（内製化）が増える SI業者は一戸建ての住宅建設業者から、マンションの室内装業者に変わることが求められる Ichiro Satoh   ソフトウェアシステムは買うものではなく使うものへの変化(サービス化)   ネットワーク上のサービスを利用   自前のサーバでは実行しない   使った分だけ払う(pay-per-use)ビジネスモデル   サービス提供に特化した企業   例：Salseforce.com   ソフトウェア開発は二分化   個々のサービスの開発   便利なサービスをクラウドコンピューティング上で提供・改良   カスタマイズ   サービスの組み合わせ（マッシュアップ）   ユーザーサイドのシステム開発（内製化） Ichiro Satoh   クラウドコンピューティングのソフトウェア開発は、通常のコンピューティングシステムは相違   インフラ依存のアーキテクチャ定義   SOAに基づくサービス単位化の機能分割   参照・更新に基づくデータ分割   いままでのように上流と下流を分離できない(上流設計時に下流を考 慮)   → 上流設計に特化したSI業者・技術者には手におえない   可用性・スケールアウトを考慮したアプリケーション構築には、対象インフラの内部構造に加えて、大規模分散システムに関する知識が不可欠   非同期処理、分散ハッシュ、キューベーストランザクションなど Ichiro Satoh   クラウドコンピューティングが普及するかはこの際関係ない・・・   クラウドコンピューティングは経営者に「刺さる」話題   顧客はクラウドコンピューティングの価格を基準にする   システム構築費の値下げ要求   アウトソーシング料の値下げ要求   顧客がシステム開発者になりかねない   サービスのカスタマイズとマッシュアップで業務システムを簡易構築   システム運用はクラウドコンピューティングインフラに任せればいい   ただし、クラウドコンピューティングに対する最大の抵抗勢力は、SI事 業者よりも社内IT部門かもしれません・・・

(6)

Ichiro Satoh 国立情報学研究所

佐藤一郎

E-mail: [email protected] Ichiro Satoh   動作箇所が複数   非決定性   デッドロックまたはライブロックの可能性   故障（通信、プロセッサ）理論的な手法で記述・解析する必要がある。プロセス A プロセス C プロセス B プロセスA プロセスB プロセスC Ichiro Satoh   送信側と受信側は独立に動作   通信プロトコルの接続可能性共有メモリプロセス A プロセス B プロセス A プロセス B 通信メディア読み書き読み書き Ichiro Satoh 手続き型プログラムは状態遷移図によるモデル化が容易状態機械（オートマトン）は逐次動作状態1 状態4 状態2 状態3 初期状態状態1 状態4 状態2 状態3 初期状態状態1 状態4 状態2 状態3 初期状態

(7)

Ichiro Satoh 手続き型プログラムは状態遷移図によるモデル化が容易状態機械（オートマトン）は逐次動作 Q2 Q3 Q1 Q0

a

b

c

b

d

Q

₀

=aQ

₁

Q

₁

=bQ

₂

+dQ

₃

Q

₂

=cQ

₁

+bQ

₃

Q

₀

=aQ

₁

Q

₁

=b(cQ

₁

+dQ

₃

)

Ichiro Satoh 入力に応じて状態遷移する機械   初期状態（高々一つ）   状態遷移   最終状態（0個以上） Q2 Q3 Q1 Q0

a

Ichiro Satoh

Q

₀

=abcQ

₂

abc

Q1 Q2 Q0

a

b

Q1 Q2 Q0

a

b

Q2

ｃ

Q1 Q2 Q0

a

b

Q2

ｃ

Q1

a

Q

₀

=abQ

₂

+acQ

₂

abまたはac

Q

₀

=abQ

₂

+acQ

₂

abまたはac

Ichiro Satoh 同じ入力でも違う動作 Q1 Q2 Q0 100円 100円コーヒージュース Q1 Q2 Q0 100円 100円コーヒージュース Q3 100円

(8)

Ichiro Satoh Process Calculus   Process Algebraと呼ぶこともある   通信を状態遷移アクションとするオートマトン   コンピュータ、エージェント、ロボット、細胞をプロセス呼ぶ能動的な動作実態として抽象化   プロセスは他のプロセスと通信（相互作用）   手続き型言語に近い記述性   代数的な記述式の関係 Ichiro Satoh  

ホワイトボックステスト

 

システムの内部構造（単体の場合には、プログラムが

実行されるパス）を意識してテストを行う。プログラム

によるテスト（Program-based Testing）

 

ブラックボックステスト

 

システムの内部構造を意識せずにテストを行う。仕様

によるテスト（Specification-based Testing）

Ichiro Satoh   プロセス式＝オートマトン＋通信手順＋プロセス合成 input

a

output

b

input

b

output

c

System =

_def

(a.b.P’|b.c.Q’)

input

a

output

b

_input

_b

output

c

P Q P’ Q’ Q1 Q2 Q３ Q1 Q2 Q３ Ichiro Satoh ＣＣＳの構文

P :

|

_a.P

|

_{a P}

|

_P

|

P Q

|

P|Q

P L

A

=

+

0 .

.

|

τ

\

停止プロセス同期入力（通信入力aを受信後、Pとなる）同期出力（通信出力aを送信後、Pとなる）内部計算（内部計算を実行後、Pとなる）選択動作（PまたはQとなる） 並行動作（PとQが並行に動作できる） 事象制限（Lに含まれる事象名の外部観測禁止） プロセス定義（A=Pとなるとき、AをPで置換）

(9)

Ichiro Satoh   表示規則を帰納的に定義   プログラミング言語や計算モデルのほとんどは文脈自由文法を用いる例： A ::= c A d | e B f B ::= g Ichiro Satoh

Structural Operational Semantics (SOS)：構文要素に応じて変換

規則を定める   プログラミング言語や計算モデルは表示規則を決める文法と、表示規則の意味を定める意味論に分かれる   計算モデルやプログラミング言語の意味論：   操作的意味論 計算動作を数学的に定式化   代数的意味論 表現(プログラム)を代数構造に写像   公理的意味論 論理式で計算前と計算後の状態を表現

P → P’

P op Q → P’ op Q

P ::= P op P

Ichiro Satoh 例：

if Condition then Statement-1 else Statement-2 endif → Statement-1

Statement ::= Statement ; Statement

| if Condition then Statement else Statement endif

| while Condition do Statement od

Condition ::= true | false

Condition = true

if Condition then Statement-1 else Statement-2 endif → Statement-2

Condition = false

while Condition do Statement od → Statement ; while Condition do Statement od

Statement-1 ; Statement-2 → Statement-1’ ; Statement-2 Statement-1 → Statement-1’

Condition = true

while Condition do Statement od → ε

Condition = false

Ichiro Satoh 並行・通信などの処理を含む動作を記述する形式系

代数的規則による定義

a+b = b+a a+(b+c) = (a+b)+c (a+b)c = ac+ab a+a = a (ab)c = a(bc)

状態遷移規則による定義プロセス計算体系の例： CCS、ACP、CSP プロセス計算をプロセス代数と呼ぶことも多い

P

a

→



.

_P

P

_Q

a

P

'

_P

_'

a

→



+

→



Q

P

Q

P

a a

|'

|

'

→



→



(10)

Ichiro Satoh

Labeled Transition System (LTS)

  オートマトンと同様に   アクションは通信（出力、入力、内部計算）   として，そのコンプリメント(相補) Ichiro Satoh   通信を状態遷移アクションとするオートマトン   同期通信を中心に表現   手続き型言語に近い記述性   代数的な記述式の関係

P

input

a

output

b

Q

input

b

output

c

P

input

a

output

b

Q

input

b

output

c

P =

_def

a.b.P’

Q =

_def

b.c.Q’

System =

_def

(a.b.P’|b.c.Q’)

Ichiro Satoh   プロセス式＝オートマトン＋通信手順＋プロセス合成

P

input

a

output

b

Q

input

b

output

c

System =

_def

(a.b.P’|b.c.Q’)

input

a

output

b

_input

_b

output

c

P Q P’ Q’ Ichiro Satoh 基本式の操作意味論

P

a

.



→

a

'

P

Q

P

→



+

→



α

Q

P

.P

:

P

+

=

|

0 α

'

Q

P

Q

→



+

→



α

P ' Q'

a

b

P

+

Q

(11)

Ichiro Satoh ラベル付き遷移システム（構造的操作意味論）

'

Q

P

Q

→



+

→



α α

P

P Q

P

α α

 →



+

 →



'

α

_{. P}

_{ →}

_

α

_P

a P.

_{ →}

_

a P P a P  → ' P ' Q'

a

b

P

+

Q

a ＝ b のときは非決定的選択 Q a Q  → ' となる遷移が可能なときとなる遷移が可能なとき

P

P L

L

α α

α

 →



 →



∉

∪

'

(

))

\

Ichiro Satoh 同じ入力でも違う動作 Q1 Q2 Q0 100円 100円コーヒージュース Q1 Q2 Q0 100円 100円コーヒージュース Q3 100円

Q=money.(juice.Q+money.coffee.Q)

Q=money.money.coffee.Q+money.juice.Q

Ichiro Satoh 同じ入力でも違う動作 Q1 Q2 Q0 100円 100円コーヒージュース Q1 Q2 Q0 100円 100円コーヒージュース Q3 100円 P1 P0 100円ジュース R1 R2 R0 100円 100円コーヒー Ichiro Satoh ラベル付き遷移システム（構造的操作意味論）

P

Q

P Q

a a

 →



 →



 →



'

|

τ

'| '

P

P Q

α α

 →



 →



'

|

'|

P

|

Q P’

|

Q’

τ

a

P

|

Q P’

|

Q’ P

|

Q P’

|

Q

a

P

|

Q P’

|

Q

a

'

|

'

Q

P

Q

P

Q

→



→



α α 一対一の同期通信非同期に遷移

(12)

Ichiro Satoh 動作式の例

a P

.

+

b Q a R

. | .

 →



τ

P R

|

a P

b Q a R

b

Q a R

.

+

. | .

 →



| .

a P_. b Q a R_{. | .} a a P_. b P R_{. |} +  → +

a P

_.

b Q a R

_{. | .}

a

P a R

_{| .}

+

 →



( .

a P

+

b Q a R

. | . ) { , }

\

a b

 →



τ

( | ) { , }

P R

\

a b

Ichiro Satoh 構文要素に応じて意味を定式化意味論   操作的意味論 計算動作を数学的に定式化   代数的意味論 表現(プログラム)を代数構造に写像   公理的意味論 論理式で計算前と計算後の状態を表現 Ichiro Satoh 表現(記号)と表現の意味を分けて考える 例：プログラムとは   ある文法で書かれた字面   その字面はコンピュータにより実行される   プログラミング言語は、字面の文法と、字面の実行方法を定義 Ichiro Satoh   プログラム   ペトリネット   プロセス計算（プロセス代数）   時相論理

(13)

Ichiro Satoh

R

通信名（ポート名）は静的に決定されている

→ 知らない通信名を介して通信ができない

知っている通信名{ a } 知っている通信名{b, c } CCSでは ポインタ、オブジェクト識別子、動的にリンクが変化する通信ネットワークを含むシステムが記述できない

P

b

知っている通信名{ a，c } と増えることはない知っている通信名{ a，b }

a

Q

a b

b

c

_R

知っている通信名{b, c }

P

b

知っている通信名{ a，b }

a

Q

a b

b

c

Ichiro Satoh •  通信プロトコル •  並列・分散システム •  社会システム •  ビジネスプロセス •  細胞間相互作用（例：ウィルス感染） •  分子生物学 Ichiro Satoh   感染型経路制御   蓄積運搬転送(Store-Carry-Forward) に よる経路制御   ノードが送信もしくは中継したいパケットを保持している場合   通信範囲内に他の端末がいる場合 ⇒パケットを複製して渡す（感染）   通信範囲内に他の端末がいない場合⇒保持したまま移動 Ichiro Satoh   通信プロトコル   送信側(S)、受信側(R)、通信チャネル(C)