数学とプログラミングとくだらないこと

プログラミングの事とか数学のこととかを書いていきます。

S1ステートなるものを知った

PCがスリープできない。 実際はスリープができないのではなく、スリープすると起動しない。 しかも強制終了してみると、次回の起動時に起動しないし、強制終了してもまた同じ状態に！ リセットスイッチを押してみたら起動はしたので、まぁよしとしよう…。

さて、原因を調べてみたいが、どうにも一切検討がつかない。 とりあえず、スリープした状態を観察してみると、スリープしているはずなのに、ファンが回っている。 調べてみると、どうやらS1ステートというやつらしい。

S1ステートというのは、PCの電源管理の規格であるACPIで定められていて、 スリープの一種らしい。 PCの状態は、電源という側面から見たときに、S0からS5までの6種類が定められている。 S0は完全な起動状態であり、S5が電源断の状態。その間の状態は、数字が大きくなるほど、待機時の電力消費が少ないらしい。 逆に、数字が小さいほど、復帰までの時間が高速らしい。 S3が一般的なスリープ、S4がいわゆる「ハイバネーション」であり、S1はスタンバイと呼ばれる状態だそうだ。この状態ではファンなどは回り続けるらしい。

さて、PCをスリープしようとしてみると、ファンが回っている。電源ランプは点滅状態だから、スリープの状態ではあるはずである。 しかし起動しない。S1ステートであるという根拠はここなのだが、調べてみると、S1ステートには対応していないという。 これが復帰しないことの原因なのだろうか？ だとしたらなぜS1ステートに入るのか? 謎である…

MacにATSをインストールした

ATSという言語のコンパイラをインストールしたのでメモ。

なんでATSを選んだのか

常々型システムが強力なC言語が欲しいと思っていた。 ATSはC/C++並のパフォーマンスが出るらしい言語で、 依存型とか線形型とかが使えるらしい。 （線形型とは何かよく知らないが、多分線形論理に対応する何かだろうと思う。 リージョン推論に使うんじゃないかな？）

インストール

基本的にはJATS-UGの記事に従って ATS2-Postiats-0.0.8と ATS2-Postiats-contrib-0.0.8をインストールしたけども、Homebrewを使ってる関係で、ソースを/usr/local/srcに展開し、 /usr/local/Cellar/ATS2-Postiats/0.0.8以下にインストールした。

cd /usr/local/src
tar -xf ~/Downloads/ATS2-Postiats-0.0.8.tgz
tar -xf ~/Downloads/ATS2-Postiats-contrib-0.0.8.tgz

cd ATS2-Postiats-0.0.8
./configure --prefix=/usr/local/Cellar/ATS2-Postiats/0.0.8
make
make install

cd ..
cp -r ATS2-Postiats-contrib-0.0.8/contrib \
/usr/local/Cellar/ATS2-Postiats/0.0.8/lib

brew link

export PATSHOME=/usr/local/lib/ats2-postiats-0.0.8
export PATSHOMERELOC=$PATSHOME

今からやる事

とりあえず、JATS-UGに載ってる日本語訳の文章読んでみて、チュートリアルなどをやってみようと思う。

PNaClのサンプルを動かしてみたい

PNaClのチュートリアルのコード（のコメント）を読んだメモ。

PNaClとはなにか

NaCl(Google Native Client)というものがある。 これは、Web上の任意のコードを安全に実行するためのサンドボックス技術らしい。 サンドボックスとブラウザはPepperAPIというAPIを使って通信する。

ブラウザ使うからプラットフォームに依存しないという利点があるらしい。

PNaClは、CPUに依存しない(Portableな)NaClらしい。

PNaClの使い方

要件

動かすのには、Python(2.6か2.7)とMakeが必要らしい。 対応しているOSはWin/Mac/Linux

SDK

開発するのにNaCl SDKという物がいる。

ココ にダウンロードからインストールまでの仕方が書いてある。

まぁ、naclsdk updateするだけだけども。

どう使うのか

PNaClを使うには、中間コードの.pexeと、マニフェストファイルである.nmfが必要。 embedタグのsrcに*.nmfのURLを指定し、typeにapplication/x-pnaclを指定する。

.nmfのファイルは見たところJSONである。 このファイルは、.pexeの場所やオプションのコマンドとかを指定するらしい。

モジュール

PNaCl用のバイナリが読み込まれると、まずpp::CreateModuleが呼ばれる。 この関数は、ロード時に一度呼ばれるだけ。 このときにpp::Moduleクラスのオブジェクトへのポインタを返す。 とりあえず、コイツの事をモジュールと呼んでおこう。

実際には、モジュールはpp::Moduleを継承したクラスを実装することになる。

インスタンス

PNaClのマニフェストを埋め込むembedタグに行き当たる度に モジュールのCreateInstanceが呼ばれる。

CreateInstanceはPP_Instanceを引数にとってpp::Instanceへのポインタを返す。 このpp::Instanceを継承したクラスに、Javascriptと通信する部分を実装していく。 とりあえず、コイツをインスタンスと呼ぼう。

ブラウザとサンドボックス間の通信

インスタンスにはHandleMessageというメソッドを実装する。 このメソッドはブラウザでjavascriptのpostMessageが呼ばれたときに呼び出される。 javascriptから送信されたメッセージを受け取って処理するメソッドである。 このメソッドの引数がpp::Varオブジェクトへの参照なのだが、詳しくはドキュメントを見ろと書いてある。

ちなみにC++側からjavascript側にメッセージを送るのは、PostMessageというメソッドを使うらしい。

ブラウザとサンドボックスの間の通信では送受信が非同期であることに注意が居るらしい。 コメントには、内部の状態を変化させるような場合に注意が必要という旨のことが書いてあった。

おわり

とりあえず読めたのはココまで。少しずつこつこつやってこう。

共有ライブラリのグローバル変数は他のプロセスからでも参照できるのか？

共有オブジェクトファイルのグローバル変数へのアクセスってどうなってるんだろう？ という事で、実験してみました。

Macの共有ライブラリ

ココとか ココとか を読んだ。

Macでの共有ライブラリは.dylibという拡張子で作るらしい。 コンパイラには-dynamiclibというオプションを付けるようだ。

Linuxならどんなオプションが必要だったっけ？

コード

実験に使ったコード。

共有ライブラリ用のヘッダファイル(share.h)

実験では、このshare_int32の値を 親子2つの別のプロセスから書き換えます。

結果の確認のためにprint_share_int32という関数を作ってます。

/* share.h */
#ifndef SHARE_H
#define SHARE_H

#include <stdint.h>
#include <stdio.h>

extern int32_t share_int32;

void print_share_int32(void);

#endif

共有ライブラリのコード(share.c)

説明略

#include "share.h"

int32_t share_int32 = 0;

void print_share_int32(void)
{
    printf("share_int32: %d\n", share_int32);
}

ライブラリを利用する側のコード(main.c)

親プロセスと子プロセスから変数を書き換えてみるコード。

#include "share.h"

#include <unistd.h>
#include <sys/types.h>
#include <sys/wait.h>

#include <stdio.h>
#include <stdlib.h>

int main(int argc, char* argv[])
{
    // グローバル変数を読めるかの確認
    print_share_int32();

    // グローバル変数に書き込めるかの確認
    share_int32++;
    print_share_int32();

    // 子プロセスでの書き込みが親プロセスで反映されるかの確認
    pid_t pid = fork();

    if(pid == -1)
    {
        perror("fork");
        exit(1);
    }

    if(pid == 0)
    {
        share_int32++;
        printf("Child Process: ");
        print_share_int32();
        exit(0);
    }

    wait(NULL);
    printf("Parent Process: ");
    print_share_int32();
    return(0);
}

出力

$ clang -dynamiclib -o libshare.dylib share.c
$ clang -o main main.c -L./ -lshare
$ ./main
share_int32: 0
share_int32: 1
Child Process: share_int32: 2
Parent Process: share_int32: 1

考察

子プロセスでインクリメントすると、子プロセスではインクリメントされた値が確認出来るけど、 親プロセスではそうではない。 多分グローバル変数はプロセスごとに別の物なんだろう。

errnoとかが他のプロセスから書き換えられたら困るもんな…

きっと親子のプロセスでなく、兄弟のプロセスだったら、出力される値は同じになるはず。

この実験はいつかやろう（やらないパターン。）

ナンプレを解く

17日に研究室に配属されました。 10日に配属の発表があったとか聞いてない… （初日を知らずに昼ごろになって呼び出される羽目に…）

とりあえず、課題が出たのでやったのでその記録。

課題

いわゆる「ナンプレ」を解くプログラムを作ります。

方針

やったことは2つ。

  1. それぞれ空のマスについて、入る可能性のある数字をあげていき、一つしか可能性が無いマスに数字を埋める。
  2. 数字を埋められなくなったら、1つ空マスを選んで、入る可能性がある数字で埋めて1に戻る。

実際にコードを書いて試してみると、解けない問題があった。 原因は、2で埋めた数字が間違っていることがあるから。 カルノー図のサイクリックテーブルみたいなわけにはいかなかった… そこで、解くのに失敗したら、バックトラック（？）するように変更した。

コード

これ

まとめ

何度もバグに悩まされた。 ビットで集合表すなんてことをやってるから、バグが出た時に分かり難い。 条件を入れておく変数とビット集合を入れ違えるなんて間違いもした。

型チェックが無いってこんなに辛いことだったんだ…

Agda2をインストールする

カリー＝ハワード同型対応とか難しい事は分からんが、型と証明が一対一で対応するらしい。 型理論の枠組みの中でプログラミングを行おうとする言語には、証明が出来るものがある。 という事で、Agdaというプログラミング言語を習得しようとインストールしてみた。

ここに書いてあることの大体は[Agda Wiki][agda-wiki]という所に書いてある。 というかAgdaに必要な知識の大体はここに書いてある。(英語の読めない自分には辛いけど。)

自分の環境はMac(Homebrew導入済み)なので、これを前提に進めていく。（というか、Debian系ディストリビューションにはパッケージがあるらしい…）

Haskell-Platformのインストール

Homebrewを使ってhaskell-platformをインストールする。

brew install haskell-platform

これだけ。ghcも必要になるけど、自動でインストールされる。

Mavericksの人へ

ghcはgccを使う事を前提としているようで、Xcode5のコンパイラ、clagnで使うには、フラグなどを適切にセットする必要がある。 ここを読んで知ったが、ghc-clang-wrapperというものがあるのでインストールした。

Agdaのインストール

haskell-platformがインストールできていれば、cabalというのが使えるようになる。 パッケージのアンインストールが手動なのが難点だけども、依存性解決とかが楽なのはうれしい。

cabal updateでパッケージ一覧をアップデートして、cabal install Agdaでインストール。 (Agda-Executableというのもあるけれど、よくわからないからAgdaの方をインストールしてしまった…)

Emacsのインストール

Agdaでの証明支援機能を使うには、コマンドラインツールかEmacsを使うらしい。 という事でEmacsをインストールした。今回インストールしたのはHomebrewからインストールできるEmacs24。 brew install emacsするだけ。--japaneseフラッグを付けた方がいいかもしれない。

とりあえずインストールできたら、mkdir ~/.emacs.dして、この下にinit.elを書いておく。

agda-modeの設定

agda-mode setupする。これでEmacsからagdaが使えるようになるらしい。

Agdasのstandard libraryをインストール

[Agda Wiki][agda-wiki]のここからstandard libraryをインストールする。

.tar.gzファイルを解凍してどこか適当なところに置いておく。/usr/local/share/agdaとかがいいんじゃないだろうか。

次はEmacsの設定で、

M-x load-library RET agda2-mode RET M-x customize-group RET agda2 RET

として、Agda2 Include Dirsというオプションのツリーを開き、そこで置いておいたディレクトリの下にあるsrcのパスを挿入する。 STATUSのところをクリックして、Save for Future Sessionを選ぶ。

終わり

これでおわった(はず）。 基本ライブラリがロードできれば成功、できなければどうしようか？

[agda-wiki] http://wiki.portal.chalmers.se/agda/pmwiki.php "Agda Wiki"

今年やったこと・来年やること

年の瀬なので今年やるはずだった事と、出来たこと、次にやる事を書き出して見る。

今年やるはずだった事

  • Rubyを習得
  • Railsを習得
  • 集合・位相入門を読む
  • 数理論理学を読む
  • 数理統計学入門を読む
  • 確率・統計演習１、２をする
  • PRMLを読んで機械学習の基礎を習得する

今年できたこと

来年（2014年）にやらないといけないこと

まとめ

やるべき事が出来てなさすぎる。 まぁ計画的にやらない事が一番ダメだったんだろうな。 一日一ページでも…と思うんだけどできてないんだよなぁ…

来年はちゃんと計画をたてて実行していこうと思う。