add formal verif

[lttv.git] / trunk / verif / Spin / Test / peterson

diff --git a/trunk/verif/Spin/Test/peterson b/trunk/verif/Spin/Test/peterson
new file mode 100755 (executable)
index 0000000..156da7e
--- /dev/null
+++ b/trunk/verif/Spin/Test/peterson
@@ -0,0 +1,20 @@
+/* Peterson's solution to the mutual exclusion problem - 1981 */
+
+bool turn, flag[2];
+byte ncrit;
+
+active [2] proctype user()
+{
+       assert(_pid == 0 || _pid == 1);
+again:
+       flag[_pid] = 1;
+       turn = _pid;
+       (flag[1 - _pid] == 0 || turn == 1 - _pid);
+
+       ncrit++;
+       assert(ncrit == 1);     /* critical section */
+       ncrit--;
+
+       flag[_pid] = 0;
+       goto again
+}