情報科学演習III小林研究室課題6
Proof Carrying Code (PCC) または Typed-Assebly Language (TAL) の設計
基本的な PCC や TAL のアイデアについては別項に譲るとして、ここでは課題の説明をします。
課題は、大まかに言って、次の２つ（余力があれば３つ）になります。
-
参考文献を読んで PCC や TAL がどういうものか理解する。参考文献は下を見てください。これらを全部読まなければいけないわけではありません。
-
適当な assembly 言語を選んで PCC または TAL を設計する。適当な、と書きましたが、おすすめは3年の演習で作った
or 作っている :-) CPU の命令セットです。命令セットの大きさも適当ですし、命令セットを勉強する手間も省けます。
-
実装 (PCC の proof checker、または TAL の typechecker） する。これができれば、自分達の作った/ているコンパイラの出しているコードが自分の設計した
PCC/TAL の安全性の基準（例： calling convention, memory usage, termination
） を満たしているか確かめることができます。ひいてはコンパイラのバグなんかも見つけられるかもしれません。（もう見つけたくないかもしれませんが）
参考文献
-
George C. Necula, Peter Lee. Safe Kernel Extensions Without Run-Time Checking.
OSDI'96,October 1996.
-
George C. Necula, Peter Lee. Proof-Carrying Code. POPL'97, January 1997.
-
Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F
to Typed Assembly Language, POPL'98, January 1998.
-
Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-Based Typed
Assembly Language, TIC'98, May 1998.
参考ＵＲＬ (論文もいくつかは download できます）
課題一覧へ
：
igarashi@is.s.u-tokyo.ac.jp