CBMC

検証

いつの間にかCBMCがオープンソースになっていた。 http://www.cprover.org/cbmc/svnでversion4.1のソースをダウンロードできる。 svn co http://www.cprover.org/svn/cbmc/releases/cbmc-4.1 これらを書いたころはver2.4のみソースが公開され、Currentの3.9…

2011-06-10

障害に関すること

検証

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

2011-03-07

JavaPathFinderの備忘録

検証

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

2011-03-01

CBMCの使い方入門:3

検証

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

2011-02-28

CBMCの使い方入門:2

検証

次回に向けて、はやくも落ち穂拾い。 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>…

2011-02-26

Postgres-XC GTM(GlobalTransactionManager)の多重化　JGroups版

PostgreSQL 検証

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