エアPOPL/Air POPL 2012: 39th ACM Air Symposium on Principles of Programming Languages
-
xhl_kogitsune
- 4029
- 2
- 3
- 0
-
- いいね！0
Deprecated: おねーちゃんですよ!⚓/xhl_kogitsune
@xhl_kogitsune
Underspecified Harnesses and Interleaved Bugs http://t.co/iOn63oY3 #air_POPL アッこれ面白いというかAbst分かりやすい!
2012-01-26 01:40:00
Deprecated: おねーちゃんですよ!⚓/xhl_kogitsune
@xhl_kogitsune
Static analysisでバグ検出する時に、precondition(引数は正常にopenされたファイルハンドルである、等)を正確に把握反映させないと、false positive出まくる問題がある #air_POPL
2012-01-26 01:41:04
Deprecated: おねーちゃんですよ!⚓/xhl_kogitsune
@xhl_kogitsune
この論文では、interleaved bug、「sequential実行だと常に正しいが並列実行でinterleaveするとバグになる」という類のbugを見つけるということにフォーカス #air_POPL
2012-01-26 01:42:22
Deprecated: おねーちゃんですよ!⚓/xhl_kogitsune
@xhl_kogitsune
本文未読だけどおそらくこの「sequential実行だと正しく動く」という前提により、preconditionは何かということが間接的に把握できて「これはfalse positiveだから無視、だってこれsequential実行時にも出るじゃん」とかできるのでは#air_POPL
2012-01-26 01:43:53
Deprecated: おねーちゃんですよ!⚓/xhl_kogitsune
@xhl_kogitsune
あ、あってた模様。 "Find violations to assertions assuming that the sequential executions (略) do not violate any assertion." #air_POPL
2012-01-26 01:45:36
病気の美少女
@lyrical_logical
"Underspecified Harnesses and Interleaved Bugs" 静的解析するときに「暗黙の仮定」を知らないために false alarm なりまくって困ることがある。続く。 #air_POPL
2012-01-28 13:01:11
病気の美少女
@lyrical_logical
でまあ concurrent なプログラムを検証するんだけども、ここで interleaved bug というのを定義してやる。これは sequential に実行すれば問題ないけど concurrent に実行するとおかしくなるバグ。 #air_POPL
2012-01-28 13:04:25
病気の美少女
@lyrical_logical
concurrent なプログラムのバグというのはその concurrency に起因するものだろうという仮定でもって、interleaved bug でないものは「暗黙の仮定」により守られた false positive ということにする。 #air_POPL
2012-01-28 13:05:55
病気の美少女
@lyrical_logical
ということで CBUGS ていうのを作ってみたよ、アブスト終わり。最後に比較があるだろうと思ってみてみたら windows のデバイスドライバ（そういえばデバイスドライバ用の何か MS が出してましたね）に対して適用したのがあるんだけど、見方が分からない！ #air_POPL
2012-01-28 13:09:53Towards a Program Logic for JavaScript (Philippa Gardner, Sergio Maffeis, and Gareth Smith)
kinaba
@kinaba
Towards a Program Logic for JavaScript、Separation LogicをC言語に使うのの延長的な感じでJavaScript用論理。こういうのは今イチやりたいことがわからんなーというのが正直な感想かもしれない #air_POPL
2012-01-26 02:03:58
kinaba
@kinaba
スコープ規則とかプロトタイプチェーンとかwithとかって、物凄く薄いdesugaringで剥がせるのを剥がさないで真っ向から扱おうとしなくてもみたいな、逆にその"剥がす"のが難しいのなら同じコードパターンをとってるCのコードの検証の時点で難しいはずで云々。
2012-01-26 02:10:46
Κeіsuke Νakanο
@ksknac
Towards a Program Logic for JavaScript: JSのためのseparation logic． prototype chain を追跡できるような仕組みを導入． (字が小さくてこの広さでは読めない) #popl12
2012-01-26 02:13:22
病気の美少女
@lyrical_logical
"Towards a Program Logic for JavaScript" タイトルからしてヤバそう #air_POPL
2012-01-28 13:13:48
病気の美少女
@lyrical_logical
js は web プログラミングのクライアント側で使われまくってるけどバグ入れやすいし静的解析の恩恵も受けづらくてちょっとやめないかなので、プロトタイプ継承をちゃんと含む js の subset に対しで seplog でとにかくなんとかどうにかせよみたいな話 #air_POPL
2012-01-28 13:24:50
病気の美少女
@lyrical_logical
うーん js_of_ocaml とか HaXe 使えば？みたいな気持ちになるしプロトタイプ継承に対する意味づけみたいなのも興味ないので次 #air_POPL
2012-01-28 13:25:391.B: Semantics
Higher-Order Functional Reactive Programming in Bounded Space (Neelakantan R. Krishnaswami, Nick Benton and Jan Hoffmann)
Κeіsuke Νakanο
@ksknac
Higher-Order Functional Reactive Programming in Bounded Space: 従来のFRPだと先読みが書きにくいし，無理に書こうとするとメモリリークが起きる． ストリーム型にdelayや線形型を導入することで解決． #popl12
2012-01-26 01:20:34