* * *
* *"> *
* * *
Akihito Nagata's Page
|
|
今までに読んだ論文の感想keyboard
Security in Plan 9(Russ Cox, Eric Grosse, Rob Pike, Dave Presotto, Sean Quinlan at Proceedings of the 11th USENIX Security Symposium)
米澤先生の授業で読むことになった論文。セキュリティは良く知らないので勉強しなくては。
Plan9というのは Unixを作った Bell研が UNIXの問題( = 分散環境に適合できなくなっている) を克服するために作ったOSらしい。 ここのワークステーションにばらばらのソフトウェアがあるのが今の現状なのでどうにかしてネットワークが一つのコンピュータのように見え、均一で集中化されたしかも柔軟なOSを目指している。
Unixに比べて、
  • エンドユーザの自由度が飛躍的に向上した事
  • 分散配置されたマシンを高度に統合性できる事
  • システム編成が柔軟に行える事
  • 高度なセキュリティ機構を備えている事
  • 新しいバックアップメカニズムを備えている事
のような特徴を持っている。
今回の論文はこの中のセキュリティについて学びます。
A Type Theory for Memory Allocation and Data Layout(Leaf Petersen,Rorbert Harper, Karl Crary, Frank Pfenning
高レベルなデータ構造の実際の表現を気にすることができるような、低レベルな言語でも、型システムを用いてメモリの安全性が保証できるぞという論文。型情報でいっぱいになってしまうTALとは違うらしい。できることはヒープ領域のメモリを複数のオブジェクトの分同時にとってしまういう最適化。この最適化によりどれほど効率があがるのか?それは書いてなかった。
Linear types can chage the world!
Linear Typeがなんなのか学びたいと思います。
Linear Typeというのを定義する。Linear Typeというのは1回作られて1回だけ使われるようなオブジェクトの型。複製されたりそのまま捨てられては駄目。でも全てのオブジェクトがLinear Typeのような言語は表現力に欠けるので普通のNonlinear Typeと共存させます。1回しかみないオブジェクトはそれを壊しながらupdateできるのでGCとかよりも効率がよい。(2002.3.21)
Flow-Sensitive Type Qualifiers
よくわからないけれど、ファイルなどのオブジェクトの使用方法を推論してバグを見つける論文。Related Workに五十嵐さんと小林さんの論文が入っていてすごい。僕も参照されてみたいです。
しかし、前提となる知識が足りなくて断念。一度読むのをあきらめました。やはりとりあえずlinearがなんなのかわかりたいです。(2002.3.15)
普通の型システムのtype qualifiersをつけます。型は場所に関係なくつけられる(flow insensitive)けど、リソースのプロパティはプログラムでの場所に依存するのでflow sensitiveなqualifiersにする。どうやらquolifiersはユーザーが指定するみたい。それを正しいかどうか確かめる。
頑張って読んだ。effect,linear type,store,restrictionなどいろいろ学べて良かった。でもPOPLではうまく発表できなかった。残念だ。次回はちゃんと発表できるようにします。(2002.4.17)
PPL & SPA
はじめて学会というものに参加しました。
大分の別府で温泉に入りながらの学会でした。自分も卒論のscheme-to-javaをSPAのポスターセッションで発表させてもらいました。ポスターセッションは教授などに自分の研究をみてもらって突っ込んでもらうための発表というような感じだったけれど、ほとんどの突っ込みには答えられた気がします。住井さん他、米澤研の人に大感謝という感じです。
あとRubyの作者のまつもとさんに興味を持ってもらえてお話ができました(少しだけど)。
発表がない時間は他の学校の人といろいろ話をすることができて。非常に楽しかったです。来年も参加できたらと思います。来年はポスター発表ではなくショート発表くらいに格上げしたいものです。あと個人的に旅行が苦手なので近いところ希望です。
残念だったことは他の人の発表がほとんど理解できなかったところ。前提となる知識がないもんだから何が新しいのかもわからないし内容もよくわからない。わからないながらもlinear typeというものに興味を持ってみました。調べてみようと思います。
あとそこで発表した僕の卒論です。(ps)(2002.3.5 - 2002.3.7)
Memory Controlled Spill Code for Software Pipelining
ループをソフトウエアパイプラインに変換すると使用するレジスタの数が増えてしまう。もしこの要求されるレジスタ数がマシンの持っている数よりも多くなってしまった場合は使用するレジスタ数を減らす必要がある。減らすには1、各ステージを長くする。2、変数をメモリに吐き出す。の2通りがあるが、これらの2つを両方適度に使うことでどちらか一方よりもいい結果が出せる。という論文。
組み合わせるあたりが自分の卒論と似てて好感触。レジスタ割り当てがどうこういうより実際にどうやってソフトウエアパイプラインに変換するのが気になります。これはこれでわかりやすくてよかったけど。(2002.2.26)
No Assembly Required: Compiling Standard ML to C
Cにどうやってtail callを実装するか、だけのために参照しました。そこ以外は全然よんでません。普通にCallしまくってスタックがあふれそうになったら区ロージャーを作って、スタックの底でまってるトランポリンという人に継続を渡します。スタックはあふれないけど、ジャンプの回数は変わらないのでそんなに速くはならないのでは?と。(2002.2.10)
Extending Java Virtual Machine to Improve Performance of Dynamically-typed Languages
動的型付け言語をJVMに効率良く実装するためにJVMを拡張。参照型とint型の両方を格納できるdescriptorという型をバイトコードに導入する。JVMの拡張なんて何から始めたらいいのかわかんないっす。さすが大岩さん。僕のSoft Typingと異なるアプローチとしていろいろ引き合いに出させて頂きました。(2002.2.10)
Kawa : Compiling Scheme to Java
これもScheme-to-Javaコンパイラ。コンパイラとしても使えるが、クラスローダを利用してJITっぽくインタプリタとしても使える。Schemeの正しいnumber型を目指したりcall-ccを部分的に実装したりとR5RSに近づける工夫がいっぱい。また一般の関数型言語-to-Javaを実装するためのライブラリとしても使えるらしい。(2002.2.10)
SILK -- a playful blend of Scheme to Java
僕の卒論のテーマと同じScheme-to-Java。こっちはコンパイラ。Schemeのコード中からJavaのクラスやらメソッドやらを扱える。すごい。(2002.2.10)
Tail call elimination on the Java Virtual Machine
Javaのバイトコードでどうにかしてproperなtail callを実装しようとした論文。自分自身を呼び出す末尾再帰ならば単純なfor loopに置き換えることができ、この場合は速いしスタックものびない。しかしJavaはメソッドの長さに制限があるのでこの方法は不向きな場合があるらしい。他にはコンティニュエーションを頑張って作るなど方法があるようだけど、バイトコードではジャンプを減らし速さを向上させるためのproperなtail callは無理でスタックを伸ばさない用にするのが精一杯という感じ。(2002.2.10)
A Practical Soft Type System for Scheme
Schemeに実際にSoft Typingをする。長い論文。Static Typeなど新しい概念が多くて読むのがたいへん。 アブセントバリアブルという特殊な型変数を設定することでプロシジャを複製すること無くポリモルフィックにできる。(2001.11.28)
Compiling Standard ML to Java Bytecodes
SMLをJavaにコンパイルする。ポリモーフィズムはすべての型に対してコードを作るというSTLまがいのことをしていた。でもバイトコードにコンパイルすることを利用して関数をただのイテレータに変換するなど頑張ってた。関数を引数に渡す場合はそれぞれのタイプについてインターフェースを作りそのオブジェクトとして渡す。よって使われる全てのインターフェースを作る必要があった。シグニチャを書くことで隠蔽をすることができるけど、外に見える部分では関数渡しのできる関数は定義できないようになってた。
あとSMLとOcamlは微妙に書式が違ってうまく書けない。(2001.11.20)
Safe polymorphic type inference for a Dynamically Typed Language:Translating Scheme to ML
SchemeのソースをMLのソースに変換しようという論文。動的型チェックのSchemeをできるところは静的に型チェックしてしまうことりにより効率化を計る。なんとなーくわかったけど自分の英語力の無さのため十分にはわからなかった。東大記録会のテントの中で読んだ。寒かった。(2001.11.6)
Soft Typing
MLのように厳格に静的に型をつけてしまうのではなく、ランタイムの型チェックも許して適度に型をつけましょう。これでSchemeにも型をつけることができます。でも重要なところはfull paperを参照してくれと書いてありfull papaerを参照すると非常に長々と書いてあるため読む気が無くなる感じだった。(2001.10.23)
|
前のページはこちら