Alloy model of lock-free stack

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

what is lock-free

• 冬のLock free祭り safe from Kumazaki Hiroki
  www.slideshare.net

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
}

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

当然のことながらスタックは壊れる。. スクリーンショットの下の方にある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]
}

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

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