2005/10/05 志村先生

並行プログラムの正当性
	限られた資源を共有する
	複数プロセスを持つシステム
		ex) ネットワークプリンター

	- あるプロセスが共有資源を利用している時には、
	他のプロセスがその共有資源を利用 *でき* ない
		ex) はさみ
	他のプロセスにはその共有資源を利用 *させ* ない
		ある仕事は、その資源は常に利用しているとは限らない
			# 利用していない時には、他に利用させてもよいか ?
			#	=> 必ずしも良いとはいえない
			仕事の途中で資源を他の者に利用されると困る
				ex) プリンターに複数枚のページを出力する
					ページとページの間に他の印刷物が入ると困る
		=> 排他制御

	# 資源を利用するための規則 (ルール) を决める
	#	規則が成立すれば、上記の問題が解決できる
	#	プログラムがその規則を守っていれば Okey

		##「悪いことがおきない」だけではいけない
		##	どの資源も利用させなければ、悪いこともおきないが..

	- 共有する資源を利用したプロセスはいつかは、資源を利用できる
		# これは「定性的」な性質。本来は「定量的」な問題も考える必要があるが..
		#	ex) 「トイレ」
		# 他にも「公平性」が要求されることもある
		## この講議では、「定量」は扱わないことにする。

==

プロセスとは ?
	(入力や、処理によって..) 「状態が変移するもの」と定式化する
		プロセスの状態 => ○
		状態の変化 => ○間の矢印

		プロセス P

			 +-------+
			 |	 |
			 |	 v

		       [[a]]	[b]

			 ^	 |
			 |	 |
			 +-------+

		プロセス Q

			 +-------+
			 |	 |
			 |	 v
		       [[a]]	[b]
			 ^	 |
			 |	 |
			 +-------+

		[例]
			[[a]] 普通の状態
			[b] プリンターを利用している状態

			# a, b は、状態を区別するラベル
			# 異るプロセスで同じラベルがあっても無関係

		状態を変移させるためには条件が必要
			上の例で、P,Q が共に [b] (プリンターを利用) になると困る
				状態 [b] に入るための条件が必要
					# ないと、共に[b] になり、問題 !!

		P
			[[a]] -> [b] とするための条件
				\not inQ \and turn=P => inP := true
			[b] -> [[a]] とするための条件
				true => inP := false; turn := Q
		Q
			[[a]] -> [b] とするための条件
				\not inP \and turn=Q => inQ := true
			[b] -> [[a]] とするための条件
				true => inQ := false; turn := P

		初期条件
			inP := false;	
			inQ := false;	
			turn := P

			P の状態は [[a]]
			Q の状態は [[a]]

				# [[]] は初期状態を表す。

		# 上の形式は「条件 => Action」の形をしている
		#	条件が成立している時に、Action をしてよい。

			inP, inQ, turn : 共有変数
				資源を「巧く」共有するためには、情報を共有する必要がある。
					個々のプロセスは、(資源を共有しない限り..) 本来は、無関係な仕事を行っている。
						資源共有のためだけに、変数の共有が必要になる。

	# 上の図 ( P,Q のプロセス図 ? 状態図 ) の説明

	- 二つのプロセス P, Q が、一つの資源の共有している
	- それぞれの状態 b でその共有資源を利用している
	- 共有変数
		inP : P が状態 b にあるかどうかを表す ( inP = true の時に、状態 b )
		inQ : Q が状態 b にあるかどうかを表す ( inQ = true の時に、状態 b )
		turn : 共有資源を次に利用できるプロセス

		# の「つもり」

	[解釈]
	# P の状態遷移条件
		\not inQ \and turn=P => inP := true
			Q が b でなく ( 資源が利用可能 )、自分の順番ならば、
				自分が使う

		true => inP := false; turn := Q
			止める時は無条件
				自分は利用終ったので、相手に順番を渡す
	# Q の方も同様

	このようにすれば、巧く行く ( 共に [b] 状態に入ることはない.. ) ことが解る。

	# 以下は、その議論

	まず、共有変数の値が、P,Q の状態と対応していることを確認する
		inP = true となる P が状態 b にあるときだけ
		P が状態 b にあるならば inQ = false
		inQ = false となるのは Q が状態 a にあるときだけ

		# Q に関しても同様なことが成立 => これによって、「排他制御」ができていることが解る。
		## ここまでの議論では、共有変数 turn は使っていない

		一度 b になってから、次に b になるには、他方が b になった時だけ

			# [注意] 次の仮定が入っている。
			#	「[b] の状態は何時かは、終る」
			#		#「クリティカル (共有)時間」は有限で終了
			#	「共に、資源を無限回利用する」

			=> この仕組では、P と Q は交互に利用することが強制される
				ある種の「公平性」を満すが.. (悪平等 ?)

==

	# この状況をどのように (時制論理で..) 表現するか

	G \not (inP\and inQ )	: 相互排除
	inP -> F \not inP	: 資源の占有はいつか終る (システムの仮定の一つ)
	inQ -> F \not inQ

	# G F inP \and G F inQ	: どちらも何回も資源を利用する ( 上の例が成立するためのもう一つのシステムの仮定 )

	## 上の例では、色々と問題がある
	##	余聞な仮定が必要
	##	「交互利用」を強制させられる ( 資源が空いていても利用できな場合がある )
	## このような制限のない解決方法はないだろうか ?


	<<P>>

	   	+-------+
		|	|
		|	|   true => y_1 := ture
		+---> [[a]] -------------------------> [b]
			|				|
	true =>		|				| true => t := false
	   y_1 = false	|				|
			|				|
		       [d] <-------------------------- [c] -----+
							^	|
				\not y_2 \or t =>	|	|
							+-------+
							y_2 \or \not t =>

	<<Q>>

	   	+-------+
		|	|
		|	|   true => y_2 := ture
		+---> [[a]] -------------------------> [b]
			|				|
	true =>		|				| true => t := true
	   y_2 = false	|				|
			|				|
		       [d] <-------------------------- [c] -----+
							^	|
				\not y_1 \or \not t =>	|	|
							+-------+
							y_2 \or t =>

	[説明]
		初期状態
			\not y_1 \and \not y_2 \and \not t

		P, Q 共に状態 d で共有資源を利用している。

		共有変数の意味
			y_1 : P が共有資源を利用したい
			y_2 : Q が共有資源を利用したい
			t :
				y_1, y_2 が共に true の時
					t が true => P が先に状態 c になった
					t が false => Q が先に状態 c になった

	# 「P at a」 を 「プロセス P が 状態 a にある」という命題と考える

	相互排除
		G \not ( P at d \and Q at d )
			P と Q が同時に d にあることはない

	公平性
		G ( y_1 -> F P at d )
			常に 「P が共有資源を希望したら、必ず、いつかは使える」状態にある
		G ( y_2 -> F Q at d )
			常に 「Q が共有資源を希望したら、必ず、いつかは使える」状態にある

	これらの命題が成立する ( つまり、システムが「正当」である ) ことを示す必要がある


	# 各々の状態を論理式で表現する
		G ( P at b -> X ( P at c \and \not t ))
			P が b にいれば、次の瞬間、P は c に行き t は false である
		G ( P at c \and (\not y_2 \or t) -> X ( P at d ) )
			P が c にいて y_2 が成立しないか t が成立すれば、次の瞬間 P は d に行く
		# 変数の値を明示的に書換えない限り、変数の値が変ることはない
		#	=> 「各々の状態で、変数がどのような値になるか」はきちんと証明する必要がある。

	# 方針としては、これらの式から、上記の相互排除等を証明する必要がある
	#	機械的にやるにしても、結構大変
	##		逆に、必要条件から、状態設計を自動的に作る

	### P, Q の状態の直積空間を作り、その間の遷移図を作って、その
        ### 図の性質を利用して、証明する方法もある。