命令型プログラミング言語におけるプログラム可逆変換の形式化
M2012MM016 前林達也
指導教員：横山哲郎

1

はじめに2

関連研究

論理的な可逆性を得る方法には，Landauer による埋プログラムの可逆実行には，効果的な応用が知られている．例えば，投機的実行では，ロールバックの代わりに め込み法が知られている [5]．埋め込み法とは，演算のト可逆実行を用いることでメモリ効率が高まる．特に 1 回 レースを作成するために，追加の情報を記録する方法での計算が少量である場合，逆方向の実行に要する時間は ある．本研究の目的であるプログラム可逆変換も，デー短く，効果的である．また，デバッグでは，バグの検出 タと制御のトレースを記録することで実現可能である．
箇所から原因を特定する作業を効率化できる場合がある． 既存のプログラム可逆変換手法には，Perumalla らによしかし，現実に用いられているプログラムの多くは可逆 る C 言語プログラムの可逆変換手法 [7] がある．Perumalla性を前提としておらず，可逆実行が不可能である．よっ らが作成したコンパイラ RCC は，C 言語プログラムを入て，これらの応用をそのまま導入することはできない． 力すると，可逆変換されたプログラムを生成し，同時に，非可逆なプログラミング言語で書かれたプログラムで 逆変換されたプログラムを生成する．しかし，Perumallaあっても，プログラム可逆変換によって得られたプログ らの手法では，必ずしも正しく可逆変換されることは期ラムを用いれば，可逆実行の導入によって，投機的実行 待されない．なぜならば，RCC は投機的実行の効率化へやデバッグを効率的に行える．そのため，既存研究では， の応用を目的として開発されており，可逆変換の正しさ非可逆な命令型プログラミング言語に対して可逆性を導 を形式的に証明していないからである．本研究では，可入するために，プログラム可逆変換器により可逆実行可 逆変換の正しさに着目し，可逆変換によって生成される能なプログラムを生成する手法が提案されている．一方， プログラムの可逆性を保証する手法を提案する．
プログラムの可逆変換は，投機的実行への応用に有効投機的実行の効率化などを主目的としたプログラム可逆変換手法では，プログラム可逆変換の正しさが形式的に である．例えば，RCC を用いた投機的実行の効率化が行証明されておらず，常に正しいことを期待できない．そ われている [2]．可逆実行が可能であれば，ロールバックの結果，プログラム可逆変換によって得られたプログラ が不要となり，メモリ効率が良い．特に，1 回の計算が少ムは可逆実行できない場合があり，投機的実行やデバッ 量であれば逆方向の実行に要する時間は短く，より効果的である．しかし，RCC により得られたプログラムを用グにおける振る舞いが正しくない可能性がある．
本研究では，命令型プログラミング言語における，プ いた可逆実行が必ずしも正しく振る舞うことは保証されログラム可逆変換の形式化を行う．われわれの知る限り ず，投機的実行は状態を復元することができず計算内容
では，命令型プログラミング言語における可逆変換に関 を損失する可能性がある．
可逆実行は他にも，デバッグへ応用されている [4]．バする研究の中に，プログラム可逆変換を形式化し，その正しさを示した手法は知られていない．形式的な正しさ グの存在箇所と検出箇所は異なる場合があり，このとき，を保証することで，制限された構文のもとでは，現実の 検出されてから実際のバグを特定するまでに，順方向のプログラミング言語において同様に正しくプログラムを 実行を繰り返す必要がある．しかし，プログラムが可逆実可逆実行できることが期待される．その場合，投機的実 行可能ならば，逆方向の実行を用いることで実行回数を行やデバッグといった可逆実行の応用例においても，常 削減することができ，作業を効率化できると考えられる．
プログラムを可逆実行するには，可逆変換による方法に正しい振る舞いをすることが期待される．
本研究の対象とする命令型言語には，一般に利用される だけでなく，可逆実行可能であることを前提とした可逆C 言語を用いる．しかし，C 言語には公式には意味論が プログラミング言語によってプログラムを作成すること存在しないので，プログラムの性質を形式的に示すこと でも実現できる．可逆プログラミング言語には，例えができない．そこでまず，本研究では，Clight[1] とよば ば， Janus[6] や, R[3] などが存在する．命令型言語でれる，形式的な意味論を与えられた C 言語のサブセット ある Janus は，言語の可逆性が形式的に証明されている．
を用いる．構文は，Clight から抜粋した基本的なものを Janus の構文規則および制約を満たすとき，プログラムは対象とし，意味論には構造的操作的意味論を用いる．次 必ず可逆となるよう設計されている．よって，入力に対に，非可逆なプログラムから，可逆プログラムおよびこ し出力が定義される Janus プログラムは可逆である．一れに対応する左逆プログラムの生成器を定義する．最後 方，非可逆なプログラムを認めないため，可逆性を前提に，これらの生成器によって得られたプログラムが可逆 としないアルゴリズムなどをそのまま導入することはで実行可能であることを形式的に示す．可逆実行可能なプ きない場合がある．R も同様に命令型の可逆プログラミ
ログラムとは，逆方向に実行可能なプログラムが存在し， ング言語であり，Janus と類似した機能を持つ．
一般的なプログラム開発やプログラミング学習の現場
順方向の実行の後に逆方向の実行をすることで元の状態に戻るような性質をもつプログラムである．このような では，蓄積された知見を組み合わせて課題を解決するが，それらの知見は可逆性を前提としていない．ゆえに，可性質を示す定理を立て，帰納法を用いて証明する．

逆プログラミング言語ではそれらの知見を直接的に導入することはできない．そこで，非可逆なプログラムを可逆化するという考えに基づくプログラム可逆変換を用いれば，蓄積された知見をそのまま用いることができる．したがって，可逆実行を幅広く応用するには，プログラム可逆変換のアプローチが有効であると言える．

3

prSAVE(x);x = e;

px = e;piRESTORE(x);図 1 代入文の可逆変換
ここで，順方向の実行が常に先行することを前提とし，左逆のみを扱うことから，プログラム可逆変換の形式化

本章では，プログラム可逆変換の正しさを示すために，[[p]]([[p−1 ]]x) = x(4)形式化を行う．形式化した命令型プログラミング言語の構文に基づき，その上でプログラム変換を定義して，形を満たすことを保証しない．ただし，本研究の手法の応式的に正しいことを保証する．
対象とする言語は，広く利用されている C 言語とする． 用例に挙げられている投機的実行やデバッグには，式 4Perumalla らによる先行研究で提案された RCC において を必ずしも満たす必要はない．
C 言語を用いた，プログラム可逆変換の例を図 1 に示も，C 言語で作成されたプログラムに対する可逆変換をす．プログラムは，変換する元のプログラム
p と，p の行っている．しかし，形式的意味論が公式に存在しないrri
C 言語の性質を示すには，形式的意味論を与える必要が 可逆化されたプログラム p ，p の左逆プログラム p である．そこで，形式的意味論を与えられた C 言語のサブ ある．ここで，2 種類のマクロ SAVE と RESTORE は，トセットとして知られる Clight[1] を対象とし，これに基づ レースを記録するスタックに対する操作を行う命令である．メモリが有効である限り，pr は可逆実行可能なプロいてプログラム可逆変換の形式化を行う．
プログラム可逆変換の形式化のために，関連する概念 グラムである．
を形式的に定義することが必要である．プログラム可逆 3.2 構文
変換が形式的に正しいことを，関連する定理に証明を与本研究では，トレースの記録によってプログラム可逆えることで保証する．
変換を行い，正しさを示すことを目的としている．ゆえ
本研究では，Landauer が示した埋め込み法に基づく，に，構文は簡略化したものを用い，単純な方法での可逆すべてのトレースを記録するアプローチでプログラム可変換を実現する．本研究で対象とする，Clight から抜粋
逆変換を行う．よって，計算時間およびメモリ空間の効した抽象構文を以下に示す：率を考慮していない．

3.1

プログラム可逆変換とは可逆性を前提としないプログラミング言語で作成されたプログラムは，通常，可逆ではない．C 言語など多くのプログラミング言語は，可逆性を前提としていない．可逆ではないプログラムを用いて可逆実行をするために，プログラム可逆変換が必要である．プログラムの可逆実行を説明するために，左逆プログラム，可逆化されたプログラムおよび可逆実行可能なプログラムの定義を導入する．
定義 1 (左逆プログラム). プログラム p が与えられたと
き，任意の x, y について，[[p]]x = y ⇒ [[p−1 ]]y = x(2)を満たす pr を p の可逆化されたプログラムとよぶ．
定義 3 (可逆実行可能なプログラム). プログラム p が与えられたとき，p の左逆プログラム p−1 が存在して，任意の x について，[[p]]x が定義されるならば，を満たす p を可逆実行可能なプログラムとよぶ．

宣言式

dcla

二項演算子

⊙(3)

::=||||::=::=||::=

id = as;sif ( a ) s else s
while ( a ) s{ dcl s }(uint id )?
idna⊙a+ | - | ^ | > | ==

代入文
文の並び
条件文
ループ
複合文
変数識別子
整数定数
二項演算

整数定数には，標準符号無し整数型の整数を用いる．表
記を簡単にするため，unsigned int を uint と記す．

3.3

定義 2 (可逆化されたプログラム). プログラム p が与えられたとき，あるプログラム pi が存在して，任意の x, yについて，[[p−1 ]]([[p]]x) = x

s(1)を満たす p−1 を p の左逆プログラムとよぶ．

[[p]]x = y ⇒ [[pr ]]x = (y, h) ∧ [[pi ]](y, h) = x

文

意味論

対象とする構文について，構造的操作的意味論を用いて形式的に意味論を定める．構造的操作的意味論では，プログラムにおける式の評価，文の実行のような各ステップでの遷移を自然に記述できる．本研究では，プログラムの順方向の実行および逆方向の実行による遷移を形式的に記述する必要があるため，構造的操作的意味論を用いることで見通しよく表現できる．まず，意味領域を定める：
ブロックの参照値
局所環境
記憶域b ∈ Zv ∈ Zuint
E ::= id 7→ bM ::= b 7→ v

式の意味規則：R[[x = e]] = SAVE( x ); x = eR[[if ( e ) s1 else s2 ]] = if ( e ) {R[[s1 ]];SAVE(1)} else {R[[s2 ]];SAVE(0)}⟨(E, M ), a1 ⟩ → v1⟨(E, M ), a2 ⟩ → v2
Bin⟨(E, M ), a1 ⊙ a2 ⟩ → [[⊙]](v1 , v2 )文の意味規則：⟨(E, M ), a⟩ → v
Assign⟨(E, M ), id = a⟩ → M [E(id ) 7→ v]⟨(E, M ), a⟩ →
̸ 0⟨(E, M ), s1 ⟩ → M ′⟨(E, M ), if ( a ) s1 else s2 ⟩ → M⟨(E, M ), a⟩ → 0′⟨(E, M ), s2 ⟩ → M ′⟨(E, M ), if ( a ) s1 else s2 ⟩ → M ′I[[x = e]] = RESTORE( x )I[[if ( e ) s1 else s2 ]] = {uint _b;
RESTORE(_b);
if (_b) {I[[s1 ]]} else {I[[s2 ]]}}
where _b ̸∈ Var(s1 , s2 )IfTrueIfFalse

図 2 意味規則の例
次に，意味規則を定める：⟨(E, M ), a⟩ → v⟨(E, M ), s⟩ → M ′図 3 生成器の例(式の右辺値の評価)(文の実行)

例えば，x = x + 1 は可逆文である．一方，Clight の例えば，⟨(E, M ), a⟩ → v という記述は，局所環境 E お
文は必ずしも可逆ではない．例えば，文 x = 1 の実行直よび記憶域 M のもとで，式 a を評価し，その結果として前の M (x) の値は一意に定まらない．したがって，この値 v を得られることを表す．
場合は，式 7 は満たされない．
構文に対して意味を定める意味規則の例を図 2 に示す．
可逆化された文を，次のように定義する．定義に示すとここで，与えられた a, E, M に対して，⟨(E, M ), a⟩ → v ′おり，可逆化された文は，元の文の意味を保持している．となる v ′ が存在して v ̸= v ′ であることを ⟨(E, M ), a⟩ ↛ v
定義 6 (可逆化された文). ある文 s とある可逆文 s′ が与と表す．また，算術演算子+, -は，[[⊙]](v1 , v2 ) = v1 ⊙ v2
えられたとする．任意の E, M, M ′ および任意の b に対mod 232 と定義する．
して3.4 左逆文，可逆文，可逆化された文M ′ (b) ̸= undef =⇒ M ′ (b) = M ′′ (b)(8)プログラムの可逆変換を行うためには，プログラムの実行において記憶域を変更し得る文の実行を可逆化する必要がある．本節では，左逆文，可逆文および可逆化された文の定義を導入する．
定義 4 (左逆文). 文 s が与えられたとする．任意の E, Mについて⟨(E, M ), s⟩ → M ′ =⇒ ⟨(E, M ′ ), s′ ⟩ → M ′′(5)ならば M = M ′′ であるとき，s′ を s の左逆文とよぶ．
例えば，x = x + 1 は x = x - 1 の左逆文である．一方，x = x * 2 には左逆文が存在しない．例えば，x の型が 32 ビットの標準符号無し整数型であるとすると，x =2147483648 の場合，式 x * 2 の評価結果はオーバーフローする．このとき，定義 4 をみたすような左逆文が存在しない．
可逆文を，次のように定義する．任意の可逆文は，実行する直前および直後の状態が一意に定まる．
定義 5 (可逆文). 任意の E, M, M ′ , M ′′ について⟨(E, M ), s⟩ → M ′ ∧ ⟨(E, M ), s⟩ → M ′′ =⇒ M ′ = M ′′(6)⟨(E, M ′ ), s⟩ → M ∧ ⟨(E, M ′′ ), s⟩ → M =⇒ M ′ = M ′′(7)である文 s を可逆文とよぶ．また，式 6 を満たすとき前方決定的であるといい，式 7 を満たすとき後方決定的であるという．

であるようなある M ′′ について⟨(E, M ), s⟩ → M ′ ⇐⇒ ⟨(E, M ), s′ ⟩ → M ′′(9)が成り立つならば，s′ を s の可逆化された文とよぶ．

3.5

可逆化文生成器と左逆可逆化文生成器

本節では，可逆実行に必要な文を生成する 2 つの変換器 R と I を定義する．R[[s]] では s の可逆化された文 srを，I[[s]] では sr の左逆文をそれぞれ生成する，すなわ
ち，R を可逆化文生成器，I を左逆可逆化文生成器になるようにする．生成器の例を，図 3 に示す．
ここで，マクロ SAVE，RESTORE を，意味規則⟨(E, M ), a⟩ → v⟨(E, M ), SAVE( a )⟩ → M [stk 7→ v :: M (stk)]

Savev :: stk′ = M (stk)⟨(E, M ), RESTORE( x )⟩ → M [E(x) 7→ v][stk 7→ stk′ ]Restoreを満たすものとして定義する．stk とは，記憶域 M における特別なブロックの参照であり，マクロ SAVE，RESTOREによってのみ変更される．stk により参照される値を基準に，記録する値を連結することで，スタックの役割をする．
生成器を用いて得られた文が可逆実行可能であることを示すために，満たすべき性質の証明を行う．まず，任意の文について，可逆化文生成器によって得られた文が可逆化された文であることを示す．

定理 7. 任意の文 s について，R[[s]] は s の可逆化された文である．

を用いた．構文と意味論を定め，対象となる文に対する可逆化文生成器および左逆可逆化文生成器を定義し，こ次に，任意の式の評価が前方決定的であることを示す． れにより得られる任意のプログラムが可逆実行可能であ
前方決定的な式は，文に関する定義 5 と同様に，次のよ ることを形式的に証明した．
既存研究では，C 言語プログラムに対するプログラムうに定義する．
′可逆変換器が提案されている．しかし，その手法には形定義 8 (前方決定的な式). 任意の E, M, v, v について式的証明が与えられておらず，結果として誤ったプログ⟨(E, M ), a⟩ → v ∧ ⟨(E, M ), a⟩ → v ′ =⇒ v = v ′ (10) ラム可逆変換が存在することを確認した．これに対して
本研究では，形式的証明のもと，プログラム可逆変換がを満たす式 a は前方決定的な式である．
前方決定的な式は，任意の E, M に対して式の評価の値 常に正しいことを保証した．さらに，既存研究の問題をを一意に定める．すなわち，式 a の評価 ⟨(E, M ), a⟩ → v 解決する可能性がある．
構文は制限されており，実際の C 言語プログラムを可という関係によって，値 v は E, M, a の関数であること逆変換することは難しい．ただし，本研究で示した形式が定められる．
化の手順および証明すべき定理に従えば，機械的に構文補題 9 (式の評価の前方決定性). 任意の式の評価は前方の拡張を行うことができるといえる．また，記録すべき決定的である．
データと制御を削減する効率化も可能であると考えてお
なお，式は必ずしも後方決定的ではない．例えば，a1 =り，この場合も同様に，生成器の定義を変更して定理を2, a2 = 3, ⊙ = + もしくは a1 = 1, a2 = 4, ⊙ = + とする
証明すればよい．と，⟨(E, M ), a1 ⊙ a2 ⟩ → 5 となるので，式の評価により今後の課題は，まず，構文の拡張が挙げられる．本研究
定まる関数は単射ではない．ただし，式の評価は局所環
では構文を制限しており，Clight において手法の健全性境および記憶域を変更しないため，文の可逆性を保証すを予想することはできるが，完全性を主張できない．次るためには式の評価が後方決定的である必要はない．に，適用実験によってプログラム可逆実行の実行効率を
次に，任意の文について可逆化文生成器で得られた文確認し，最後に，手法の効率化を行う必要がある．
が可逆文であることを示す．これを示すために，まず可逆化に用いられるマクロ SAVE の可逆性を示し，これを補 参考文献
題として用いて証明を行う．
[1] Blazy, S. and Leroy, X.: Mechanized semantics for
補題 10 (SAVE の可逆性). 任意の式 a に対して，SAVE( a )the Clight subset of the C language, Journal of Autoは，可逆文である．
mated Reasoning, Vol. 43, No. 3, pp. 263–288 (2009).
定理 11. 任意の文 s について，R[[s]] は可逆文である．た[2] Carothers, C. D., Perumalla, K. S. and Fujimoto,だし，s に関する導出木は有限であるとする．
R. M.: Eﬃcient Optimistic Parallel Simulations Us文 s が “While” 文の場合，導出木の前提に結論と同じ
ing Reverse Computation, ACM Transactions on
大きさの導出木が出現する．このとき，構造帰納法によModeling and Computer Simulation, Vol. 9, No. 3,る証明ができず，導出木が有限であることを前提とした
pp. 126–135 (1999).
数学的帰納法によって証明が与えられる．この前提は，導[3] Frank, M. P.: Reversibility for Eﬃcient Computing,出に関する帰納法を用いた証明により省略できる．
PhD Thesis, Massachusetts Institute of Technology
最後に，任意の文について，左逆可逆化文生成器で得ら(1999).
れた文が，可逆化文生成器で得られた文の左逆文となっていることを示す．これにより，対象とする言語におい [4] Koju, T., Takada, S. and Doi, N.: An Eﬃcientand Generic Reversible Debugger using the Virtualて，任意の文は可逆実行可能であることが示される．
Machine based Approach, Proceedings of the 1st定理 12. 任意の文 s について，I[[s]] は R[[s]] の左逆文でACM/USENIX International Conference on Virある．
tual Execution Environments (VEE ’05), pp. 79–88
なお，一般に，I[[s]] は R[[s]] の逆文ではない．実際，s が(2005).
x = 1 のとき，まず SAVE によって実行直前の x のデータを記録すれば，RESTORE(x) が左逆文となることが予想で [5] Landauer, R.: Irreversibility and Heat Generationin the Computing Process, IBM Journal of Research
きるが，記憶域に記録されたデータがない場合，RESTOREand Development, Vol. 5, No. 3, pp. 183–191 (1961).
を用いることができないので，右逆文ではない．

4

おわりに

本研究では，命令型プログラミング言語におけるプログラム可逆変換の形式化を行った．これにより，本研究の対象となる形式化された言語において，プログラム可逆変換が形式的に正しいことを保証した．
C 言語が対象であるが，形式的意味論が公式に存在しないことから，形式化された C 言語のサブセット Clight[6] Lutz, C.: Janus: A time-reversible language, Letter
to R. Landauer. http://www.cise.ufl.edu/~mpf/rc/janus.html (1986).
[7] Perumalla, K. S. and Fujimoto, R. M.: Source-code
Transformations for Eﬃcient Reversibility, Technical
Report GIT-CC-99-21, Georgia Institute of Technology (1999).