日々の流転

λ. “Checking Race Freedom via Linear Programming” by Tachio Terauchi

We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to (rational) linear programming. Unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. We achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying an implementation to real world C programs.

を読んだ。先日のPPL2008で発表されていたもの。そのときはちょっと良く分からなかったのだけど、改めて読んでみるとやっぱり面白いなぁ。線形計画法(linear programming)をこんなことに使えるなんて思いもよらなかった。

リファレンスにアクセスする権限をスレッド間で分け合ったり受け渡したりする。権限を少しでも持っていれば読み込みが出来て、権限を全部持っていると書き込みが出来る。それで、権限を非負の有理数で、制約を不等式で表現して、線形計画法のソルバを使って制約を充足するような割り当てが存在するかをチェックする。

C言語とpthreadで書かれたプログラムを検証するためのプロトタイプが実装済み。フロントエンドしてCILを使い、線形計画法のソルバにはGLPK (GNU Linear Programming Kit)を使っている。

ちょうど半年前くらいにGLPKとGLPKで楽しく最適化しよう！というページを知人に教えてもらったんだけど、それにしてもこんなことに使えるとは……

λ. パニックルーム

テレビでやっていたので見た。 こんな狭い舞台でどんな話が展開するのかと思ったが、結構面白かった。