COSC6411

User Tools

Site Tools

You are here: F09-GS/CSE6411: Programming Logic for Complex Systems » Assignments » Assignment 1
Trace:
assignments:a1

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
assignments:a1 [2009/03/13 19:37] – jonathanassignments:a1 [2009/03/20 04:06] (current) – jonathan
Line 2: Line 2:
 Assignment 1 due date:before class on Wednesday March 18th. 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> <code>
Line 12: Line 12:
  
 int r = 1; /* semaphore */ int r = 1; /* semaphore */
-bit p1, p2;+bit p1, p2 = 0;
  
  
 active proctype P1() { active proctype P1() {
 do do
-:: p1 = 0;  +:: atomic{r > 0 -> r = 0}; /* request(r)*/
- atomic{r > 0 -> r = 0}; /* request(r)*/+
  p1 = 1; /* critical section */  p1 = 1; /* critical section */
  p1 = 0;  p1 = 0;
Line 27: Line 26:
 active proctype P2() { active proctype P2() {
 do do
-:: p2 = 0;  +:: atomic{r > 0 -> r = 0}; /* request(r)*/
- atomic{r > 0 -> r = 0}; /* request(r)*/+
  p2 = 1; /* critical section */  p2 = 1; /* critical section */
  p2 = 0;  p2 = 0;
Line 40: Line 38:
 Hint: In Event-B you have to think **events** rather than statements in a coding language. Hint: In Event-B you have to think **events** rather than statements in a coding language.
  
-Submit a Latex hardcopy of your work and a mutex.zip file via the +Submit a Latex hardcopy of your work and a mutex.zip file via electonic submit:
    submit -l 6411 a1 mutex.zip mutex.tex mutex.pdf    submit -l 6411 a1 mutex.zip mutex.tex mutex.pdf
  
 The zip file can be created from the Rodin export facility (see Rodin Tutorial). The zip file can be created from the Rodin export facility (see Rodin Tutorial).
assignments/a1.1236973025.txt.gz · Last modified: by jonathan