Hello, if you have any need, please feel free to consult us, this is my wechat: wx91due
Assignment 2 CSSE7610
Due date and time: Thursday 17 October, 4pm
Before writing to the shared variables x1 and x2, the writer increments a counter c. It then proceeds to write to the variables, and finally increments c again. The two increments of c ensure that it is odd when the process is writing to the variables, and even otherwise. Hence, when a reader wishes to read the shared variables, it waits in a loop until c is even before reading them. Also, before returning it checks that the value of c has not changed (i.e., another write has not begun). If it has changed, the process starts over. This ensures the pair of values read corresponds to a single occurrence of a write.
|
Non-blocking reader-writer |
|
|
integer c, x1, x2 ← 0 |
|
|
reader |
writer |
|
integer c0, d1, d2 loop forever p1: repeat p2: repeat p3: c0 ← c p4: until (c0 mod 2 = 0) p5: d1 ← x1 p6: d2 ← x2 p7: until (c0 = c) p8: use(d1,d2) |
integer d1, d2 loop forever q1: d1 ← get() q2: d2 ← get() q3: c ← c+1 q4: x1 ← d1 q5: x2 ← d2q6: c ← c+1
q7:
q8:
|
(b) Extend the algorithm with a third type of process called an incrementer. An incrementer increments the values of x1 and x2, i.e., adds 1 to them. It is a low priority process and so should not block writers while reading x1 and x2, and synchronisation mechanisms should give preference to writers over incrementers.
Deliverable: A file named Q1 {student number} {first name} {last name}.pdf containing your name, student number, and your answers to (a) and (b). For example, if your student number is 12345678 and your name is Mark Zhang, then the file should be “Q1 12345678 Mark Zhang.pdf”.
(a) any pair of values used by a reader or incremented by an incrementer are either the initial values, or were written by a single occurrence of a write, and
(b) the values incremented by an incrementer are the current values of x1 and x2.
Note: if you get very long counter-examples from Spin, click on Advanced Parameter Settings (while in the Verification tab) and set the Maximum Search Depth to a smaller number. If it is too small no counter-example will be found, but you will be able to find a counter-example of around 20 or 30 steps in many cases.
Alternatively, just look at the last few steps (and states) of the counter example as these usually indicate the problem. Use Step Backward and Step Forward to move through these steps.
Deliverable: A file named Q2 {student number} {first name} {last name}.pml containing the Promela specification, a comment describing the property you proved, and your name and student number (as a comment). For example, if your student number is 12345678 and your name is Mark Zhang, then the file should be “Q2 12345678 Mark Zhang.pml”.
3. Implement your algorithm from Question 1(b) in Java. You should have 5 reader threads, 5 writer threads and 5 incrementer threads. Each writer and incrementer waits for a random time (between 0 and 10 milliseconds) then updates the shared variables (just once) and terminates. The writers can update the variables with random values. The readers wait a random time (between 0 and 10 milliseconds) before each read. When all readers have read the final update, the entire program should terminate gracefully, i.e., all threads should reach the end of their run methods. Your program should produce output by calling the appropriate methods of the provided class A2Event.java. For testing purposes, it is a requirement that you call the A2Event class every time one of the events occurs. In particular, the writers and incrementers must call the A2Event class before another writer or incrementer begins to update the results. It is also important that you do not modify the provided class.
Deliverables: A zip file named Q3 {student number} {first name} {last name}.zip containing a file ReadWrite.java with your main method for the program, along with all supporting source (.java) files (apart from A2Event), and a file readme.txt describing (in a few paragraphs) the ap proach you have taken to coding your program and providing a list of all your classes and their roles. All files should be well-documented and in particular the code for synchronisation should be well explained. All files should also contain your name and student number (as a comment).
For example, if your student number is 12345678 and your name is Mark Zhang, then the file should be “Q3 12345678 Mark Zhang.zip”.
package packageName;
Marking criteria
Students failing to explain their submission or attend this meeting will receive a grade of ZERO for this assignment.
• Counter-example for original algorithm (2 marks)• Justification of synchronisation constructs (2 marks)• Modification of algorithm (6 marks)
• Promela specification of algorithm (3 marks)• Properties for correctness (2 marks)
• Java classes implementing your design (4 marks)• Appropriate use of synchronisation mechanisms (3 marks)• Program producing correct behaviour (2 marks)• readme file (1 mark)