AWSにおける形式手法の適用 ― 2015年10月21日 10:56
Communications of the ACM、2015年4月号から。AWSで形式手法(Fomal Methods)を適用して成果を上げているとの記事の寄稿。
クラウドのサービスを利用することがあたりまえになってきた中、それらのサービスの品質が満足行くものか、一抹の不安を抱えながら、ということはよくある。本稿は、AWSでS3やDynamoDBなどの構築に携わった面々が、形式手法を適用して、簡単には見つからない設計バグの解消に取り組んだ事例を報告する。
バグを解消する、というと、幾多のレビューを受け、考えられるだけのテストケースと負荷試験を十分な時間を掛けて実施し、というのがよくあるが、AWSのように同時並行で多数の処理が動き、それぞれが複雑に作用し合うサービスでは、それだけでは十分でなかった。その解決を模索する中で、形式手法にたどりつき、DynamoDBのプロジェクトで成果を上げてから、S3をはじめ、他のプロジェクトに普及していったという。
トラブルが発生すると、どれだけの人と時間を投入して改善した、ミスを発生させた人員にはペナルティを課す、監視システムを充実させた、などの対応策を説明されることがあるが、これらで本当にトラブルがなくなるのか、納得するのは難しいのが本当のところ。その点、本稿にあるようなAWSの取り組みは本質に迫り、安心感を高める。
なお、Amazonが、自社のプロジェクトに適していると判断したのは、TLA+とそれを元にしたアルゴリズム記述言語のPlusCal。ちょっと見た感じ、記号論理学で習った記述に近しいやり方で、処理のロジック(アルゴリズム)を書き下している。
※TLA+の解説
スノーデン以後のプライバシー意識 ― 2015年10月21日 11:51
Communications of the ACMの2015年5月号から。
スノーデン以後の米国民のプライバシー意識についての調査報告。本稿によると2013年の暴露以後、プライバシーを守るという行動は高まりを見せたものの、すぐに元に戻り、現在ではむしろ低下しているという。
懸念はあるのかもしれないが、便利なものは使ってしまう、ということか。感覚としては、身内や近所で話をしているのと変わらないのかもしれないが、今の技術では見知らぬ人や機関がそれを記録して、利用することができるようになっている。本人が気にしないならよいのでは、という意見もあろうが、自由と独立を口にするなら意識的でありたい。
別稿になるが、知的財産権(Intellectual Property)についての記事で、Bill Gatesが言ったという格言が面白い。
Intellectual Property has the shelf life of a banana.
知的財産権の賞味期限は、バナナなみ（に短い）。
これを伸ばそうという動きについて議論するのだが、バナナの対極におかれたのが、Twinkiesというお菓子。少し前に、製造を止めるといって大きなニュースになっていた。
満を持して主機をWindows10にUpgrade ― 2015年10月23日 20:55
まわりの対応も進展してきたので、満を持して主機をWindows10にUpgrade。
バックアップとして、Windows8.1のシステムイメージを取得の後、アップグレードを実施。8コアにSSDでもあるので、タブレットと異なり、ぐっと速い。
ところが、バックアップ用の外付けドライブを外すのを忘れていたため、中身のチェック処理が入り、セットアップに時間を要す羽目に。これは失敗。
アップグレード終了後、画面下部のタスクバーにアイコンが出ない。しばらく我慢しているとふと現れる。バックグラウンドの移行作業はしばらくつづくようだ。体感で30分ほどだったか。
アップグレード後、使えなくなるデバイスを心配したが、主だったものの内、NGだったのは、RolandのUSB外付け音源（UA-25）。型は古いが、8.1の時も、Rolandからは遅れたもののドライバは提供されたので、しばらく待ってみる。当分は、別のデバイスから出力。それとも、DSD対応のものを新調した方が良いか。心配した、Blackmagicのキャプチャボードは問題なし。
つづいて、主なアプリケーションの起動確認。
・少し古めのOffice2010や一太郎2014もOK。
・eBookJapanのReaderは、本を開くと中身が白紙になったが、ログインをやり直し、PCを改めて登録することで回復。本によっては、アップロードの上、改めてダウンロードする必要がある。
少し問題が出たのは、VMware Workstation10。仮想ネットワークのブリッジ接続が無効になっている。VMwareのコミュニティでもずいぶんと話題になっていた。Windowsアプリ開発時のテストで使用するには、リモート接続が必要なので、NATでは困る。
※VMwareのコミュニティの議論
結論から言うと、アップグレード時に、VMware Bridge Protocolがアンインストールされていたのが原因のよう。改めて、NICのプロパティからインストールすると、無事、ブリッジ接続は復旧。
元のOSに戻す予定がなければ、作業用のファイルを削除。約27GBほど使用していた。
Giuliano Carmignola with Venice Baroque Orchestra @三鷹 ― 2015年10月24日 23:04
久しぶりのコンサート。今日は三鷹。
会場の三鷹市芸術文化センター。定員は600人余。箱形で三方を二階席が囲む。昔のカザルスホールに似ている。今回は、よく見えるように二階席。会場は撮影禁止。
奏者は、Giuliano CarmignolaとVenice Baroque Orchestra。気心の知れた組み合わせ。個人的には、2010年の来日以来。演目は、All Venice Program。A.Vivaldiを中心に、Veniceで同時期（18世紀前半のあたり、日本だと将軍吉宗の頃）に活躍した作曲家の作品から。紀尾井ホールの公演もあったが、こちらは半分が、J.S.Bachのプログラム。ここは、Vivaldiを堪能したく、三鷹へ。
演奏は、前回と同じく、最初の数曲をオーケストラの面々が熱演し、場が暖まったところで、Carmignolaが登場。実際のところは、ソロが引き立つ演目なってから登場というところ。
今回は、プログラムに楽器の紹介はないが、艶のある音色は健在。見事な弦さばきを見ていると、バイオリンは、大柄なイタリア男性の体格に合わせて設計されているのだと思えてくる（小柄な方にはごめんなさい）。オーケストラ共々、キレのある演奏。ソロと合奏の掛け合い、間と呼吸の見事さ。生ならではの、全身で感じる音の厚み。
Veniceに縁の曲のなせる技か、奏者もどんどん調子に乗ってくる。よほど、気分がよかったのか、4曲ものアンコール。CDになっている2台のヴァイオリンのための協奏曲や、四季の夏からなど。四季が奏せられて終わりと皆が思った後の、最後のアンコールには会場がどよめく。
アンコールの最後の方は最前列は立ち上がる人も大勢。さすがに光る棒は登場しないが、人気のパフォーマーのライブさながら。当時の演奏の様子はわからないが、曲想から判断するなら、行儀よすぎず、観客と距離感の近いライブのような演奏会もあっていい、と思えてくる。
最近のコメント