yukobaのブログ

■Flashの未来をFLASH MEETUPで聞いてきた！

先ほどまで、FLASH MEETUP http://atnd.org/events/22297 があり、Adobe Flash の現状・未来についての質疑応答のイベントがありました。Flash の技術の偉い方のちゃんとわかっている人が3名アメリカから来ていて、超内容が濃かったです！7〜9時の予定が11時まで延長して、京都から来た方は泊まりこみになりました！

Flash 関係で、最近誤解を招いてしまったことについて解説があったのですが、まぁ、ネットではたくさん出ているので、Flash の今後について話していたことについてこの記事では書きます。

あと、僕、間違ったことを書いていたらごめんなさい。私見も混じっています。アドビの太田禎一さん @otachan さんに聞くと色々と教えてくださると思います。

全体の方針

現状、Flash がよく使われているのは、「ゲーム」「動画」「広告」なんですが、ゲームと動画に今後は注力していくとしていました。

Stage 3D

Flash Player 11.0 から入った GPU を呼び出せる Stage 3D ですが、方針としては、

• 2D フレームワーク や 3D フレームワーク経由で使ってね。
  • 2D フレームワークは Starling などがあるのですが、（私見：3D 程は注目されていなく）ぜひぜひ使ってね、と言っていました。Angry Bird は Starling を使って書いた Flash 版を発表するそうです。
  • 2D でも結構フレームレート良くなるそうです
  • ソフトウェアレンダリングエンジンになってしまった場合でも、Flash 10.x の方式よりも速いそうです
• Adobe 自前ではこれらのフレームワークを作ることはなく、その下のレイヤーだけに注力する。
• 3D のオーサリングツールも作らない。Flare3D のオーサリングツールを紹介していました。

あと比較的高度な話として、

• 11.0 では Pixel Bender 3D で for ループが出来なかったり、描画命令もすごく種類が少ないのは、広範にいろいろなコンピュータでテストしてみたところ、あまりにもちゃんと動いてくれない GPU が多すぎて、その結果、こういう命令になった。GPU ベンダーにバグ修正の要望を色々出している。
• バグのある GPU は動作させないブラックリストを Flash Player は持っていて、統計的に 50% 近く弾いている。そのリストは今後公開予定。最新のドライバなら動く GPU でも、ドライバのバージョンが古かったりするとブラックリスト入りしている場合がある。最初のインキュベータ版では「2009年1月よりも前にリリースされたドライバ」を全て弾いていたそうです。
  • 個人的には、Flash Player の力で、ビデオカードのドライバのバージョンが古い場合、ダウンロードしてインストールする機能をつけてしまっても良い気がしました！
• それでも、WebGL のブラックリストよりは広範囲のドライバをサポートしている。（例えば、WebGL の場合、第１世代 Core i の Intel HD Graphics ですらブラックリストに入っています）

モバイル関係としては、

• モバイル Adobe AIR の Stage 3D 対応は2012年頭までにはやります。たぶん、まもなく出る、Flash Player 11.2 でサポートするという意味だと思います。これのデモもやっていました。

HTML 5 向けのアニメーションツール

Adobe Edge で HTML 5 向けの2Dアニメーションオーサリングツールを公開していますが、スマートフォンが HTML 5 しか使えなくなった以上、これは積極的に投資してく方針みたいです。CS6 -> CS7 とどんどんこの手の機能を良くしてく感じみたいです。話の流れだと、Adobe 製のアニメーションツールで <canvas> 相手に生成できるのも積極的に作っていくみたいな感じでした（たぶん）。「この手の大型のオーサリングツールが市場に出ていないからね」という感じでポロッと言っていました。（でも、Flash と違って独占にはならないから、アメリカベンチャーから強いライバルが出る可能性もありそう…）

なんか、話の感じだと、ActionScript 3 → JavaScript のコンパイラも研究している感じでした。本当か？

ここらへんの話は特にデモがなく、詳細は不明です。

プロファイリングツール

Flash の新しいプロファインリグツール（ボトルネックを探すツール）のデモもやりました。フレームごとに、どの処理・スクリプトに何msかかったか見ることができる GUI ツールです。良い感じでしたよ！スマートフォン相手にも Wifi 経由でリモートプロファイリングができるそうです。

サイレントアップデート

Flash Player 11.2 からサイレントアップデートの機能が入り、ユーザーが拒否しない限り、Google Chrome みたく、勝手に自動的にアップデートするようになりました。これを、Mac OS X にも近いうちに入れる予定だそうです。（Liunx は yum や apt などに頼るのでしょう）

サウンド

現状200〜250ms 程度サウンドのレイテンシがあるそうですが、それを 40ms 程度まで短縮した Flash Player を今後出すそうです。

国際化

これは会場の質問から出たのですが、Flash が日本語など非英語圏でテストが甘くバグが多い、という文句が出たのですが、（日本語入力がテキストフィールドでできなくなったり、マイク選択で英語以外のデバイス名が含んでいると動作がおかしくなるなど）、「頑張ります」的な回答しかなかったのですが、日本語でバグレポートを出来る場を作って欲しいと言われていて、これはそのとおりだと思います。

Alchemy 2

C/C++ ライブラリを Flash Player 内で動かす Alchemy ですが、一度死にかかった感じがあるのですが、Alchemy 2 としてちゃんと再生させることが発表されています。（技術的に何が変わるのか質問したかったのですが、タイムオーバーで質問出来なかった）。話によると、ネイティブと変わらないパフォーマンスで動いているよと言っていました。コンパイラは LLVM のコンパイラなので、最適化関係は LLVM の強力な最適化で行われるのですが、あとは、生成される命令がどの程度ちゃんと JIT されるかなんですが、まぁ、期待！

ネイティブエクステンションという選択肢も Adobe AIR ではありますが、

• パーフォマンスが理由なら、Alchemy 2 を使って
• OS の特殊な API を呼び出したいなら、ネイティブエクステンションを使って

という使い分け方を推奨していました。

Flex

Flex にさく予算は減らし、Apache 管轄で、コミュニティ主導で維持していくと発表していました。僕の意見として、HTML 4 でできることは Flash でやらないほうが良いことが多く（日本語入力にバグがあるなどの理由から）、Flex は HTML 4 と被る部分が多く、HTML 4 と被る部分は積極的に投資しないというのは正しい判断だと思います。

Text Layout Framework

Text Layout Framework は Flex の一部になっているけれど、純粋に一部というわけではないので、これはちゃんとメンテナンスしていくと言っていました。

こんな内容だったかな。少し上記、報道というよりは、私見も混じっていてすいません。動画関係も抜けています。

ツイートする

■mixiアプリのユーザーIDプラットフォーム共通化の移行方法

mixiが海外のSNSとプラットフォーム共通化をするらしく、その関係で、今まで数字のIDだったのが、文字列のIDに切り替わります。その関係で、mixiアプリ提供者は今月中(2011年10月)に新方式に移行が必要です。

http://developer.mixi.co.jp/news/news_apps/009668.html

なんか、あまり手法とかブログで見かけなかったので、やり方とか書いておきます。手抜きしたい方の参考にどうぞ。

まず、変わるのは、ID だけで、API は変わりません。今まで、ID を文字列で管理していた人は、データベースの ID さえ、差し替えてしまえば対応完了です。数値でやっていた人は、文字列にプログラムを書き換える必要があります。

一連の話、テストアプリで一通り練習してから、本番アプリで行ってくださいね。

ステップ1

http://developer.mixi.co.jp/appli/com/change/setting/trans_id/ にあるように、ID変換API の申請をします。アプリが稼働中の状態でやってしまっても、通常は大丈夫です。

ステップ2

まず、旧ID の一覧が必要です。in.csv は（1列のCSV、つまりカンマなし）で旧IDをずらずらと並べた形式にしました。

in.csv の作り方は、アプリ次第ですが、僕の場合は、PostgreSQL でこんな感じでした。

COPY (SELECT mixi_id FROM account_mixi) TO '/tmp/in.csv' CSV;

ステップ3

次は、旧ID → 新ID の変換です。RESTful API を使うと、変換表が手に入ります。こんな感じの Java のアプリでやりました。http://code.google.com/p/opensocial-java-client/ が必要です。

java -classpath .;opensocial-1.0.jar;commons-codec-1.3.jar;json_simple-1.1.jar;oauth-20090825.jar MixiOldIdConverter in.csv out.csv failed.csv

で実行します。一度実行したら、out.csv や failed.csv に保管するので、2回目は差分だけ実行できます。1回目は、アプリが動いた状況で実行し、その後必要なら、数回、アプリが実行している状態で行い、最後にアプリを停止して変換すると、アプリの停止時間を小さく出来ます。

import org.opensocial.Client;
import org.opensocial.Request;
import org.opensocial.RequestException;
import org.opensocial.Response;
import org.opensocial.auth.OAuth2LeggedScheme;
import org.opensocial.models.Model;
import org.opensocial.services.PeopleService;

import java.io.*;
import java.util.Date;
import java.util.HashSet;

public class MixiOldIdConverter {
    // 本番
    private static final String consumerKey = "fuga";
    private static final String consumerSecret = "barbar";
    // テスト
//    private static final String consumerKey = "fugaTest";
//    private static final String consumerSecret = "barTest";

    public static void main(String[] args) throws IOException {
        File inFile = new File(args[0]);
        File outFile = new File(args[1]);
        File failedFile = new File(args[2]);

        HashSet<String> converted = new HashSet<String>();
        readOutFile(outFile, converted);
        readOutFile(failedFile, converted);

        BufferedReader reader = new BufferedReader(new FileReader(inFile));
        PrintWriter writer = new PrintWriter(new FileWriter(outFile, true));
        PrintWriter failedWriter = new PrintWriter(new FileWriter(failedFile, true));

        int lineNo = 0;
        String line;
        while((line = reader.readLine()) != null) {
            if (line.length() == 0) continue;
            if (converted.contains(line)) continue;
            lineNo++;

            try {
                String platformUserId = convert(line);
                writer.println(line + "," + platformUserId);
            } catch (Exception e) {
                //e.printStackTrace(); // ここコメントアウトしてもあまり問題ない
                failedWriter.println(line);
            }

            if ((lineNo % 10) == 0) System.out.println(lineNo + " " + new Date());
        }

        failedWriter.close();
        writer.close();
        reader.close();
    }

    private static void readOutFile(File outFile, HashSet<String> converted) throws IOException {
        if (outFile.exists()) {
            BufferedReader reader = new BufferedReader(new FileReader(outFile));
            String line;
            while((line = reader.readLine()) != null) {
                if (line.length() == 0) continue;
                converted.add(line.split(",")[0]);
            }
            reader.close();
        }
    }

    public static String convert(String oldId) throws IOException, RequestException {
        OAuth2LeggedScheme authScheme = new OAuth2LeggedScheme(consumerKey, consumerSecret, oldId);
        Client client = new Client(new MixiProvider(), authScheme);

        Request viewer = PeopleService.getViewer();
        viewer.addParameter("fields", "platformUserId");
        Response response = client.send(viewer);
        Model person = response.getEntry();

        return (String) person.getField("platformUserId");
    }
}

import org.opensocial.providers.Provider;

public class MixiProvider extends Provider {
    public MixiProvider(){
        super();

        setName("mixi");
        setVersion("0.8");
        setSignBodyHash(false);
        setRestEndpoint("http://api.mixi-platform.com/os/0.8/");
    }
}

ステップ4

1. Webアプリを停止する。
2. データベースのバックアップをとる。
3. in.csv の最終形を作る。
4. 変換して、out.csv の最終形を作る。
5. この後記載する SQL みたいな感じで、新 ID に置き換える。
6. 念のため、別なファイル名で、再度、データベースのバックアップをとる。
7. 「IDのプラットフォーム共通化対応完了」をクリック。これ以降、新 ID で mixi の方からは応答が来るようになります。
8. Webアプリを再開する。

CREATE TABLE old_new_mixi_id_map (
  old_mixi_id VARCHAR(255) PRIMARY KEY,
  new_mixi_id VARCHAR(255) NOT NULL
);

COPY old_new_mixi_id_map FROM '/tmp/out.csv' CSV;

UPDATE account_mixi SET mixi_id = 
  (SELECT new_mixi_id FROM old_new_mixi_id_map 
    WHERE old_new_mixi_id_map.old_mixi_id = account_mixi.mixi_id)
  WHERE mixi_id in (SELECT old_mixi_id FROM old_new_mixi_id_map);

場合によっては、他にも関連するテーブルの情報を削除する場合がアプリによってはあると思います。（僕の場合は、他に2カ所、データを削除しました）

ツイートする

■福島県飯舘村は屋内退避させるべきか否か

ソフトバンクの孫正義さんが、Twitterで、政府の出している避難指示に関して、http://twitter.com/masason/status/51832607117295616 以下のように書いていて、この問題についてです。

政府は飯舘村や南相馬市に明確な避難命令を出すべき。RT @mryoshi55: 政府が中途半端なことをするから、ここ米沢の避難所から飯館村や南相馬市に戻る避難者が今日出てきた、今はまだ止めた方が良いと思う

http://twitter.com/masason/status/51836389716795392

「直ちに問題無し」「避難命令拡大不要」を連呼する政治家や学者は自らの家族がそこにいても避難させないのだろうか？ @dunce_jp @masason: 政府は飯舘村や南相馬市に明確な避難命令を出すべき。

僕は、政治哲学として、「平時に決めた緊急時マニュアルはちゃんと守るべき」というのが僕のスタンスです。国が決めた、ルールは以下の通りです。

対策	外部被ばく	内部被ばく
屋内退避	10ミリシーベルト〜50ミリシーベルト	100ミリシーベルト〜500ミリシーベルト
避難	50ミリシーベルト以上	500ミリシーベルト以上

この問題、色々な単位が飛び交っていて、ややこしいのですが、これは「累積量」です。混乱している方もいますが、「1時間あたりの」というやつではないです。なお、1ミリシーベルト以下なら、日常で自然から浴びるレベルなので無視できるとされています。そして、健康被害が出るのは500ミリシーベルトといわれ、福島第一原発で命がけで作業に当たっている人たちで100ミリシーベルト以上被ばくしている人が多数いますが、今のところ大丈夫みたいです。国の基準の詳細は http://www.mext.go.jp/component/a_menu/other/detail/__icsFiles/afieldfile/2011/03/28/1304305_2810.pdf の末尾2ページをご覧ください。

現在は、

• 半径20km以内 - 避難
• 半径20〜30km以内 - 自主避難（元は屋内退避）

という指示が出ています。

あと、内部・外部とあるのですが、以下、「外部被ばく」の方で、計算します。なお、「内部被ばく」の方は、SPEEDIによるコンピューターによる概算の予測値があるのですが、外部被ばくの方は17日以降は実測値があり、より実際に近いはずなので、外部被ばくの方をみます。この違いも、ややこしいよね。

なお、僕はIT業界の人で、原子力は素人ですが、一連の話、超ひも理論（素粒子）を研究している友人に色々教えてもらいました。（ただし、彼も、厳密には原子力工学は専門じゃないです）。色々ありがとうね！あと、専門家の皆様、この記事に誤りを含んでいたら、訂正お願いいたします。m(_ _)m

次に、外部被ばくで問題となる、飛んでくる放射性物質ですが、風に流されて飛んできて、雨が降ると大量に地面に落ちてきて、地面に降りてくるとあまり動かなくなり、その場で放射線をまき散らすそうです。放射線には半減期というのがあり、例えば、今回、大量にばらまかれている、ヨウ素131だと、半減期が8日なので放射線の量は8日で1/2、16日で1/4とだんだん減っていきます。

そして、放射性物質が大量に飛散した原因は、3月15日あたりに、福島第一原発のバッテリーが切れた後、原子炉の格納容器内の圧力が高まったので、中の空気をそのまま外に逃がす作業を緊急的にやっていました。ここら辺の経緯は 福島第一原子力発電所事故 - Wikipedia をどうぞ。

ただし、この作業は、最近は行っていません。なので、

• 新たに放射性物質を大量飛散させるような作業を原発で行わない
• 雨が降っても、これ以上、放射性物質が大量に落ちてくることはない

ならば、あとは半減期で減っていくだけです。確証はもちろんないですが、現状の様子だと、この2つ、どっちも起きる可能性は低そうな気がします。（ちなみに、最近問題になっているのは、空気中ではなく、海に放射性物質をまき散らしています）

というわけで、新たに放射性物質が増えないなら、半減期を足し算（積分）すれば、放射線量の「累積量」がわかります。

その計算に必要なデータは文部科学省が サイトマップ：文部科学省 で公開しています。風は北西方向に吹くことが多く、北西方向に多く放射性物質が飛んでしまったので、北西方向の以下の3地点を選びました。全て、30kmエリアの外です。自主避難などが出ていないOKとされている場所です。

場所	距離	計測地点番号
浪江町津島	30km	32
飯舘村	40km	62
福島市	60km	1

文部科学省が計測しているのは、役場や小学校があるなど、それぞれの集落の中心部です。今問題になっているのが「飯舘村」です。「浪江町津島」は自主避難してしまったのか、多くの人が残っているのか僕はよくわかりません。

結論

先に結論を書いてしまうと、以下の通りです。mSvはミリシーベルトです。

場所	距離	15日から積分	17日から積分	判定
浪江町津島	30km	39.4mSv	30.4mSv	たぶんアウト
飯舘村	40km	8.3mSv	6.5mSv	たぶんギリギリセーフ
福島市	60km	2.1mSv	1.7mSv	たぶんセーフ

計算方法

まず、文部科学省が発表している元データです。15日から飛散しているのですが、多くの地点で計測を始めたのは17日からなので、17日からのデータです。単位はマイクロシーベルト／時です。1000マイクロ＝1ミリです。

日付	経過日数	浪江町津島	飯舘村	福島市
3月17日	0	170		7
3月18日	1	150	30	8.5
3月19日	2	136	26.5	7.2
3月20日	3	110	25.8	5
3月21日	4	90	20.4	5
3月22日	5	75	15.3	3.5
3月23日	6	75	16.8	4
3月24日	7	65	13.2	3.6
3月25日	8	65	12.3
3月26日	9	46	10.2	2.5
3月27日	10	50	11.2	3.5

飯舘村の3/17のデータはおかしかったので空欄にしました。3/18のデータも30以上となっていますが、30としました。

これをグラフにプロットすると以下のようになります。半減期は指数関数で表現できるので、Excelの近似曲線は「指数近似」です。浪江町津島や飯舘村はかなり綺麗に近似曲線にフィットします。福島市は少し不正確です。

この近似曲線を積分すると、累積量がわかるのですが、3月15日は経過日数「-2」なので、「-2〜無限大」で積分すると累積量がわかります。ただし、3/15や3/16のデータがない部分をこのように予測値で埋めて良いのかどうかは、若干、不確実です。しかし、それにより、判定結果が変わるわけではないので、この手法を採用しても大丈夫だと思います。「結論」の「15日から積分」が「-2〜無限大」で「17日から積分」が「0〜無限大」です。

積分計算は WolframAlphaを使いました。計算結果のリンクは以下の通り。浪江町津島の分だけ、キャプチャ画像を張ります。

• http://www.wolframalpha.com/input/?i=%28integrate+164.5exp%28-0.13x%29+dx+from+-2+to+infinity%29+24
• http://www.wolframalpha.com/input/?i=%28integrate+33.596exp%28-0.124x%29+dx+from+-2+to+infinity%29+24
• http://www.wolframalpha.com/input/?i=%28integrate+7.6315exp%28-0.1054x%29+dx+from+-2+to+infinity%29+24

専門家へのお願い

原子力が専門家の方は、もっともっと、ブログなどでインターネットで、現状どうなっているか解説記事を書いていただけるとすごく嬉しいです！正確な情報が広まれば広まるほど、非科学的な行動をする人・デマに流される人・政府や電力会社のおかしな行動は相対的に減ります！

そして、一日8時間以上インターネットを使っている（笑）、インターネット業界の人は、難しめの専門的な記事は、クチコミで広がりにくいので、専門家による良質な記事を見つけられた際は、Twitter や はてなブックマーク などで、少しでも「拡散」するように、ぜひぜひ、ご協力をお願いします！

疑問点（半減期）

http://ja.wikipedia.org/wiki/%E5%8D%8A%E6%B8%9B%E6%9C%9F に半減期の計算方法があり、上記の近似式を使うと、半減期は以下の通りになります。

場所	半減期
浪江町津島	5.3日
飯舘村	5.6日
福島市	6.6日

5〜7日とヨウ素131の半減期の8日よりも少し短いです。原発に近いほど減るペースが速く「風で再拡散しているのでは？」という説を教えてもらったのですが、そういう物なのでしょうか？

ツイートする

■JavaScriptでソフトウェアの正しさを数学的厳密に証明してみた

現在、Shibuya.js が開催中です！Ustream で http://www.ustream.tv/channel/shibuyajs にて放送されています。これから、このブログの内容をしゃべります！

今回「テスト」がテーマなうえ、Shibuya.js は「役に立つ話担当」「ネタ担当」に分かれていて、僕は「ネタ担当」なんですが（笑）、いつも通りネタです。でも、遠い未来の役立つネタです！

きっかけは、id:t-wada さんに、GUIの自動テスト関係の質問をしたら、凄くいいことを教えてもらいました。

全てのテストはサンプリングテストである

（少し表現違ったらごめんなさい）話の流れで、部屋を移動しなくていけなくて、たしか、それしか話ができなかったのですが、要するに、サンプリングテストである以上、全ての入力パターンをテストすることは不可能であり、できることは、限られたコストの中で、効率よくテストする必要がある、という意味だと思います。だから、手動テスト vs 自動テスト、どっちが良いのかは、その文脈での効率性で決まるという、趣旨の発言だったと、僕は理解しました。（ちょっとしか会話できなかったので、ほとんど推測です。t-wada さんの意図は、全然違ったりして…）

この名言は、本当に凄くいい名言だと思うんですが、Shibuya.js の「ネタ担当」としては、あれ？全て？と引っかかりました (^^♪ 「例外のない規則はない」ということわざもありますしね！この、ことわざは自己矛盾しているんですが…（笑）

自動証明

というわけで、プログラムが与えられて、そのプログラムのテストプログラムが与えられて、数学的にその正しさを式変形を繰り返して、正しさを証明するプログラムを作りました！

ターゲットは、一番やりやすそうな「挿入ソート」を選びました。（申し訳ないですが、挿入ソートとは何かは、検索してください。手抜きごめんなさい）

プログラムは以下の通りです。

function sortInner(ary) {
  if (ary.length < 2) {
    return ary;
  } else {
    if (head(ary) < head(tail(ary))) {
      return ary;
    } else {
      return append(head(tail(ary)), sortInner(tail(swap(ary)));
    }
  }
}

挿入ソートは2重ループなのですが、ループの内側の部分だけです。つまり、ary[1] 以降はソート済みで、ary[0] を適切な位置まで挿入する部分をターゲットにしました。

head(ary) = ary[0]、tail(ary) = ary.slice(1)、swap(ary) は ary[0] と ary[1] を入れ替えを非破壊で（新しい配列を生成して）行います。

ソートの正しさの判定

正しくソートされていることを証明するには、以下の2つを証明する必要があります。

1. ary[i] < ary[i + 1]
2. 「ソート前」「ソート後」で要素が1対1対応すること

扱う問題を小さくするために、今回は、１の方だけを扱います。

というわけで、判定プログラムは以下の通りです。（isOrdered の方が正確な名前かもしれません）

function isSorted(ary) {
  if (ary.length < 2) { 
    return true; 
  } else {
    return head(ary) < head(tail(ary)) && isSorted(tail(ary));
  }
}

証明すること

証明することは、isSorted(sortInner(ARY)) = true です。前提条件として、isSorted(tail(ARY)) = true が成立します。加えて、数学的帰納法を使い証明するので（まだ、この部分は自動化できませんでした）isSorted(sortInner(tail(ARY))) = true を条件に加えます。

証明時に、変数と定数を区別しているのですが、数学的帰納法において、配列の長さは制限が加えられていて、任意の配列というわけではないので、対象の配列を定数化し、ARY で表現しました。

プログラムの表現方法

Haskell のような純粋関数型言語は難しすぎて、人間には書きづらいと思うのですが、自動証明においては、凄く扱いやすく、採用しました。関数は全て副作用がありません。つまり、配列操作は、絶対に配列を破壊しません。なので、sortInner は以下の形になります。

sortInner(ary) = 
  if(lt(len(ary), 2),
    ary,
    if (lt(head(ary), head(tail(ary)),
      ary,
      append(head(tail(ary)),
        sortInner(tail(swap(ary))))))

DOM & XPath

これをひたすら式変形します。上記の通り、関数は木構造になっているので、パターンマッチングでひたすら木構造の変形になります。

木構造をどう扱うか悩んだんですが、最初、正規表現を使おうかと思ったんですが、Perl の正規表現とは違って JavaScript の正規表現は再帰が扱えないので、木構造が扱いづらく、JavaScript (HTML) は DOM が使えて、木構造のための API があるので、関数を DOM に押し込みました！その上で、式変形のパターンマッチングを XPath を使って検索するようにしました。Firebug などを使うと、木構造の変形を追いやすく、便利でした！

定義＆公理

そのほか、使う定義や公理は以下の通り。

head(tail(swap(ary))) = head(ary)
tail(tail(swap(ary))) = tail(tail(ary))
tail(append(ary, v)) = ary
head(append(ary, v)) = v
if(true, a, b) = a
if(false, a, b) = b
if(a, b, b) = b
a && true = a
true && a = a

ちょっとズルなんですが、定義のような定理。

len(append(ary, v)) < 2 = false

連結すると、長さが2以上になるよと言う件です。len と append の関係性を手抜きしました。

上手く扱えなかった数学的帰納法

昨日・今日でこの準備をしていて、発表までに間に合わなかった、数学的帰納法の取り扱いです。以下の2つは単独で証明できると思うのですが、うまく、自動証明の流れの中で証明できなかったので、定理に加えてしまいました。ごめんなさい。次の課題として、これをちゃんと自動証明できるようにしたいです！

1. head(tail(ARY)) < head(tail(tail(ARY)))
2. isSorted(sortInner(head(swap(ARY)))) = true

最初の方は、tail(ARY) はソート済みだから tail(ARY)[0] < tail(ARY)[1] という事です。

次の方は、head(swap(ARY)) は長さ n – 1 だから、数学的帰納法により証明済み という事です。

if 条件の伝搬

さらに、特殊な式変形が2つ必要です。一つ目は、if (A) { B } else { C } において、B の中で A = true であることを使うことが必須です。これが、「if 条件の伝搬」。

if (A, B, C) で

• Bの中でAを使っていたら、A = true
• Cの中でAを使っていたら、A = false

否定形も必要でした

• Bの中でnot Aを使っていたら、not A = false
• Cの中でnot Aを使っていたら、not A = true

if の親関数の繰り込み

2つ目は、if の親関数の繰り込みです。 f(A ? B : C) = A ? f(B) : f(C) です。fの引数の数が任意でも扱えると言うことを上手く表現する方法が思いつかなかったので、別枠でコードを書きました。

証明戦略

式変形において、次の一手は、たくさんあり、指数関数的に増えると思ったのですが、なんと、式変形に優先順位をつけたら、一直線で証明できました。

1. ノード数が減る変形 や if 条件の伝搬。
2. if の親関数の繰り込み
3. ノード数が増える変形（定義の代入）

ノード数が減る方を優先して、それをやることがなくなったら、ノードを数を増える変形をやってみて、さらに、また、ノード数を減らす変形を繰り返して、というので、できました。でも、これは、今回の特例で、おそらく、次にどういう手を繰り出すかは上手い評価関数を作って、証明が分岐していくパターンは絶対に必要だと思います。

if の親関数の繰り込み は少しだけ、木構造が複雑になる方の変形です。

デモ

というわけで、デモです。http://yukoba.jp/autotest/sort.html をごらんください。出力は、console.log() に出ます。Internet Explorer 8は未対応です（XPath の扱いが違います）。細かいアルゴリズムは http://yukoba.jp/autotest/js/sort.js をご覧ください。

というわけで、console.log() をみるとわかるのですが、なんと38回の式変形で証明できちゃうんです！

ログの出力は、「証明すべき対象の式」「使える変形式」を出力した後、そこから先は、式変形ごとに、「どの式を使って変形したか」「証明すべき対象の式の変化した結果」を繰り返し表示しています。

使用したスライド

ツイートする

■ARM vs Intelの未来の展望

ARMはスマートフォン・携帯電話で広く使われていますが、クロック周波数の割に微妙にIntelのCPUよりも遅く、なんでなのかなーということで調べてみました。

まず、CoreMark an EEMBC Benchmark のベンチマークの結果から、色々数字があり、すごく悩みながら信用できそうな数字を拾ってみました。

1コア当たりの性能

名称	性能	備考
ARM Cortex-A8 600Mhz	2.035/MHz	Cortex-A8は2010年のスマートフォンの主流
NVIDIA Tegra 250 1GHz	2.646/MHz	Cortex-A9は2011年のスマートフォンの主流かな？
Intel Core2 Duo 1596MHz	3.205/MHz
Intel Core i5-650 3200MHz	3.244/MHz

このように、クロック当たりの性能がIntelよりも悪いです。消費電力を増やさないためだと思います。この数字が正しいとすると、今のスマートフォンの1GHzというのは、600MHzな感じです。（JavaScriptのベンチマークだと、さらに25%程度遅いイメージがあります）

今のスマートフォンの主流は Cortex-A8 ですが、これから、Cortex-A9 に移行する状態です。NVIDIA Tegra 250 は Cortex-A9 のデュアルコアで、フルハイビジョン (1080p) を再生できます。（まぁ、再生能力は、GPUの力が大きいですが…）

そして、ARMの公称値では Cortex-A8 2.0 DMIPS/MHz、Cortex-A9 2.5 DMIPS/MHz なので、CoreMark は DMIPS と数字を合わせているみたいですね。DMIPS は整数演算がどれくらい実行できるかという指標です。2.0 DMIPS/MHz というのは、1クロックあたり2回計算ができるという意味です。

2010年をにらんだARMの戦略と新CPUコア によると、Cortex-A8, Cortex-A9 は演算論理装置(ALU)が2つです。A8の 2.0 DMIPS/MHz は理屈通りですが、A9 の 25% 増しは、アウト・オブ・オーダー実行を搭載していて、命令を出てきた順番ではなく、高速に実行できるように順番を入れ替えて実行しているので、それによる効果かなと僕は思っているのですが、あんまり自信なし…。

【レポート】ARM、次世代プロセッサコア「Cortex-A15」に関する説明会を開催 | エンタープライズ | マイナビニュース によると、Cortex-A9 の次の Cortex-A15 は2013年くらいに主流になるみたいです。ALUが3つになっています。ということは、3 DMIPS/MHz 以上なるのではないかとおもいます。

ASCII.jp：詳細解説　これがSandy Bridgeのアーキテクチャーだ｜Sandy Bridgeこと新Core iシリーズが登場 によると、Sandy Bridge は ALU が3つです。かなり昔から、IntelのCPUはALUが3つみたいです。だから、Cortex-A15 と Intel のクロック当たりの動作速度が大体同じになる気がします。

ARMのクロック当たりの動作速度は、たぶん、Cortex-A15 で Intel と同じになり一回伸び悩むようになり、クロック周波数を上げるのもチンタラになると思いますし、コア数を増やす方向に行くんでしょうねぇ。まぁ、少なくとも、Cortex-A15 が主流になる時代までは、スマートフォンはどんどん順調に速くなっていく気がします。

数年後のスマートフォンの使われ方

2011 International CES：次期版WindowsはARMアーキテクチャをサポート - ITmedia エンタープライズ にあるように、Windows 8 や Office を ARM 対応させることを正式に発表しています。リリース時期から考えて、Cortex-A9 + メモリ1GB を最低ラインにして出荷すると思うのですが、たぶん、パフォーマンス的に問題ない気がします。2012年ならちょっと心配ですが、2013年 (Cortex-A15) なら全く問題ないと思います。

Windows の特徴として、「大きなディスプレイが必要」というアプリが中心です。大きなディスプレイというのは 1024x768 以上の事ね。純粋にスマートフォン内蔵のディスプレイで Windows や Office を使うのは非現実的ですが、スマートフォンから HDMI や無線などでディスプレイにつなぐ使い方が主流だと思います。そして、Bluetooth でキーボードやマウスとつなぎます。そういう使い方であれば、ノートパソコンがさらにダウンサイジングしただけで、一般ユーザーから見たら大差ないと思います。10インチ以上の「モバイル用ディスプレイ」というのも出回るかもしれません。

そして、スマートフォンの小さな画面用には、それ用のアプリが必要なので、今まで通り Android が使われると思います。そうすると、Android と Windows のデュアルブートになります。たぶん、端末の横にスイッチみたいのがついて、ハイバネーションして Android <-> Windows を行ったり来たりできる端末になる気がします。

数年後の話ですが、結構、この予想自信があるのですが、あたるかな〜？！

ツイートする

■JavaScriptでVM作って「30日でできる！OS自作入門」をやってみた (2日目)

カーネル／VM Advent Calendar の40日目です。ごめんなさい1日遅れ。他の方のも面白いですよ！左のリンクからどうぞ。

私、JavaScriptでVM(仮装機械)を色々作ってきましたが、いつも、言語処理系のVMばかりで、VMwareのような、マシン自体のVMはやったことがなかったので、トライしてみました。

選んだテーマは、川合秀実さんの5年前の名著、「30日でできる! OS自作入門」。これ、凄くいい本ですね！読んでみてびっくりしました。かなりお勧めです。英訳は出ていないと思いますが、英訳を出すに値する本だと思います。でも、川合さんのOSASKは終了（中断？）しちゃっているみたいですね。

どうやって、VMを作るか、何時間も悩みました。OS自作入門では、NASKという川合さん自作のアセンブラとC言語で書かれています。C言語で書かれたのも一度NASKのアセンブラに変換されて、最終的にバイト列に変換されるので、NASKをターゲットにすることにしました。というわけで、やることは、CPUとBIOSの作成です。

インタープリタ方式にするか、コンパイラ方式にするかも悩んだのですが、とりあえず、コンパイラ方式にしました。NASK は LIST ファイルという、左側にバイト列があって、右側にニーモニックが出る、扱いやすい出力を作ってくれます。これを、Groovyで x86 -> JavaScript のコンパイラを作り、JavaScript に変換することにしました。本当はコンパイラを JavaScript で書きたかったのですが、ごめんなさい、手抜きです。

やってみて思ったのですが、x86 のバイト列は、命令列とデータ列が混在になっていて、コンパイルがやっかいです。NASK のアセンブラなら、データ列の部分は DB などのデータ列を表現するニーモニックを使っているので、データ列を避けてコンパイルすることができます。今回はそれに逃げています。本当にコンパイルしようと思ったら、JavaScript でJITコンパイラを作り、x86 -> JavaScript のソースコードに変換して、それを eval() で読み込むロジックが必要そうです。データとプログラムが混在するバイト列の中で、実行しようとした番地はプログラムの始まりなので、そこからJITコンパイルしていけば良さそうです。ただし、プログラムの終わりがわからないので、適当なところで中断して、そこから先も実行しようとしたら、再度コンパイルすると言う処理が必要そうです。また、プログラムの自己書き換えとかがあると、やっかいかも。

OS自作入門は、1日目はビルド方法などなので、2日目から挑戦しました。2日目は、print "\n\nhello, world\n" を実行するだけのOSです。ちなみに、3日目から32ビットモードになり、VRAMの操作が必要で、ハードルがぐんと上がります。いつか機会があったら、3日目も挑戦したいです。

あと、もう一つ愚痴。x86 って命令数がなんか多いですね！Intel® 64 and IA-32 Architectures Software Developer Manuals に命令セットのマニュアルがあり、なんか、わかりにくく、x86 -> JavaScript の変換はだいぶ想像で作ってしまいました。（追記：日本語技術資料のダウンロード に日本語マニュアルがあるんですね）

と言うわけで、作ったファイルやデモの一覧。

• helloos.nas - これが、元のアセンブラです。川合さんのコメントが大量に入っていてわかりやすいです。一文字ずつ読み込んで、INT 0x10 を使ってビデオBIOSを呼び出します。末尾に、RESB 1469432 という命令が入っていて、これは、サイズを1.4MBのフロッピーのサイズに揃えるために入っているのですが、これがあると次のLISTファイルの生成でエラーになるのでコメントアウトしました。
• helloos.lst - 付属の asm.bat を書き換え、nask.exe helloos.nas helloos.img helloos.lst で生成できます。左側に番地やバイト列がつきます。
• Compiler.groovy - これが、lst -> JavaScript のコンパイラです。前半の方で lst を読み込んで、後半の方で JavaScript を生成しています。170行程度ですし、たぶん、簡単に読めると思います。実行すると、helloos.js を生成します。
• videoBios.js - ビデオBIOSの部分です。id が stdOut のいうDIVタグに innerHTML で追加しています。
• helloos.js - これが、コンパイル結果です。素直にコンパイルしています。末尾に、全てのバイト列を含めていて、これを、一文字ずつ print する時に読み込んでいます。

以上により作られるデモがこれです〜！ちゃんと表示された！

helloos.html

ツイートする

■[JavaScript]WebSoocketではなくTCPSocketが欲しい！

現在、WebSocket は既存のHTTPプロキシを通した際にセキュリティ上の問題があるという理由で、Firefox 4 beta と Opera 11 で無効になっています。Chrome や Safari も悪意のある攻撃が始まったら無効にすると言っています。

そして、どのようなプロトコルにするかを IETF のメーリングリストであーだーこーだ議論されています。→ hybi Discussion Archive - Date Index

つまみ食いで読んだだけですが、話し合いは全然まとまっていないみたいです。TLSは重いからXORがいいとか、クッキーが使えるように普通のHTTPヘッダを使いたいとか、なんか色々です。（つまみ食いなので間違っていたらごめんなさい）

そもそも、既存のHTTPプロキシを通すSocketを作るというところにだいぶ無理があります。Skypeがルーター越えをするというのと同レベルの話じゃないでしょうか。バッドノウハウ過ぎて、IETFやW3Cでやるレベルのことなのだろうか？

複雑すぎる物を作ると大人数の話し合いではまとまらないというのは ECMAScript4 の反省ですが、同じ過ちを WebSocket で繰り返している気がします。

Flash には Socket クラスがあり、生の TCP が使えます。HTML5 でも TCPSocket を作って、生のTCPを使えるようにして、どうやって HTTP プロキシを通すかは、JavaScript のライブラリで解決すれば良い問題じゃないのでしょうか？

僕は、JavaScript は21世紀のC言語だと思っているのですが、仕様として用意すべき物はC言語同様、プリミティブな物にすべきだと思います。

TCPSocket と UDPSocket 作って！

（追記）ちなみに、ActionScriptでは似た話はas3corelibに入っているRFC2817Socketです。解説はここ→A Proxy-savvy Socket in ActionScript 3 « Christian Cantrell。

ツイートする