PR

 形式検証や形式手法を対象とした専門学会「ATVA 2008(6th International Symposium on Automated Technology for Verification)」(ホームページ)が10月20日~23日に開催された。AVTAは2003年の開始以来,アジアの都市で行なわれており,今年は韓国のソウルでの開催だった。

 今回のATVAでは,27カ国から66件の研究論文と16件のツール論文の投稿があり,その内研究論文21件,ツール論文7件,ショート・ペーパー7件が採択された。参加者は全体で70名程度とこぢんまりとした学会だが,主催の韓国をはじめ,日本,中国,台湾,インド,米国、フランス,ベルギー,アルジェリア,ナイジェリア,スペイン,イスラエル,ノルウェー,カナダ,チェコ,ドイツ,スウェーデン,オーストラリア,イタリア,南アフリカ,などからの参加があり,非常に国際色豊かな学会だった。

 この学会の2日目に,並行プログラムのスレッド実行順を扱った発表が米NEC Laboratories America, Inc.(NECLA)らからあった。同社は2008年6月に開催の「44 th Design Automation Conference(DAC 2008)」でも,このテーマに関して米University of California, San Diegoと共同発表している(Tech-On!関連記事)。

従来手法は網羅性や規模に難点

 今回NECLAはUniversity of Utahと共同研究しており,その成果をNECLAのChao Wang氏がSession 2:Software Verificationで発表した。講演のタイトルは,「Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions」である。同氏は,共有変数アクセスでのレーシング検出を高速化する手法を提案した。この手法は,ロック変数を用いて共有変数への排他制御を実現している,スレッド・プログラムを対象にする。

 従来の検出手法は,シミュレーション・ベースだったり,モデル・チェッキングを利用していたが,検出の網羅性や実行時間などに問題があった。任意のインタリービング実行を深さ優先探索で構築し,Partial Order Reduction(半順序簡約)手法を用いて探索すべき実行系列を削減することで高速化する手法も提案されているが,対応できる規模に難点があった。