いろいろあって、障害というものについてちょっとだけ書いてみる。 万が一のときに壊滅的致命的破滅的災害にいたる技術を、人間は使っていいものか。 いい方悪いが飛行機事故で最悪1000人規模。スタジアムに落ちれば桁がかわってくるか。では原発事故では？…

イタリアのPostgreSQL Users Groupからのメッセージ。JPUGのあるメンバー向けメッセージですが、複数のMLにすでに流れているので、勝手に転載。 I want to express our deepest sympathy for the recents events in Japan. We hope that your families and l…

名前しか知らなかったjavaPathFinderを数時間いじってみた。 ダウンロード、セットアップ JavaPathFinderから最新版をダウンロード。解凍すれば問題なく動作する。 できること Javaのバイトコードを読み込んで、デッドロックや競合状態の有無などを検査する…

2005年ころ、PostgreSQL+QueryCacheという実験をやっていたことをふと思い出す。今みてもソースが汚い。ソースよりも「インスパイヤライセンス」を書きたくて作った側面も否定できず。

実際に使われている800行規模のCプログラムに対してCBMCを使ってみる。 ここでは拙作mcbというmemcachedのベンチマークプログラムを俎上にのせる。このプログラムのバージョン1.0rc2はここで指摘されているように、初歩的なミスを含んでいる稚拙なものであっ…

次回に向けて、はやくも落ち穂拾い。 double intだけでなくdoubleでも使えるか、確認。 #include <stdio.h> #include <stdlib.h> #include <assert.h> int main (int argc, char **argv) { int _rand = rand(); double r; #ifdef __CBMC__ __CPROVER_assume(0 <= _rand && _rand <= RAND_M</assert.h></stdlib.h></stdio.h>…

Postgres-XCの単一障害点であるgtmを多重化するmgtmを作ったので公表する。これはAPPIA版の改良でJGroupsを使っている。 2011年2月現在、最新版はver0.9.3〜0.9.4だが、mgtmはver0.9.2で動作する。もうすこしUI修正や動作を整えてから公開しようと思ったが、…

昨日、某懇親会で天文関係者と話す機会があり、なぜか一瞬フォーマルメソッドの話に。情報工学ってのはほんとにサイエンスなのかい？*1ってな流れから。 否定的な意見も少なくないフォーマルメソッドについて、注目している理由を書いてみる。 それ動くの? …

"CBMC"というモデル検査ツールの使い方を学ぶ。組込み分野では有名なツール。すでに開発終了したという人もいる*1が、最新版3.9は2010.12.19リリース。2010年には3.6,3.7,3.8,3.9と4バージョンリリースなので、アクティビティが落ちているようにはみえない。…

ポツポツとアクセスがあるのでアップデイト。2011年1月現在、最新版はver0.9.3だが、ver0.9.2で動作するgtmとgtm_proxyのJava版を作ったので公表する。 ダウンロード jgtm-0.3.2a.jarをダウンロードする。Java1.5以上のJDK、もしくはJREを用意すること。つづ…