SPL parsing, parameterized program example

In parameterized programs, an unbounded number of processes are composed with each other. The classic example is when N processes, rather than only 2, are competing to enter a critical section. The algorithm that arbitrates between these process can be expressed as a parameterized SPL program, as shown below.

in 	N : int
local 	flag : array [0..N-1] of int
		where Forall i : [0..N-1] . (flag[i] = 0)
local   turn : array [0..N-1] of [0..N-1]

|| P [i:[0..N-1]] ::
	[ local j : int
	  loop forever do
	     [  l0: j := 1;
		l1: while j < N do
		    [l2: flag[i] := j;
		     l3: turn[j] := i;
		     l4: await (turn[j] != i \/ 
				Forall k : [0..N-1] . 
				   (k != i --> flag[k] < j));
		     l5: j := j + 1
		    ];
	        l6: critical;
		l7: flag[i] := 0
	      ]
	]

---

step-comments@CS.Stanford.EDU