osiire’s blog

ふしぎなそふとやさん

Alloy model of lock-free stack

alloy

唐突にlock-freeをAlloyで書いてみたくなったので書いた。

what is lock-free

kumagiさんの資料によると、lock-free stackはリンクリストみたいなもので、先頭へのポインタをCAS(Compare and Swap)で切り替えるらしい。
素直にAlloy化するとこうなる。

sig Data {}

// linked elements of stack.
sig StackElem {
  data:Data
, next:lone StackElem // edge dosen't have next element.
} {
  no next & this // prevent self pointing.
}

sig HeadPointer { // HeaderPointer indicates the first stack element
  point: disj StackElem
}

このスタックの先頭を書き換えるPush操作を定義しなければならないが、今回はこれをfという3項関係で表現してみた。
元のポインタから次の新しいポインタへ書き換えることを表現している。

sig Push {
  newData:Data
, f : HeadPointer -> HeadPointer //old pointer replaces to the new one.
} {
 one f
}
fact UniqPush {
  all x,y:Push | x.f = y.f <=> x = y
}

// the rule of push operation.
// Push Behavior
// HeaderPointer-(point)->StackElem2 -(next)-> StackElem1
//      push a data ↓
// HeaderPointer-(point)->StackElem3 -(next)-> StackElem2 -(next)-> StackElem1
pred pushOperation[w:Push, p, p':HeadPointer] { 
    w.f = p -> p'
    p'.point.data = w.newData
    p'.point.next = p.point  // new
    no p & p'
}

fact {
  // Push.f satisfy pushOperation rule.
  all w:Push | one p, p':HeadPointer | pushOperation[w,p, p'] 
  // no pointer without push operation.
  Push.f.univ + Push.f[univ] = HeadPointer
}

ここまででインスタンスを出してみる.

f:id:osiire:20160408022626p:plain

当然のことながらスタックは壊れる。. スクリーンショットの下の方にあるStackElem3を見ると、他の２つのポインタからnext参照されており、
これは同時に2方向にスタックが伸びたことを意味する。並行動作に対して制約を入れないといけない。

ここでCASの出番。CASを使えばポインタを書き換える操作を逐次的にできる。HeadPointer -> HeadPointerという2項関係を直線(連結、分岐なし、合流なし、循環なし）にすればよい。これが意外と難しくて、何も考えずに書くとhigher orderでskolem化できないとAlloyに怒られる。試行錯誤した結果、下記の条件で二項関係を直列化できた。

pred linear[f:set elem -> elem] {
   let xs = f.univ + f[univ] | {
      // linear(no branch and merge)
      all x:xs | lone f.x && lone f[x]
      // connected and two edges.
      let s = f.univ & f[univ] | one (f.univ - s) && one (f[univ] -s )
      // non cyclic
      no ^f & iden      
   }
}

この制約をCASとして導入する。

fact useCASforRewritePointer {
   linear[Push.f]
}

これで完璧。下記のようなインスタンスが得られる。

f:id:osiire:20160408233419p:plain

linearに手間取って最初の構造で力尽きた感じ。

ScalaでDBアクセスの抽象化の件

本記事は関数プログラミングAdventCalendar2015 4日目の記事です。予定を変更してDBアクセス抽象化の話をしたいと思います。

pab_techさんによる二つの記事やtayama0324さんの記事でDBアクセスに対する抽象化が取り上げられています。


ちょうど某プロジェクトでScala + Repositoryパターン的なものを利用しようとしていたので、参考にさせて頂きました。結論から言うと、うちの開発では「Minimal Cake Pattern」と呼ばれるものほぼそのままと、Readerモナドによるトランザクションの合成で手を打った感じです。ドワンゴさんのところ程本格的じゃないけど似たようなことをやろうとする人には参考になるかもしれませんので紹介します。
まずはRepositoryです。例えとして商品データ(Products)を扱うとします。クラスの関係は下図のようなイメージです。実際にはxxxServiceのtraitが沢山あってそれをmixinする事を想定しています。




/**
 * 複数のxxxServiceをmixinした時に名前空間を区切るために変数を導入する。
 */
trait ProductsSevice[Context] {
  val productsRepository : ProductsRepository[Context] // リポジトリの実体を束縛する変数
}
/**
 * データベースアクセス用のServiceの実体(scalikejdbc版)
 */
trait ProductsServiceDBImple extends ProductsService[scalikejdbc.DBSession] {
  @Override
  val productsRepository : ProductsRepository[scalikejdbc.DBSession] = ProductsRepositoryDBImple
}
/**
 * DBアクセスインターフェイス
 * ここに色々抽象的なデータ取得/更新関数を定義する。
 */
trait ProductsRepository[Context] {
  def readAll : Transaction.T[Context, Seq[Product]] // 全商品情報の読出し
}
/**
 * DBアクセスインターフェイスの実装.
 */
object ProductsRepositoryDBImple extends ProductsRepository[scalikejdbc.DBSession] {
  import scalikejdbc._
  def readAll : Transaction.T[DBSession, Seq[Product]] = {
    Transaction ({ implicit session:DBSession =>
      // ここに実装が入る. 例外も捉えてアプリケーションレベルの例外にするなども行う.
    })
  }
}

DBアクセスの結果をTransaction.Tという型で包んでいます。これがドワンゴさんではトランザクションモナドと呼んでいた機能の一部(合成する機能だけ)を担うもので、実体はDBアクセスの文脈を運ぶReaderモナドです。実装は下記のような感じです。

/**
 * DBトランザクションを表現する
 */
object Transaction {
  type T[Context, A] = scalaz.Reader[Context, A] // scalazのReaderモナドの名前を付け替えただけ。

  def apply[Context, A](run : Context => A): T[Context, A] = {
    scalaz.Reader(run)
  }
  /**
   * DBアクセス用実行関数.
   */
  def runDB[A](t:T[scalikejdbc.DBSession, A]) : A = {
    import scalikejdbc._
    DB localTx { implicit session =>
      t.run(session)
    }
  }
  /**
   * ユニットテスト用実行関数(文脈無し)
   */
  def runDummy[A](t:T[Unit, A]) : A = {
    t.run(Unit)
  }
}

これらの下準備をしたら、利用する側では下記のようなコードを書きます。ポイントはRepositoryServiceトレイトでContextを存在型にしてrunTransactionの実装を要求しているところです。これでRepositoryServiceを使う側でrunTransactionを実行できます。

/**
 * 全てのサービスをまとめたもの
 */
trait AllService[Context] 
  extends ProductsService[Context]  // 商品サービス
  with SalesService[Context]    // 売上サービス
  with xxxService[Context] ... // その他種々のサービスをまとめる

/**
 * Transaction実行を含むRepositoryService
 */
trait RepositoryService {
  type Context                         // Context型パラメーターを存在型にする。これでrunTransactionメソッドを実装できるようにする。
  val repos : AllService[Context]
  def runTransaction[A](transaction:Transaction.T[Context, A]) : Try[A] // 隠した型パラメーターに対応するトランザクションの実行メソッド
}
/**
 * RepositoryServiceのDBアクセス実装版
 */
object RepositoryServiceDBImple extends RepositoryService {
  override type Context = scalikejdbc.DBSession
  override val repos = new AllService[scalikejdbc.DBSession]
                          with ProductsServiceDBImple
                          with SalesServiceDBImple
                          with xxxServiceDBImple

  @Override
  def runTransaction[A](t:Transaction.T[Context, A]) : Try[A] = {
    Try(Transaction.runDB(t))
  }
}

// ロジックを書くときにはRepositoryServiceを使う
class ApplicationLogic(service:RepositoryService){
  /**
   * お客が品物を買う動作を表現する
   */
  def buy(Customer customer, goods:Seq[(Product, Integer)]) : Try[Sales] = {
    // 複数のDBアクセスをトランザクションとして扱う。
    service.runTransaction(for(
       number <- service.repos.salesService.add(customer, goods) // 売上を保存して伝票番号を得る
         _ <- Traverse[List].sequence( goods.map( (p,n) => service.repos.stockService.sub(p, n, number) )) // 在庫の減算
    ) yield ( Sales(number, customer, goods ) ))
  }
}

// 
// new ApplicationLogic(RepositoryServiceDBImple).buy(...)
//

DBアクセス中に例外発生したらReaderモナド台無しじゃんというご指摘はごもっともですが、トランザクションがロールバックするので勘弁してもらう感じです。runTransactionで発生した例外の種類でエラーを拾います。

■

以前祖父の古銭コレクションを整理した記事を書いた。これが両親に好評で、息子共々にわか古銭コレクターとの認識を得た。その関係で、母が友人の親の遺産整理で大量の古銭を譲り受けてくれたとの事で、今日実家から荷物が届いた。


とりあえず分類のためにビニールに詰めなおされた古銭たち。同じやつを集めるだけで1時間以上はかかった。お昼ご飯を食べた後、早速息子と一緒に中身の解読を行った。なお、以下紹介する硬貨はhttp://ja.wikipedia.org/wiki/%E8%87%A8%E6%99%82%E8%A3%9C%E5%8A%A9%E8%B2%A8%E5%B9%A3にほぼ解説がある。

まず最初は小さくてあまり綺麗でない一銭硬貨↓。菊のご紋に大日本の文字。昭和19年から使われた硬貨らしく、当時の物資のない状況が伺える。

次は大量の10銭硬貨↓。十銭錫貨というものらしく、戦時中にアルミニウム不足のために錫と亜鉛の合金で作った硬貨だそう。

　十銭錫貨　http://homepage3.nifty.com/redpepper/round/10sen_suzu.htm

こちらは穴あき5銭硬貨↓。よくみると何種類かの異なる硬貨が混ざっている。小型五銭白銅貨、五銭アルミニウム青銅貨、穴あき五銭錫貨と呼ばれるもののよう。

　小型五銭白銅貨　http://homepage3.nifty.com/redpepper/round/kogata_5sen_hakudou.htm
　五銭アルミニウム青銅　http://homepage3.nifty.com/redpepper/round/5sen_arumiseidou.htm
　穴あき五銭錫貨　http://homepage3.nifty.com/redpepper/round/anaaki_5sen_suzu.htm

大量の黄色い50銭硬貨↓。小型五十銭黄銅貨と呼ばれるものらしく、やはり戦時中のもの。

少し大きめの10銭硬貨↓。大量。娘が菊のやつとか呼んで集めてた。

　菊十銭アルミニウム貨。http://homepage3.nifty.com/redpepper/round/kiku_10sen_arumi.htm

アルミニウムの5銭硬貨↓。割と簡素な感じ。

少し凝ったデザインの1銭↓。

カラス一銭アルミニウム貨 http://homepage3.nifty.com/redpepper/round/karasu_1sen_arumi.htm

稲がデザインされた10銭↓。娘が稲のやつとか呼んで集めてた。

稲十アルミニウム貨 http://homepage3.nifty.com/redpepper/round/ine_10sen_arumi.htm

先の黄色い50銭より少し大きめの50銭↓。50銭黄銅貨幣（鳳凰）。鳳凰が2体描かれたやつは別管理になっていた。たぶん多少価値が高いと思われる。

アルミニウム1銭↓。大量。

　富士一銭アルミニウム貨　http://homepage3.nifty.com/redpepper/round/fuji_1sen_arumi.htm

穴が空いていないアルミニウムの5銭↓。

鳩五銭錫貨 http://homepage3.nifty.com/redpepper/round/hato_5sen_suzu.htm

大きい1銭↓。桐一銭青銅貨と竜一銭銅貨。

桐一銭青銅貨 http://homepage3.nifty.com/redpepper/round/kiri_1sen_seidou.htm
　竜一銭銅貨　http://homepage3.nifty.com/redpepper/round/ryu_1sen_dou.htm
2銭のものもあった。

さて、残るは江戸時代以前の貨幣。お馴染みの寛永通宝から開元通宝、永楽通宝、常平通宝、治平元宝、淳熈元宝、洪化通宝、光中通宝、元豊通宝、皇宋元宝。開元通宝なんかは1000年以上前の渡来銭ではるか昔に思いを馳せざるを得ない。息子も戦国時代より古いと歓喜していた。
　←寛永通宝　　←常平通宝
　←永楽通宝　　←開元通宝
　←治平元宝　　←淳熈元宝
　←洪化通宝　　←光中通宝
　←元豊通宝　　←皇宋元宝

お札もあった。

OCamlの開発環境の作り方(2014年夏版)

OCaml 4.02.0が出ましたね。PCを新しくしたついでにemacs 24系でOCaml環境を作った時のメモを置いておきます。

$ apt-get install opam
$ opam init
$ opam update
$ opam switch 4.02.0
$ eval `opam config env`
$ opam install omake ocp-index ocp-indent
$ apt-get install auto-complete-el
$ cat .emacs.d/ocaml.el
(if window-system (require 'caml-font))
(setq auto-mode-alist
      (cons '("\\.ml[iylp]?$" . caml-mode) auto-mode-alist))
(autoload 'caml-mode "caml" "Major mode for editing Caml code." t)
(autoload 'run-caml "inf-caml" "Run an inferior Caml process." t)


(add-to-list 'load-path (file-truename "~/.opam/current/share/emacs/site-lisp"))
(setenv "PATH" (concat (getenv "PATH") ":~/.opam/current/bin"))
(setq exec-path (append exec-path '("~/.opam/current/bin")))

(require 'auto-complete)
(require 'ocp-index)
(require 'ocp-indent)

~/.opam/currentは~/.opam/4.02.0や~/.opam/4.01.0へのシンボリックリンクです。
flymake化もできますが、それは以前の記事(2012年12月19日のやつ)を参考に。

ATSのお勉強メモ

秘密結社Metasepiに関連してATSを勉強しているのでメモ。特にマニュアルには書いてないのではないかと思われる文法が散見されてつらぽよ。分からない時はぐぐって過去に作者がメーリングリストに回答している説明を探すべし。

  • バージョン
    • ATS2(ATS/Postiats) 0.04
  • コンパイルコマンド。ATS2からatsccじゃなくてpatscc.
  • メモリアロケーションが必要な場合は -DATS_MEMALLOC_LIBCオプションが必須。
  • メイン関数は次のように実装。mainではないので注意。

implement main0 () = {
val () = println! ("Hello World\n");
}

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

  • 数値の表現
  • 四則演算は+ - * /
    • doubleからintへの変換など、型変換の関数は沢山定義されている。
    • g0float2int, g0string2intとか。
  • 文字列はダブルクォートで囲む。val msg = "abc"
  • 文字列はメモリリソースなので動的に扱う場合単純なstring型だけでは済まない。
  • メモリアロケーションの事を考えなくていい場合は次の二つをロードする。

staload "libats/ML/SATS/string.sats"
staload _ = "libats/ML/DATS/string.dats"

  • リストプログラミングをMLっぽくやるなら次の二つをロードする。

staload "libats/ML/SATS/list0.sats"
staload _ = "libats/ML/DATS/list0.dats"

mbedではじめる関数型マイコンプログラミング講習会β

今日はmbedではじめる関数型マイコンプログラミング講習会β @名古屋 #0(http://partake.in/events/ab56454b-c305-4f3b-b8ce-872871ab7da9)に参加。@master_qさんに組込み技術とAjhcについて教えてもらい有意義だった。
しかし、@master_qさんの目標へ向けた活動のアクティブさには感心する。私も大きな目標を掲げて活動したい。

OCamlの開発環境の作り方 2012年暮れ版

この記事はLL/MLアドベントカレンダーの記事です。

一時期停滞していたOCamlの開発環境は最近進化してきています。2012年暮れ時点における知見をまとめてみましょう。なお、これらの進化はOCaml開発チームはもとより、OCamlPro, @camlspotter氏、@m2ym氏の多大な貢献によるものです。

OPAM

OPAMはGODI,OASISと同様OCaml専用のパッケージマネージャーです。従来システムに比べて使いやすさが格段にアップしています。現時点ではパッケージマネージャとしてOPAM一択で問題ないでしょう。

http://opam.ocamlpro.com/

ダウンロード&インストール：
$ wget http://opam.ocamlpro.com/build/opam64
$ chmod +x opam64
$ sudo cp opam64 /usr/local/bin/opam
$ opam init
$ echo 'eval `opam config -env`' >> ~/.bashrc
$ source ~/.bashrc

使い方：
$ opam switch -install 4.00.1 <- 4.00.1のインストール
$ ln -s ~/.opam/4.00.1 ~/.opam/current
$ opam list  <- 利用可能なパッケージの一覧
$ opam install lwt <- ライブラリのインストール(例えばlwt)

なお、opam switchで複数のバージョンのコンパイラを切り替えることもできます。しかし、その場合ocamlコマンドが入っているbinディレクトリへのパスが変わってしまいます。そこでopam switchは使わず、~/.opam内にcurrentというシンボリックリンクを作って対応すると良いと思います。

typerex

typerexはemacs用OCaml開発環境です。式の型表示、定義ジャンプ、補完などが可能で、emacsを使っている人は現時点ではこれを使うと良いと思います。Version 4.00系でのインストール方法と使い方は次の通り。

http://www.typerex.org/

ダウンロード：
$ https://github.com/OCamlPro/typerex.git
$ cd typerex
$ git checkout typerex2
コンパイル&インストール：
$ ./configure -prefix /usr/local
$ make
$ make install

.emacsの定義。

;; REPLのためにocamlコマンドへのパスを通しておく.
(add-to-list 'exec-path (expand-file-name "~/.opam/current/bin"))

;; typerex2の設定.
(with-temp-buffer (insert (shell-command-to-string "ocp-edit-mode emacs -load-global-config")) (eval-buffer))

:; flymakeのための設定(OMake限定)
(require 'flymake)
(push '("File \"\\(.*\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)--?\\([0-9]+\\):\\(.*\\)" 1 2 3 5) flymake-err-line-patterns)
(push '("\\.ml\\'" flymake-ocaml-init) flymake-allowed-file-name-masks)
(defun flymake-ocaml-init ()
  (list (expand-file-name "~/.emacs.d/ocaml-flymake.sh")))

ocaml-flymake.shの内容。omakeへのパスが通っていない場合にはenv PATH=${PATH}などでパスを通します。(teeでログ出力するのは@tomy_kairaさんの改良！)

$cat ~/,emacs.d/ocaml-flymake.sh
#!/bin/bash
omake -s 2>&1 | tee -a /tmp/ocaml_log | tr -d "\n" | sed -e 's/\t//g'

typerexの設定ファイルの一部である~/.ocp/ocp-edit-mode.confを書き換えておきます。これで標準ライブラリの補完が効くようになります。

mli_directories = [
  "/usr/lib/ocaml";
  "/home/osiire/.opam/current/lib/ocaml";  <- この行を加える. 絶対パスで.
]

emacs上での主な使い方は次の通り.

  • Cc-tでカーソル上の式の型を表示.
  • Cc-;でカーソル上の値の定義位置へジャンプ.
  • モジュール名ドットの後でタブキーを押すと補完.

その他整備

さて、typerexとOPAMで一通りの環境が揃いました。しかし、実際OCamlを使ったプロジェクトで開発を行うにはもう一工夫欲しいところです。そういったちょっとしたノウハウを集めたプロジェクトスケルトンを用意しました。プロジェクトを始めるときにcloneして.git消して使うと便利かと。

https://github.com/osiire/optemplate

たぶん参考になる点：

  • ライブラリをロードしたToplevelの起動方法
  • OMakeでの複数ディレクトリの取り扱い方
  • Cのソースを含むOCamlプログラムのビルド
  • pack付きでライブラリをビルドする方法

以上、OCamlの開発環境についてまとめてみました。Happy Hacking!