--並行プログラムのLMNtalでの実装--

-LMNtalの概要-

LMNtalは階層的グラフ書き換えに基づくモデリング言語である。 LMNtalは、アトム、リンク、膜、ルールで構成されています。 また、LMNtalは、状態空間探索とLTLモデル検査器を備えている。

-並行プログラムのLMNtalでの実装-

ここにある並行プログラムの例題は並行プログラム内でデータ競合を起こさないためにLockをかける、 相互排他制御についての例題を示し、そのプログラムをLMNtalで実装する。
また、この例題プログラムはThe Art of Multiprocessor Programming を参考文献としている。

-LockOneアルゴリズム-

    class LockOne implements Lock {
        private boolean[] flag = new boolean[2];
        public void lock() {
            int i = ThreadID.get();
            int j = 1 - i;
            flag[i] = true;
            while (flag[j]) {}
        }
        public void unlock() {
            int i = ThreadID.get();
            flag[i] = false;
        }
    }
                

このプログラムはスレッド数が2のときのLockをかけるアルゴリズムである。 このプログラムはSafety propertyを満たすが、Liveness propertyを満たさない。 よって、このプログラムはDeadlockすることになる。 Deadlockしないためには、一方のスレッドがlock()を行う際にwaitをしてから、 もう一方のスレッドがlock()に入り実行されることが条件である。 以下にLockOneアルゴリズムのLMNtalでの実装を示す。

/* LockOne */

flag(0, 0), flag(1, 0), lock(0), lock(1).


/* lock */

i@@ flag(N, X), lock(M) :- N=:=M | 
		i(N), flag(N, X), defJ(N).
	
j@@ i(N), defJ(M) :- N=:=M, N1=1-N | 
		j(N1), i(N), true(N).
	
true@@ i(N), flag(M, X), true(N1):- N=:=M, N=:=N1, int(X) | 
		flag(N, 1), wait(M).
	
wait1@@ j(N), flag(M, X), wait(N1) :- N=:=M, N1=:=(1-N), X=:=1 | 
		j(N), flag(M, X), wait(N1).
wait2@@ j(N), flag(M, X), wait(N1) :- N=:=M, N1=:=(1-N), X=:=0 | 
		flag(M, X), lock(N1).


/* unlock */
i_u@@ flag(N, X), lock(M) :- N=:=M| 
		i_u(N), flag(N, X), false(N).

false@@ i_u(N), flag(M, X), false(N1):- N=:=M, N=:=N1, int(M), int(X) | 
		flag(N, 0), lock(M).

LMNtalでの実装方法としては、まずflagの配列を2引数のアトムで表現している。 1引数目に配列のindexを、2引数目に値を入れている。 また次のプログラムへの遷移はトークンを生成し行っている。 このプログラムはスレッド数が2であるため、各スレッドとしてlock(0), lock(1)と表現している。

-LockTwoアルゴリズム-

    class LockTwo implements Lock {
        private int victim;
        public void lock() {
            int i = ThreadID.get();
            victim = i;
            while (victim == i) {}
        }
        public void unlock() {}
    }
                    

このプログラムもスレッド数が2のときのLockをかけるアルゴリズムである。 このプログラムもSafety propertyを満たすが、Liveness propertyを満たさない。 よって、このプログラムはDeadlockすることになる。 lock()の実行が並行に起きるようにすればdeadlockは発生しない。 以下にLockTwoアルゴリズムのLMNtalでの実装を示す。

/* LockTwo */

victim(0), lock(0), lock(1).


/* lock */
i@@ lock(N) :- int(N) | 
		i(N), vic(N).
		
vic@@ i(N), victim(X), vic(N1) :- N=:=N1, int(X) | 
		victim(N), i(N), wait(N).
		
wait1@@ i(N), victim(X), wait(M) :- N=:=M, N=:=X |
		i(N), victim(X), wait(M).
wait2@@ i(N), victim(X), wait(M) :- N=:=M, N=\=X |
		victim(X), lock(N).		
		
		
/* unlock */

このプログラムも2スレッドのためlock(0), lock(1)を用いてスレッドを実装する。 また、変数victimもアトムとその引数で値を表現する。

-PetersonLockアルゴリズム-

    class Peterson implements Lock {
        private boolean[] flag = new boolean[2];
        private int victim;
        public void lock() {
            int i = ThreadID.get();
            int j = 1 - i;
            flag[i] = true;
            victim = i;
            while (flag[j] && victim == i) {};
        }
        public void unlock() {
            int i = ThreadID.get();
            flag[i] = false;
        }
    }
                

このプログラムもスレッド数が2のときのLockをかけるアルゴリズムである。 このプログラムはLockOneアルゴリズムとLockTwoアルゴリズムを組み合わせたプログラム。 PetersonLockはSafety property、Liveness propertyを満たす。 以下にPetersonLockアルゴリズムのLMNtalでの実装を示す。

/* PetersonLock */

flag(0, 0), flag(1, 0), victim(0),
lock(0), lock(1).


/* lock */

i@@ flag(N, X), lock(M) :- N=:=M, int(N) | 
		i(N), flag(N, X), defJ(N).
	
j@@ i(N), defJ(M) :- N=:=M, N1=1-N, int(N) | 
		j(N1), i(N), true(N).
	
true@@ i(N), flag(M, X), true(N1):- N=:=M, N=:=N1, int(X) | 
		flag(N, 1), i(N), vic(M).
		
vic@@ i(N), victim(X), vic(N1) :- N=:=N1, int(X) | 
		victim(N), i(N), wait(N).
	
wait1@@ i(S), j(N), flag(M, X), victim(Y), wait(N1) :- N=:=M, N1=:=S, X=:=1,  Y=:=S | 
		i(S), j(N), flag(M, X), victim(Y), wait(N1).
wait2@@ i(S), j(N), flag(M, X), victim(Y), wait(N1) :- N=:=M, N1=:=S, X=:=0, int(Y) | 
		flag(M, X), victim(Y), lock(N1).
wait3@@ i(S), j(N), flag(M, X), victim(Y), wait(N1) :- N=:=M, N1=:=S, Y=\=S, int(X) | 
		flag(M, X), victim(Y), lock(N1).


/* unlock */
i_u@@ flag(N, X), lock(M) :- N=:=M, int(N) | 
		i_u(N), flag(N, X), false(N).

false@@ i_u(N), flag(M, X), false(N1):- N=:=M, N=:=N1, int(M), int(X) | 
		flag(N, 0), lock(M).

このプログラムはLockOneアルゴリズムとLockTwoアルゴリズムを合わせたものであるため、 LMNtalでのプログラムも同様に実装を行った。

-FilterLockアルゴリズム-

    class Filter implements Lock {
        int[] level;
        int[] victim;
        public Filter(int n) {
            level = new int[n];
            victim = new int[n];
            for (int i=0; i<n; i++)
                level[i] = 0;
            }
        public void lock() {
            int me = ThreadID.get();
            for (int i=1; i<n; i++) {
                level[me] = i;
                victim[i] = me;
                while (( k != me) (level[k] >= i && victim[i] == me)) {};
            }
        }
        public void unlock() {
            int me = ThreadID.get();
            level[me] = 0;
        }
    }

このプログラムはPetersonLockアルゴリズムをnスレッドに拡張したアルゴリズムである。 FilterLockアルゴリズムもSafety property、Liveness propertyを満たす。 以下にFilterLockアルゴリズムのLMNtalでの実装を示す。

/* FilterLock */
t(3), filter.


/* Filter */

t(N), filter :- int(N) | t(N), n(N), lv.
n(N), lv :- N1=N-1, N > 0 | n(N1), level(N1, 0), lv.
n(N), lv :- N=:=0 | v.
	
t(N), v :- int(N) | t(N), n(N), vic.
n(N), vic :- N1=N-1, N > 0 | n(N1), victim(N1, -1), vic.
n(N), vic :- N=:=0 | defs.

t(N), defs :- int(N) | t(N), n(N), def.
n(N), def :- N1=N-1, N > 0 | n(N1), thread(N1,0), def.
n(N), def :- N=:=0 | start.


/* lock */
thread(N,0), start :- int(N) | me(N,N), start, thread(N,1).

thread(N,1), me(M,X) :- N=:=M | me(N,X), i(N,1), thread(N,2).
thread(N,2), i(X,Y), t(M) :- N=:=X, Y<M | i(X,Y), t(M), thread(N,3).
thread(N,2), i(X,Y), me(S,T), t(M) :- N=:=X, N=:=S, Y>=M, int(T) |
	t(M), cs(0), thread(N,10).

	thread(N,3), me(M,Z), i(S,T), level(X,Y) :- N=:=M, N=:=S, Z=:=X, int(Y), int(T) | 
		me(M,Z), i(S,T), level(X,T), thread(N,4).
	
	thread(N,4), me(M,Z), i(S,T), victim(X,Y) :- N=:=M, N=:=S, T=:=X, int(Y), int(Z) | 
		me(M,Z), i(S,T), victim(X,Z), thread(N,5).

	thread(N,5), me(M,Z), i(S,T), level(K,Y), victim(A,B):- N=:=M, N=:=S, T=:=A, K=\=Z, Y>=T, Z=:=B | 
		me(M,Z), i(S,T), level(K,Y), victim(A,B), thread(N,5).
	thread(N,5), me(M,Z), i(S,T), level(K,Y), victim(A,B):- N=:=M, N=:=S, T=:=A, K=\=Z, Y<T | 
		me(M,Z), i(S,T), level(K,Y), victim(A,B), thread(N,6).		
	thread(N,5), me(M,Z), i(S,T), level(K,Y), victim(A,B):- N=:=M, N=:=S, T=:=A, K=\=Z, Z=\=B | 
		me(M,Z), i(S,T), level(K,Y), victim(A,B), thread(N,6).

thread(N,6), i(X,Y) :- N=:=X, Y1=Y+1 | i(X,Y1), thread(N,2).


/* unlock */
thread(N,10), cs(0) :- int(N) | me(N,N), thread(N,11).

thread(N,11), level(X,Y), me(S,T) :- N=:=S, X=:=T, int(Y) | level(X, 0), thread(N,12).

このFilterLockアルゴリズムはnスレッドでのプログラムであるため、スレッドの実装をアトムthreadで実装している。 アトムの1つ目の引数はスレッド番号を表すようにした。 2つ目の引数は今までのトークンと同じ役割である、次のプログラムへの遷移を示すようにすることで、スレッドの実装を行った。 level, victim配列の実装は今までと同様に1引数目に配列のindexを、2引数目に値を入れている。

-BakeryLockアルゴリズム-

    class Bakery implements Lock {
        boolean [] flag;
        Label[] label;
        public Bakery (int n) {
            flag = new boolean[n];
            label = new Label[n];
            for (int i=0; i<n; i++) {
                flag[i] = false;
                label[i] = 0;
            }
        }
        public void lock() {
            int i = ThreadID.get();
            flag[i] = true;
            label[i] = max(label[0], ..., label[n-1]) + 1;
            while(( k != i) (flag[k] && (label[k], k) << (label[i], i))) {};
        }
        public void unlock() {
            flag[ThreadID.get()] = false;
        }
    }

このプログラムもnスレッドでLockをかけるアルゴリズムである。 BakeryLockアルゴリズムもSafety property、Liveness propertyを満たす。 また、このアルゴリズムはLock()に入った順番がCriticalSectionに入る順番になるといった性質がある。 一方、このプログラムを実装する際は、整理券番号画像化し続けるといった問題を考慮する必要がある。 以下にBakeryLockアルゴリズムのLMNtalでの実装を示す。

/* Bakery */
t(3), bakery.


/* Bakery */

t(N), bakery :- int(N) | t(N), n(N), f.
n(N), f :- N1=N-1, N > 0 | n(N1), flag(N1, 0), f.
n(N), f :- N=:=0 | l.
	
t(N), l :- int(N) | t(N), n(N), la.
n(N), la :- N1=N-1, N > 0 | n(N1), label(N1, 0), la.
n(N), la :- N=:=0 | defs.

t(N), defs :- int(N) | t(N), n(N), def.
n(N), def :- N1=N-1, N > 0 | n(N1), thread(N1,0), def.
n(N), def :- N=:=0 | start.


/* lock */
thread(N,0), flag(X,Y), start :- N=:=X, int(Y) | flag(N,1), start, thread(N,1), max(N,0), i(N,0).

thread(N,1), max(A,B), i(C,D), label(X,Y), t(M) :- N=:=A, N=:=C, D=:=X, D<M, B=<Y, Y1=Y+1, D1=D+1 | 
	max(A,Y1), i(C,D1), label(X,Y), t(M), thread(N,1).
thread(N,1), max(A,B), i(C,D), label(X,Y), t(M) :- N=:=A, N=:=C, D=:=X, D<M, B>Y, D1=D+1 | 
	max(A,B), i(C,D1), label(X,Y), t(M), thread(N,1).
thread(N,1), max(A,B), i(C,D), label(X,Y), t(M) :- N=:=A, N=:=C, N=:=X, D>=M, int(Y)| 
	label(X,B), t(M), thread(N,2), k(N,0), while(N,1).

thread(N,2), while(A,B), k(C,D), t(M) :- 
	N=:=A, N=:=C, D<M, N=:=D, D1=D+1| 
		while(A,B), k(C,D1), t(M), thread(N,2).
thread(N,2), while(A,B), k(C,D), label(X,Y), label(S,T), flag(E,F), t(M) :- 
	N=:=A, N=:=C, D=:=X, N=:=S, D=:=E, D<M, F=:=1, Y<T, int(B)| 
		while(A,1), k(C,0), label(X,Y), label(S,T), flag(E,F), t(M), thread(N,2).
thread(N,2), while(A,B), k(C,D), label(X,Y), label(S,T), flag(E,F), t(M) :- 
	N=:=A, N=:=C, D=:=X, N=:=S, D=:=E, D<M, F=:=1, Y=:=T, D<N, int(B)| 
		while(A,1), k(C,0), label(X,Y), label(S,T), flag(E,F), t(M), thread(N,2).
thread(N,2), while(A,B), k(C,D), label(X,Y), label(S,T), flag(E,F), t(M) :- 
	N=:=A, N=:=C, D=:=X, N=:=S, D=:=E, D<M, D1=D+1, F=:=1, Y=:=T, D>N, int(B)| 
		while(A,0), k(C,D1), label(X,Y), label(S,T), flag(E,F), t(M), thread(N,2).
thread(N,2), while(A,B), k(C,D), label(X,Y), label(S,T), flag(E,F), t(M) :- 
	N=:=A, N=:=C, D=:=X, N=:=S, D=:=E, D<M, D1=D+1, F=:=1, Y>T, int(B)| 
		while(A,0), k(C,D1), label(X,Y), label(S,T), flag(E,F), t(M), thread(N,2).
thread(N,2), while(A,B), k(C,D), label(X,Y), label(S,T), flag(E,F), t(M) :- 
	N=:=A, N=:=C, D=:=X, N=:=S, D=:=E, D<M, D1=D+1, F=:=0, int(B)| 
		while(A,0), k(C,D1), label(X,Y), label(S,T), flag(E,F), t(M), thread(N,2).	
		
thread(N,2), while(A,B), k(C,D), t(M) :- 
	N=:=A, N=:=C, D>=M, B=:=0, int(B)| 
		t(M), cs(0), thread(N,10).	

/* unlock */
thread(N,10), cs(0), flag(X,Y) :- N=:=X, int(Y) | flag(X,0), thread(N,11).

このLMNtalプログラムもFilterLockアルゴリズムの場合と同様に実装を行っている。

戻る