Differences

This shows you the differences between two versions of the page.

--- assignments:a1 [2009/03/13 19:41] – jonathan
+++ assignments:a1 [2009/03/20 04:06] (current) – jonathan
@@ Line 2: / Line 2: @@
 Assignment 1 due date:before class on Wednesday March 18th.
-The following is a Spin description of a mutual exclusion algorithm using a semaphore variable ''r''. You should be able to show (in JSpin) that the algorithm is safe (does not allow two processes in the critical area at the same time), and does not deadlock. However, it is not fair (i.e. there is no guarantee, under weak fairness, that processes will eventually get into the critical region).
+The following is a Spin description of a mutual exclusion algorithm using a semaphore variable ''r''. You should be able to show (in JSpin) that the algorithm is safe (does not allow two processes in the critical area at the same time), and does not deadlock. However, it is not fair (i.e. there is no guarantee, under weak fairness, that processes will eventually get into the critical region). If using JSpin, make sure there are no spaces in the file names.
 <code>
@@ Line 12: / Line 12: @@
 int r = 1; /* semaphore */
-bit p1, p2;
+bit p1, p2 = 0;
 active proctype P1() {
 do
-:: 	p1 = 0;
+:: 	atomic{r > 0 -> r = 0}; /* request(r)*/
-	atomic{r > 0 -> r = 0}; /* request(r)*/
 	p1 = 1; /* critical section */
 	p1 = 0;
@@ Line 27: / Line 26: @@
 active proctype P2() {
 do
-:: 	p2 = 0;
+:: 	atomic{r > 0 -> r = 0}; /* request(r)*/
-	atomic{r > 0 -> r = 0}; /* request(r)*/
 	p2 = 1; /* critical section */
 	p2 = 0;