思いつきメモ

思い立って、HaskellとOCamlそれぞれでWebアプリを開発するにあたって、どれくらいの性能が出る ものなのか、まずはベンチマークをとってみることにした。フレームワークとして、Haskellに ついてはSpock, OCamlについてはOpium を選んだ。

Spockは、GHC7.6.3とcabal-installを使用してビルドした。Spockは0.10.0.1を使用した。 まずは、src/Main.hsを示す(ほぼGitHubにあるもののまま)。

{-# LANGUAGE OverloadedStrings #-}
import Web.Spock

import qualified Data.Text as T

main =
  runSpock 7777 $ spockT id $
    do get ("echo" <//> var) $ \something ->
        text $ T.concat ["Echo ...

自分も参照できるようにブックマークをまとめます。随時更新。

Haskell関連

• Understanding F-Algebras
  • カタモルフィズムについて分かりやすい
• Morte: an intermediate language for super-optimizing functional programs
  • CoCで正規化。Literatureのリンクが有益。
• Total Functional Programming
  • 構造的帰納法とCovariantな高階函数に制限して⊥の無い型にすれば停止性が保証できるよね、という文献。Codataはこれから読む。
• What I Wish I Knew When Learning Haskell
  • Haskellのマニアックな部分も説明している
• Auto as Category, Applicative & Arrow (Intro to Machines/Arrows Part 2)
• A Modern Architecture for FP
  • Freeモナドの使い方が比較的分かりやすく記述されている。
• Free ...

型理論で良く出てくるのが、依存型である。これは、ある型が別の型に依存して いたり、ある型の値に依存して決まったりできるような型のこと。

これにはdependent sum(Σ)というのとdependent product(Π)というのがある。 何となく説明を読んだりして分かった気になるのだけれど、人に説明できる ほどではないような気がするので、Programming in Martin-Löf's Type Theory を元に勉強してまとめる。

CoqとかAgdaを使えるようになるには、このあたりの最低限の理解が必要だと思う。

2章の導入をまず読んでみる。

大切な考え方は、命題を集合と同一視するということ。普通の数学でするように、命題は 必ず真か偽かどちらか一方である、という考え方ではなく、命題が真であるのは、それを証明できるとき だけである、とする考え方に基づいている。

A∨¬Aという命題は、Aが真か偽かのどちらかなので、いずれにせよ真である、と考えることも出来る。 一方、論理和の一方が証明できたときに、上記命題が真である、とする立場もある。 これが型理論が元とする考え方となる。

この考え方を進めて、

A⊃Bの証明とは、Aの証明を与えたときに ...

自分用のメモ。Haskellにてmutable vectorを使う方法。STモナドの中であれば変更できる。STモナドは PrimMonad ST, PrimState STとなっている。実装はここ. DctQuantという名前なのにDCTしか実装していない。ijgjpegのfloatバージョンを元にして変更。あまり確認していないので、計算に間違いがあるかも。

前回、Vivado HLSにていろいろと問題に遭遇していることを書いたが、 いくらか前進できた。

まず、Co-simulationとC simulationの結果が一致しないという問題。大体以下のような形のコードになっていた。topが合成したい関数のトップレベル。

static int A[] = {...};
static int B[] = {...};

int g(int* array){
    ....
    use array element
    ....
}

void f(int* array){
     ....
     g(array);
     ....
}

void top(){
     ....
     f(A);
     f(A);
     f(B);
     f(B);
     ....
}

これを、次のように書き換えた。

static int A[] = {...};
static int B[] = {...};

int g(int* array ...

現在Vivado HLSを使用して回路合成の実験をしているが、いろいろと問題に遭遇している。

• バージョン2014.2で合成するとCo-simulationが終了しない。
• バージョン2014.4で合成するとCo-simulationは終了するが、C simulationと結果が一致しない。

ひょっとしたら合成側ではなく、シミュレータ側に問題があるかと予想し、 2014.2で合成した結果を2014.4のシミュレータで動かしてみたが、終了しないのは 変わらなかった。

また、2014.2で合成した結果をインプリしてみたが、AXI Stream出力なのに、 TREADYがHighになっていないにも関わらず、TVALIDがHighでTDATAが変化してしまっていたりする 状況が見られた(FIFO fullなのに書き込み側が止まらずに進んでしまっているような状況)。 これは明らかにハンドシェークとしておかしい。

今はC++から合成しているが、自分の意図としては「ここは並列して動いて欲しい」 というところがツールにちゃんと伝わらないことが多いのも不満がある。 RTLでの記述は並列に動作するのが前提だが、Cのような言語は逐次実行が前提なので、 どこまで並列化できるかは、ツールの賢さに完全に依存してしまう。

細かいところでは、配列はBlock RAMとして実装されることがあるが、 その場合自動的に変数は複製してくれないので、Block RAMの2ポート制約の せいで並列性が犠牲になることがある。自動的に同一のBlock RAMを複数 コピーするようにしてくれれば嬉しい(あるいは複製数を指定できるとか)。 仕方ないので ...

今年コンピュータ関連でやったことの一部を振り返ってみた。

• Zynqまわり
  • VivadoでAXI Master/Slave IP作成
  • Vivado HLSの実戦投入
    • これは一度使ってしまうと、手RTLでパイプラインを作成するのが億劫になってしまうという効果があった。ただし、データパスの生成はあまり賢くない(というか思い通りになかなか生成されない)ので、hls::streamでモジュールを分離して合成するなどした方が良さそうに思われた。
  • Yocto Linux
    • これまた便利極まりない。一々コマンドを入力してLinuxの環境を作るとなると、どうしても手順書をしっかり残さないと再現性が無くなってしまうが、Yoctoではレシピの形で手順が残っているので、再現性が基本的に高い。
  • IPからDMAするためのドライバ作成
    • dma_alloc_coherentではなく、kmallocとか__get_free_pagesで確保するようにした。これをuser spaceにmmapできるようにもした。少なくとも4MBまでは確保できることを確認した。また、DMAするためには、確保したバッファに対して、dma_map_single, dma_unmap_singleなどを呼び出せばOK。
• Linuxの動くSoCをZynq以外で二つほど使ってみた
• libsvmで画像認識の実験
  • あまり精度が出ないように感じた。このあたりのチューニングはあまり突っ込まなかった。
  • DNでは、特徴量の抽出も自動的に行えるというのがウリとよく言われるが、適応領域によって適切なネットワーク構造が変わってくるとしたら、結局そのあたりのチューニングが必要なのでは? このあたりは要調査。

全体としてはZynqをいろいろいじってみた、という印象か。 最近勉強する気力が衰えていると感じる。どちらかというと実践よりの 新しい知識は少しだけ増えた気がする。

これまでBloggerを使用していたけれど、ずっとWebベースのUIがいまいち 好きになれなかった。また、カスタマイズも結構面倒だった。

色々調査した結果、GitHub Pagesが 便利そうだ、ということが分かったので、なんとか色々駆使することで Bloggerのデータを移行できたと思う。

最初は静的サイトの生成にhakyllを使おうと したけれど、なかなかカスタマイズが面倒になってしまった。実はこれだけでも 暇なときに2,3週格闘していた。

結局Pelicanを使用することで、最低限の 状態にはなったと思う。また、GitHub Pagesの場合、gh-pagesというブランチに コミットしなければいけない、というルールがあるので、そのために ghp-importを使用した。 これで少しはまったのは、ghp-import outputとすると、とくに何もコンソールには 表示されずにコミットまでされてしまうので、それに気付かずに何回も コミットしてしまったこと。基本的にはghp-import -m 'message' -p outputのように 使用するのが良さそうだ。

これでMarkdownも使えるようになった。コードのハイライトなども楽に書けて嬉しい。

引き続き、SDカードからのLinuxブートを試してみた。

Digilentのu-bootのxilinx-v2013.4をチェックアウトしたものでは、ZYBOのu-bootはSD起動にジャンパ設定されていると、SDカード内にuImage, devicetree.dtb, uramdisk.image.gzというファイルを探して、それをメモリに展開、Linuxをブートしてくれるようになっている(printenvで確認可能)。

したがって、BOOT.binにはカーネルやramdisk, devicetreeは必要ではなくて、FSBLと(必要であれば)FPGAのbitstream, u-bootだけが入っていればよい。BOOT.binの作り方については、基本的にこちらに記載されている方法に従えばよい。

以上でSDカードからのブートが出来るようになった。

Zynq上でPLにロジックを自作してDMA処理を行う場合、アプリケーションからレジスタを操作するために最も手軽 なのは、以前書いたとおり UIOを使用することだと思う。

このような場合、ロジックで使用するメモリ領域はLinuxが使用する領域と完全に分けておいた方が (少なくとも自分のような初心者には)楽だ。このためには、実装されているメモリより少ない領域を 使用するようにLinuxを構成しないといけない。

今回は、ZYBOで512MB実装されているところを256MBだけLinuxに割り当てた。しかし、結構これにはまった。 やり方は、以前の通りXilinx純正gitをcloneしてxilinx-v2014.1をcheckout。zynq-zed.dtsを編集し、 ps-clk-frequencyを変更するまでは同じ。bootargsを

console=ttyPS0,115200 root=/dev/ram rw earlyprintk

となっているのを、

console=ttyPS0,115200 mem=256M root=/dev/ram rw earlyprintk

とする。また、ps7_ddr_0: memory@0をreg = <0x0 0x20000000="">;からreg ...