ソフトウェア動的更新の理論的限界

ソフトウェア動的更新の理論に
ついて
産総研
橋本政朋
動機
• ユビキタスコンピューティング時代の本格到来
もそう遠くなさそう
– マイクロサーバが至る所に存在
• ソフトのバグは加算無限個存在
• 機能拡張も必須
• サービスを停めたくない
• 動的更新とは何なのか?
• どのような動的更新が安全なのか?
ユビキタスな世界
It needs:
•的確な状況把握
•位置追跡
•予定表との連携
•プロファイリング
どこに
行け
ば?
•整備された情報インフラ
•環境埋込小型サーバ
•サービス間のシームレスな接続
(Web,プロファイル情報,etc.)
...
Direct!
乗換案内
小型サーバ
位置追跡
位置追跡
検査項目
尿検査
心電図
血液検査
文献
• D.Gupta, P.Jalote, and G.Barua. A Formal Framework
for On-line Software Version Change. IEEE Transaction
on Software Engineering, Vol.22 No.2, pp. 120-131, 1996.
• D.Gupta. On-line Software Version Change. PhD thesis,
Dept. CSE, IIT Kanpur, June 1995.
Plan
• 一般更新モデル
– 更新の妥当性
• 更新妥当性の決定不能性
– シンプルプログラムモデル
– 定理:更新の妥当性の検証は決定不能
• 妥当性が決定可能な動的更新
– 妥当な更新の構成法
• プログラムモデルの拡張
一般更新モデル
• あるプログラムCからC’への更新
• C,C’それぞれは“正しい”と仮定
• 実行状態の変換はプログラマが与える
プロセス
プログラム
入力
C
SC0
C
C
S1
C
Sn
Si
状態
プロセス
•各Cに対しSC0(初期状態)を唯一定める
•SC0からある時点,ある入力列によってとりうる状態は
到達可能
動的更新
プログラム
入力
C
C
S1
SC0
C
Si
状態
更新
プロセス
状態変換
C’
T(Si)
Points
• 即時的変更
– インクリメンタルな変更はその組み合わせで
表現可能
• 状態変換はユーザが定義する
– 妥当性を決するのはタイミング
更新の妥当性
C
C
C
C
S1
SC0
Sn
Si
更新
C’
C’
SC’0
T(Si)
有限ステップで
新プログラムの
到達可能な状
態に達するとき
妥当
更新妥当性の決定不能性
シンプルなプログラムモデルの導入
妥当性の決定不能性
より複雑なプログラムモデルででも決定不能
シンプルプログラムモデル
• 命令型言語の単純版(関数,手続きなし)
– プログラムはステートメントの列
• プログラムCに含まれる変数の集合をV(C)
• プログラムCの状態SCは変数(V(C)⋃{PC})
から適当な値(⊥含む)への写像
• SC0は, SC0(v)=⊥(∀v∈V(C))
SC0(PC)=First(C)
決定不能性
SがCの到達可能な状態であるような任意のC,C’,T,Sに
ついて,SにおけるTを用いたCからC’への動的更新が妥当
であるかどうかは決定不能
C
C
SC0
S
C’
T(S)
C’
SC’0
任意のプログラムC に対し,SC(PC)=Last(C)+1であるような
状態SCが到達可能であるかどうかは決定不能 (停止問題)
妥当性が決定可能な動的更新
状態変換TCC’を制限
– 恒等変換,変数追加,変数名変更,のみ扱う
– +変域(状態)も制限
• 実質,更新タイミング(更新可能状態)の制限
• PCのみ制限 ←実用上の問題
TCC’は(KT,N)という形
CのPC値からC’のPC値への写像
変数名変換
まだ決定不能!
やりたいこと
• 妥当性のための十分条件を求める
計算可能
十分条件
妥当
ステートメント実行毎にチェック
算出したPC値のときのみ更新を起こす
全ては算出不能
十分条件
SにおけるCからC’へのTを用いた更新が妥当
⇑
∃S’’ s.t. C’で到達可能かつS’’(PC)=S’(=T(S))(PC)かつ
∀x∈V(C’),x使用前に再定義される,または
S’(x)= S’’(x)
•V1:更新後使用されるまでに再定義される変数
•V2:更新後そのままでOKな変数
C
C
SC0
S
V1
A1
V2
A2
PC
K
C’
T(S)
C’
SC’0
C’
∃
S’’
V1
A’1
V2
A2
PC
K
更新ポイントの選定
• 更新前プログラムCの各コントロールポイントに
おいてV1とV2を見付ける
– 見付けきるアルゴリズムは存在しない
– データフロー解析活用で近似
• V1⋃V2=V(C’)となるコントロールポイントを選ぶ
例:階乗計算プログラム
入力nを読み,階乗を計算出力するループ
{i,n,p}
{i,n,p}
{i,p}
{i,p}
S1
while true do
read n;
S’1.1
read n;
S1.2
if n < 0 then
S’1.2
if n < 0 then
S1.2.1
write “error”
else
S’1.2.1
write “error”
else begin
S1.2.2
if n = 0 then
S’1.2.2
i ← 1;
S1.2.2.1
write 1
else begin
S’1.2.3
p ← 1;
S’1.2.4
while i ≤ n do
S1.2.2.2
i ← 1;
S’1.2.4.1
S1.2.2.3
p ← 1;
S’1.2.4.2
S1.2.2.4
while i ≤ n do
S1.2.2.4.1
S1.2.2.4.2
S1.2.2.5
{i,n,p}
while true do
S1.1
{i,p}
V1
S’1
p ← p * i;
i←i+1
done
write p
end
done
Version 1 (C)
S’1.2.5
p ← p * i;
i←i+1
done
write p
end
done
Version 2 (C’) V ={n}
2
V1 ⋃ V2={i,n,p}=V(C)=V(C’)
より一般的なプログラムモデル
• 関数,手続の導入
• 更新を関数単位として妥当性を再検討
–
–
–
–
関数間DFAは高くつく
呼び出し中の関数は更新しない
大域変数しか変更しない
関数集合Fのどの関数も呼び出し中でないと
きの更新が妥当であるようなFを求める
更新される関数が全て
functional enhancementなら
それらがFをなす
まとめと課題
• 動的更新の定式化
– 更新妥当性
• 更新妥当性の決定不能性の証明
• 安全な更新の構成
– シンプルケース(関数,手続なし)
– CやPascal 程度ケース
• 更新に対する実用的な制限とは?
• 実時間性は扱っていない