AlloyでDining Philosophers 〜その２: デッドロックを検出しよう〜

形式手法 モデル検証

さて、この前の日記で、哲学者たちとフォークを一つのテーブルに着かせる事ができました。
では、今度はナイーブなアルゴリズムでデッドロックが起きる事を検証してみましょう。

今回のアルゴリズム

  • 哲学者は同時に１本のフォークをとる。
  • ２本獲得して満足したら２本同時に手放す。
  • 哲学者はとってもグリーディなので、１本握ったら、食べるまでそれを離さない。

Alloyで記述してみる。

まずは、システムのグローバルな状態を定義して、その状態間の関係を定義することで、アルゴリズムの実行を記述します。
今回は簡単の為にフォーク自体の排他制御は仮定した上で、「フォークが誰に持たれているか」を追う事にしましょう。

-- Global State
sig State {
        -- フォークの保持者は高々一人(lone:least or equal to one)
	owned: Fork -> lone Philosopher
}{
	-- フォークは自分の両脇の哲学者からしか保持されない
	-- f.ownedでも良いが、ボックス結合を使って読みやすく(a.bをb[a]って書ける)
	all f:Fork | owned[f] in f.(left+right)
}

あとは、この状態間の関係を定義してやればいい訳ですね。
とその前に、ちょっと記述を読みやすくするために述語を導入しておきます。

-- フォークの為の述語
-- ある状態sでフォークfはフリーである（誰にも保持されていない）
pred free ( s: State, f: Fork ) {
	no s.owned [ f ]
}

-- 哲学者の為の述語
-- ある状態sで哲学者pは食べている（両隣のフォークの保持者がpである）
pred eating ( s: State, p: Philosopher ) {
	p  = s.owned[p.rightFork] and p =  s.owned[p.leftFork]
}

さて、準備は整いました。「状態間の関係」を定義してみます。具体的に言うと、

ある状態sである哲学者が左のフォークを取ると状態s'になる

みたいな事です。
これをAlloyで書いてみます。今回は状態間の遷移で、誰か一人しか動かないと仮定します。

-- 状態sで哲学者pが左のフォークを取った状態がs'である
pred TakeLeft ( s: State, s': State, p: Philosopher ) {
	-- sではpの左のフォークは空いていて、s'ではpの左のフォークはpが保持している
	-- (述語に引数を適用する場合には[]を使う)
	free[s,p.leftFork] and s'.owned[p.leftFork] = p
	-- それ以外のフォークは保持者が変化していない
	and (all f: (Fork - p.leftFork) | s.owned[f] = s'.owned[f])
}

こんな風に右のフォークを取る場合、食べてる時に両方のフォークを離すを記述してみると、校鳴ります。

-- 状態sで哲学者pが右のフォークを取った状態がs'である
pred TakeRight ( s: State, s': State, p: Philosopher ) {
	free[s,p.rightFork] and s'.owned[p.rightFork] = p
	and (all f: (Fork - p.rightFork) | s.owned[f] = s'.owned[f])
}
-- 状態sで哲学者pが食べていて、両方のフォークを手放した状態がs'である。
pred Release(s:State, s':State, p:Philosopher){
	eating[s,p] and (free[s',p.rightFork] and free[s',p.leftFork])	
	and (all f: (Fork - (p.leftFork + p.rightFork)) | s.owned[f] = s'.owned[f])
}

さて、後は、「初期状態」と「次の状態」を定義してやれば、状態が時系列に並びますね。その並んだ状態列の中で、デッドロック、つまり、全員がどのアクションも取る事ができない状態があるかどうかを調べます。
Alloyでは任意のシグネチャ(sigで定義したやつ)に全順序を導入してくれるモジュールが用意されていますので、それを使います。

open util/ordering[State]

って書いておくと、Stateに全順序を導入してくれて, first,next[s],lastなんていうので状態にアクセスできます。
これを用いて、アルゴリズムの実行を、State間の順序の制約として記述します。

-- 初期状態の述語
pred init ( s: State ) {
	all f: Fork | free [ s, f ]
}
-- 状態上の全順序に与える制約
fact Traces {
	-- firstはinitを満たす
	init [ first ] 
	-- 最後の状態以外の状態sは
	-- 誰かが動作できる状態ならsの次の状態next[s]は誰かが動いた後の状態であり、
	-- かつ、そう出なければ、何も変わっていない(デッドロックが続いている)
	all s: State - last
		| SomeoneCanMove[s] => SomeoneActioned[s,next[s]] else s.owned = next[s].owned
} 
-- 状態sで、誰かが動いた状態がs'である。
pred SomeoneActioned ( s: State, s': State ) {
	some p: Philosopher | TakeLeft [ s, s', p ] or TakeRight [ s, s', p ] or Release[s,s',p] 
}
-- 状態sで誰かが動作できる。
pred SomeoneCanMove(s:State){
	some p: Philosopher | 
		free[s,p.leftFork] or free[s,p.rightFork] or eating[s,p]
}

さて、これで記述が終わりました。Alloyにデッドロックに陥るまでの実行を検出してもらいましょう。

-- デッドロックが存在する実行である
pred WithDeadLock{
	-- ある状態sは、初めてのデッドロック状態で、その後ずっとデッドロック。
	some s:State | not SomeoneCanMove[s] 
				and all s': s.^next | not SomeoneCanMove[s'] -- s以降のs'はずっとデッドロック
				and all s'': s.^prev | SomeoneCanMove[s''] -- s以前はずっと誰かが動ける
}
-- デッドロックが存在する実行を見つけてくれ、というコマンド。
-- 3フォーク、3人の哲学者、実行の長さは10ステップ
run WithDeadLock for exactly 3 Fork, 3 Philosopher,  10 State

これを実行するとこんな感じの状態が出てきます。（Stateプロジェクションを利用したり不要な関係は表示しないようにしてあります。)

確かにデッドロックが検出できていますね。３人が同じ方のフォークを握ってしまった瞬間誰もはなせなくなる、というのが発見できました。

タイムアウトをつけたりすると、デッドロックは起きなくなりますが、今度はスタベーションが起きたりしてきます。
いろんな制約をつけて実行を探させても面白いですね。

今回使ったスクリプトをココに置いておきます。

AlloyでDining Philosophers 〜その１: とりあえず全員テーブルに着席させよう〜

形式手法 モデル検証

最近形式手法について勉強したくて、この本を買ってAlloyって言語について勉強してみたので書いてみる。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−

Alloyって？

いわゆる形式手法と呼ばれる「仕様がちゃんとしているチェックしようぜ」って手法の一つである、「軽量形式手法」という手法をサポートするツールです。
仕様をモデル記述言語で書いて、その仕様が「へんてこな事になってないか？」ってのを、状態を網羅的にチェックして検査してくれるというモノです。
で、Alloyってのは

軽量形式手法のツールで、タダで、グラフィカルに例示ができて、言語自体も、論理と集合の言葉と、みんなが大好きSQLが基にしている「関係」がわかってれば、覚える事は「記法」くらい。と、とりあえずモデリングさえできれば、取っ付ける、とっても取っ付きやすい形式手法のツールです。

中身としてはモデルと制約を全部論理式に展開してSATソルバにかけるっていう風にやってるみたいです。
[参考]Alloyの紹介記事：

さて、Dining PhilosophersをAlloyで解いてみよう！

システムの陥ってほしくない状態の代名詞でもあるデッドロック。これを検出させるのを目標にしてAlloyでモデルとアルゴリズムの仕様を記述してみましょう。蛇足ですが、僕が大学でこの概念に出会った時はたしか「死の抱擁」って訳されてた覚えたがありますw

問題の説明は割愛します。定義はwikipedia参照。
wikipedia - 食事する哲学者の問題

さて、小難しい説明は抜きにして書いてみましょう。まずは哲学者とフォークを定義してみましょう。

-- 哲学者
sig Philosopher {
	-- 左と右には異なるフォークが1本ずつある
	disj leftFork, rightFork: one Fork,
	-- 左と右には哲学者が１人ずついる
	left, right: one Philosopher
}
-- フォーク
sig Fork { 
	-- フォークの左と右には異なる哲学者が一人ずついる
	disj left, right: one Philosopher
}

さて、これだとフォークと哲学者の間に何の制約も無いので、leftとかrightってフィールドに何でも代入できちゃいますから、哲学者とフォークが互い違いに並んでいるように制約を書きましょう。制約はfactってキーワードで記述します。

fact{
	-- フォークと哲学者の数は同じ
	#Philosopher = #Fork
	-- すべての哲学者に対して、右(左)の哲学者は、右(左)のフォークの右(左)の哲学者と等しい
	(all p: Philosopher | p.left = p.leftFork.left and p.right = p.rightFork.right )
	-- すべてのフォークに対して、左(右)の哲学者の右(左)のフォークは自分
	(all f: Fork | f = f.left.rightFork and f = f.right.leftFork)
}

これで隣どうしの哲学者の間に共通のフォークが存在している制約がかけました。なんか足りない気もしますが、進みましょう。まずは、この制約の上でどんな例が存在するのかAlloyに探させてみましょう。そうすれば色々わかるはずです。そんな時によく使うイディオムがこれ。

-- 常に真であるという述語
pred show{}
-- showという述語が成立する例を探せ
run show for 4 Philosopher, 4 Fork

run は述語を第１引数にとって、その述語が成立する例を探してくれるコマンドです。for 〜〜で続けると、探索範囲を指定できます。この例だと、フォークも哲学者も最大４個(人)で、っていう指定です。showって述語はいつも真になるような述語を定義しておくことでとりあえず制約を満たすモデルを例示できるというわけ。
Alloy Analyzerでこれを打ち込むと、いろんなパターンが出てきます、サイズ２、３、４でちゃんとテーブルに並んで座ってる図もでてきますが、こんな図も出てきてしまいます。

これだと、一つのテーブルにつけてません。足りなかった制約はこれのようです。そうですね。フォークと哲学者が交互に並んでるというだけでは、テーブルは複数でもOKだということですね。ということで次の制約を付け加えてテーブルを一つにしてみます。

-- テーブルは一つ
fact OneTable{
	-- すべての哲学者に対して、どの哲学者も左、左(右、右)とたどる事で到達できる
	-- left(right)の推移的閉包は哲学者全体を含む
	(all p: Philosopher | Philosopher in p.^right and Philosopher in p.^left)
	-- すべてのフォークに対して、どのフォークも左、左(右、右)とたどる事で到達できる
	-- left.leftFork(right.rightFork)の推移的閉包はフォーク全体を含む
	(all f: Fork | Fork in f.^( left.leftFork ) and Fork in f.^( right.rightFork ))
}

さて、これでどうでしょうか。同じようにrunしてみると、さっき出てきた２テーブルの例は出てこなくなるのがわかると思います。
うん。よしよし。これで、哲学者とフォークを１つのテーブルに並べる事ができました。
次は、単純なアルゴリズムを記述してみて、デッドロックが発生してしまうことを検出してみます。

モナドを勉強してみたので、オブジェクトっぽいのを作ってみた。

言語 Haskell

社内勉強会でHaskellを細々とやっているんだけれど、やっとこさウワサのモナドの章が終了。使用している本はふつうのHaskellプログラミングです。

そこで、「モナドを使うと参照透明性を保って擬似的に状態をプログラミングできるっぽい」というモナドの気持がわかったような気がしたので書いてみる。これまであやふやなまま圏論を勉強したり、いろんなブログをよんだりしてきたけれど、それがほとんど繋った気がします。で勉強会でちょろっと作ったものが、本質をうつしだしてるわけじゃないけど、最初のとっつき段階ではいいんじゃないかなという例だったので書いてみます。

とりあえず、オブジェクト指向畑で育ってきた僕にとっては、「オブジェクト」は状態を保持している代名詞です。それをsetterをつかって状態をゴニョゴニョかえる感じ。なのでそれをモナドをつかって書いてみました。

まず、サンプル。Personクラス的なものをば。

続きを読む

Just do it. 〜答えはそこにある。いやそこにしかない〜

Life

デブサミ2008感想です。すみません、特定の講演の感想ではないです・・・・

僕は今回は今僕が最も興味があることの一つである「アジャイル」に関する公演をメインに聞いた。仕事で関さんの講演が聴けなかったのが残念だが、朝一の平なべさんのと、片山さんのと、最後のパネルディスカッションはちゃんと聞くことができた。

今回のアジャイルのセッションでは「リーダーシップ」についての議論があったのが印象的だった。僕は以前からソフトウェア開発という風に範囲を限定しない立場でのリーダーシップというのに非常に興味がある。そしていくつか持論も持っている。

僕の中では「リーダーシップ」と「マネジメント」を発揮するのは別だと考える。（結構人間系というか、自己啓発や成功するためには系ではこの分離はめずらしくない）。

よく聞く例えだが、森を切り開いて道路を作る時に

  • リーダー：木に登ってどっちの方向に進むべきかを木を切る人に伝える
  • マネージャー：効率よくリーダーの示した方向へ木を切り倒していくかを実践する

こんな具合だ。そして僕の持論として「良いリーダー」のための4要素。

  1. グループの状態の把握
  2. グループの要求の把握
  3. グループへの明確な方向性の提示
  4. グループとの信頼感

この4つを自分の中では納得して持っている。
そして平鍋さんが言っていたリーダーの4象限のうちの「技術に関する知識」というのは、要求を汲み取って矛盾のない方向性を出すためにあった方が良い能力なんだと僕は考える。片山氏の言っていた折衝力というのは僕の中ではリーダーの方向性の提示と信頼感の構築にかかわってくる話だ。片山氏はカリスマをあまり良く評価していなかったが、明確な方向性を提示して人を引き付けたいようなときには一種のカリスマがあった方が良い時もある。
（マネージャーはそれとは別に、グループの人達をよりやる気にさせる環境づくりに励む役割だと思う。僕の中で良いマネージャーの資質というのは固まっていない。）

と、こんな話をパネルディスカションの後、片山氏にぶつけてみた。彼は静かにうなずきながら聞いてくれた。そして



「うんうん。それでもいいんじゃないかなとおもいますよ。」



最初は、謙虚に答えてくださったんだと感じつつ、家路についていたわけだが、ふと気づいたのだ。
彼は「それでも」と答えてくれたのだ。

この「それでも」という言葉に、僕は打ち抜かれた。

僕は同意してほしかったのだ。僕の意見は正しい、私も賛成だと。
僕はこれまでいろいろ思いを巡らせては、こうしてどこかに書き記したり、人に話したりしてきた。

正しい答えなど無いとは分かっていながら、僕は自分の答えに自信を持ちたかったのかもしれない。
そして片山氏に思いをぶつけたときも同じ思いだったのだろう。
しかし片山氏は「それでもいいんじゃない」と答えてくれた。
そう、こういう問題というのは、答えというのはないんだ。いろいろな人たちがいわゆる成功者たちから何かを学び取ろうとする。
そして、いろいろ分析し共通点を見出し普遍的な要素だと予想してそれを答えだと思い始める。

しかし、今回の「それでもいいんじゃない」という答えをいただいて、目が覚めた気がする。

そんな答えはいくら分析して帰納して抽出したところで、それが正しいかどうかなんてわからない。
その答えは自分でやってみるしかないんだ。 Just Do It!

正しい答えなどない。
自分で正しいと信じる道をガムシャラに進んだそのずっと先に、その考えが正しかったかどうかがあるだけだ。

そんなことを教えていただいた気がする。


だから、進もう！自分の信じたことを、ただやればいいんだ！

その先に答えはまっているんだから。

Melted Brainの作り方

ソフトウェア開発

デブサミ2008の平鍋さんの講演でメアリーポペンディックさんの本からの引用で「Melted Brain」という話があった。

「ビジネス的な事」と「技術的な事」。これらは基本的にとても性質の違うもので、専門家も別々の場合が多い。しかしながら、ソフトウェア開発に本当に必要なのは、これらの通常別々の脳で考えられる二つの事柄を「ひとつの脳」でできる人物ではないか、という話だ。2つの脳がひとつの脳の中で溶け合うという表現だろう。

この話を聞いた時、以前から僕の頭の中にあった考えと非常に強い関連性があるのがわかった。

ソフトウェア業界では営業と技術（開発）との距離が遠いのは知っていた。そこで僕が考えていたのは

「いかに営業といえども、やっぱり開発を十分経験した人がするのが ベストだろう。
　そして開発も時には営業をすべきだ。 」

ということだ。

しかしながら、営業には営業に適した特性、開発には開発に適した特性があり それはまったく異なることも事実だ。なので専任者はそれぞれ置くべきだが、 営業と開発の中間に、営業と開発を適当な周期でローテーションするような役の人がいたりすると理想的だと思っていたのだ。

この人たちは通常の技術営業のように「単に技術を知っている営業」というのではない。
営業の時は実際に営業をし、開発の時は実際に開発を行う。実際に体を使って営業と開発を実践するのだ。
なぜならば、やはり知識だけでは足りない。 どちらも実践して初めて見えることの方が大切な部分が多いと僕は思うからだ。

彼らを適当な周期でローテーションさせることで、 営業の空気（マインドや仕事に対する考え方など）と開発の空気を混ぜることが一番の目的です。
彼らが実際に業務を通して双方の空気を伝え合うのです。 営業という歯車と開発という歯車の潤滑油のようになる感じです。

いや潤滑油なんてあまっちょろいものではない。なんていうのかな・・・媒体とも呼ぶべきか。

営業のエネルギーを開発にフィットするエネルギーに、
開発のエネルギーを営業にフィットするエネルギーに、
それぞれトランスフォームして双方に注入する役割だ！

と考えていたのだが、僕が考えていた話はMelted Brainの作り方とも言えるのではないだろうかとふと思った。
僕が考えていることが実際にいろんなところで考えられている。僕の考えとそれらがつながっていく。こんなに楽しいことはないな。

マインドはプロセスを生み、プロセスはマインドを育てる。〜マナーとルールに見る関連性〜

プロジェクト ソフトウェア開発

最近、アジャイルマインドという言葉をよく目にする。
そしてマインドと対極的な位置にあるのがプロセスやプロトコルという言葉じゃないだろうか。

最近マナーとルールについての興味深い記事があった。これはマインドとプロセス（プロトコル）にそのまま当てはまるように思う。
プロトコルが無くなった場合のマナーの無力化は多少言いすぎなように個人的には感じるがおおむね賛成だ。

高速道路が渋滞している時に、合流の所でお互いに譲りあって一台づつ交互に進めば全体として一番早く進む。我先にと進路を奪いあえば、流れは滞るし、接触事故なども起きやすく、平均の流量は最低になる。

この譲りあいの暗黙のルールが守られる度合いは地域によって違うと聞いたことがあるが、自然発生的にそれができていれば、自分が譲ってもすぐ次に行けると期待できるので、自然と譲る人が多くなるだろう。

「一台づつ交互に」というのはマナーでもあるがプロトコルでもある。

プロトコルが存在していれば、ドライバーの平均のマナーレベルが低くても、つまり、他人より自分を優先して考える人が多くても車は進む。その逆に、譲る気持ちを持ったドライバーの存在密度が高くても、プロトコルがないとマナーのレベルの低いドライバーの行動様式が全体を支配する。

プロトコルが存在しない所にプロトコルを確立するには、マナーが必要である。だが、すでに確立しているプロトコルとマナーが同時に崩壊していく時代に生まれたとしたら、どちらを優先して守るべきかははっきりしている。

プロトコルを守っていけばマナーが低下しても秩序は保たれる見込みがあるが、プロトコルが崩壊したら、マナーの有無はほとんど無意味になる。プロトコルを守るべきだ。

罵倒から生まれる公共性 - アンカテ(Uncategorizable Blog)

そうなのだ。
現在アジャイルマインドと呼ばれている多くのマインドは確かにすばらしい。そして、それらのマインドを広めることの重要性を認識しない人はいないだろう。

しかし、マインドだけ語られるとき、アジャイルマインドという言葉がニュースに踊る時、常にどこかにもやもやがあった。
「本当にマインド"だけ"でよいのだろうか。」と。

そして、昨年のオブジェクト倶楽部クリスマスイベント後の懇親会（ＰＦＰ冬の宴）で

マインドが「プロセス」を生み出し、「プロセス」がマインドを育てる。

という話をした事も、それに由来する。マナーとルールという関係がきれいにこの構図に当てはまっているのだ。

現実問題、マインドだけでは、マインドを持たない人（すなわちマナーの悪い人々に対応する）の悪影響を排除できないのではないのだろうか。引用例をみてもそれは明らかだ。交通ルールはマナーだけでは絶対に秩序は保てないのだ。

だからこそ、ルール（プロセスやプロトコル）を用いて、マインドを持たない人の悪影響を抑制しつつ彼らにマインドを植え付ける必要があるのだ。これはマインドを広めるためにも十分に有効な方法だと思う。

芽生えさせるというのは少々言い過ぎかもしれないが、マインドを持たない人々に、マインドを芽生えさせ・熟成させるのがプロトコルやプロセスの真の役割だと僕は思う。だから良いプロトコルや良いプロセスはそのような性質を持つべきだ。

最近「マインド」という言葉が踊っている、そのこと自体に異論は全くない。
しかしながら、「マインド」という言葉が踊っているのを目にするたびに僕の中に生まれていたもやもやがこれできれいに晴れた気がする。


そう、「マインド」と「プロセス」は一緒に語られるとき、初めてその真価を発揮するのだと思う。
そう、まるでダンスを踊る男女のように。

The Core Protocols 〜チームワークの最強兵器〜

プロジェクト

2008年のオブジェクトの広場にて、先日日本語訳で貢献することができたJim McCarthyのCoreProtocols V3の紹介記事を寄稿しました。

今回のキーワードは 「チームワーク」。
よく耳にする言葉ですよね。 そして、この「チームワーク」の力を実感している人も多いと思います。 チームワークが効果的に働くとき、１＋１が１０にも１００にもなるとも言われます。

でも、 チームワークの力を実感できる人と同じくらい多く、 いやもしかしたらもっと多くの人が

「チームワークをうまく発揮するのは難しい」

と思われる人もいるんじゃないでしょうか。 特に、会社、ビジネスにおいて、付き合いが浅かったり、個人的なお付き合いが ほとんどない人たちで、ひとつの目標にむかってチームワークを発揮する時などは難しいと思われる方も多いかもしれません。 メンバーと積極的に個人的な付き合いができる方とそうでない方もいること場合もあったりで、ノミニュケーションなどで親睦を・・・ともいかない場合もあるでしょう。


いろんな考え方の人がいて、いろんな人の思いがあって、 時にはうまくいくこともあるけど、時にはぶつかって大爆発・・・ そんなことも起きてしまうでしょう。


人は思ったより感情的な生き物だと、僕は思います。

今回の記事は、そんな、様々な感情の渦をうまくコントロールして、うまくチームワークを発揮する最強ツールのご紹介です（最強ってのは誇大広告かもしれませんがｗ）

「チームワーク」って言葉に興味がある方、
「チームワークをうまく発揮するのはむずかしいんだよねー」という方、
是非、読んでいただきたいと思います。
（記事の最後にアンケートがあるので、様々なご意見お待ちしています！）

The Core Protocols 〜チームワークの最強兵器〜
「メンバーをソフトウェア開発というゲームに没頭させろ！」
Visual C++ の開発チームを率いて成功に導いた Jim McCarthy。 彼によるソフトウェア開発でチームワークを十二分に発揮するための最強コミュニケーションツール「The Core Protocols」をご紹介。 日本語版の訳者である筆者がその魅力を熱く語ります。

オブジェクトの広場:http://www.ogis-ri.co.jp/otc/hiroba/index.html