|
|
|
|
|
02158 Concurrent Programming Fall 2024 |
Mandatory Assignment 2: Verified Synchronization |
| Home | Plan | Material |
Read about semaphores and semaphore techniques in [Andrews 4-4.5].
You are assumed to have set up a working SPIN/JSpin environment and gained experience with the tool as described in CP Lab 2.
Part I picks up on your results from Lab 2.
Describe how you have achieved a fair solution for the mutual exclusion problem in section C of CP Lab 2.
Hand in a Promela file Lab2c.pml with your solution including an inline LTL formula expressing fairness for (an arbitrary, non-special one of) the processes. The model must satisfy both mutual exclusion as well as the fairness property.
Part II consists of a number of problems which, following a long tradition of Concurrent Programming, are cast in a made-up setting:
At a playground, 8 pedal-driven cars are available for the children to use. Each car must follow a given track circling around a hut on the ground. Some of the cars go one way round, some the other way. Unfortunately, the alley behind the hut has one lane only. Each car has to pass a special gate on the track, where it may be stopped if needed. A special 9-th car (Car no. 0) is available for the youngest children. It follows its own tiny track that does not intersect the other ones. Those toddlers really go incredibly fast! Everything usually goes fine although the cars bump into each other from time to time. When the cars meet front-to-front in the alley, the children sort it out their own way...
One day it is decided to upgrade the cars to electric ones. Since these are very expensive, a control system should ensure that they do not bump into each other anymore. And now the playground attendants also get ideas about new functionalities...
You have been engaged to implement this control system.
[All files mentioned below have been packed into man2.zip, see later.]
Your are given a Java-class Cars.java which provides a graphical user interface (GUI) illustrating the state of the playground and the cars. The GUI also allows for starting and stopping the cars (described later). You are not supposed to study its implementation.
You are also given a Java class CarControl.java that runs and controls the cars.
The means of interaction between the graphics and the control parts is given by three interfaces. The CarDisplayI.java provides methods for the control part to get various information and get access to objects which represent the actual cars. Through the interface CarI.java, the control part can make the car move along a desired route. The CarControlI.java defines the methods by which the GUI requests change of the control.
The playground is structured as a 11 rows times 12 columns matrix of tiles using (row,col)-indexing starting with (0,0) at the left-most tile of the the top row. To communicate such matrix positions, an auxiliary class Pos.java is used by the interfaces.
The cars move on the tiles following a rectangular grid. A car can autonomously drive along a grid line to a given position on the playground. For each car there is a dedicated conductor-thread which decides upon the whereabouts of the car using the method driveTo(pos) which makes the car move towards pos and then awaits that the car arrives at that destination (viz. when it is fully within the destination tile). Cars cannot move outside the playground, but otherwise they have no knowledge about obstacles or other cars.
The CarControl.java class uses two auxiliary classes: Field.java and Alley.java which are provided in rudimentary forms for you to elaboarate on. It also uses the classes Gate.java and SemGate.java which you are not supposed to change.
The program may be run by the command
which will create the GUI and make a single instance of your the CarControl class, passing it an implementation of CarDisplayI. The CarControlI-methods of the CarControl class will then be called when the various buttons are activated in the GUI. [The given GUI does not provide all possible interactions though.]
For testing purposes, a special test class may be provided as described later.
Even though you might feel tempted to improve upon the graphics, you are not supposed to make any changes to any classes in the Cars.java file.
[If the playground turns out too tiny, you may change the resolution of your screen.]
In this assignment, you are only allowed to make changes to the Field.java, CarTest.java and various *Alley.java files. All other given class and interface files must remain intact.
You should assume that you are in an environment where the only synchronization mechanism available is that of semaphores. For this, you must use the provided class Semaphore.java that implements a classical, weakly-fair Dijkstra semaphore.
All the files needed have been put together in the file man2.zip.You can unpack this and compile and run the system using:
Alternatively you can import the .zip-file into your favourite Java IDE, eg. Eclipse, IntelliJ IDEA or Visual Studio Code.
No particular package-scheme is applied for this application. Therefore all classes must be placed and compiled in the same directory.
For reasons of evaluation testing, no package structure should be applied.
Your solutions will be tested using JDK 17. If you compile with a higher version of Java, you should set the compliance level to 17.
Bumping may occur when two cars are (partly) covering the same tile. You can check whether bumping takes place by setting the mark called "Keep".
Device a solution which prevents bumping. The solution must be confined to the class Field.java which is called whenever a conductor thread is about to move the car to a new tile, and whenever the car has fully left a tile.
To solve this problem, you must carefully study the workings of the Conductor thread in the CarControl class - especially its run() method.
The problem must be solved using the given Semaphore class as the only means of synchronization. Auxiliary variables may be used if needed.
For this problem, you must hand in your modified Field.java class.
Once the cars no longer bump into each other, deadlocks start to occur in the alley.
Change the Alley.create() method in the given Alley.java class to use the MonoAlley implementation.
Run the program, and explain why deadlocks no longer occur in the alley.
The children, however, are not happy with this solution. They would like to follow each other in the alley when there are no cars in the opposite direction around.
A suggestion for such a more efficient solution is given by the class MultiAlley.java
Change the Alley.create() method to use the MultiAlley implementation and describe the behaviour you observe.
Although the solution may seem work well and the children are happy with it, you feel a bit suspicious and are therefore going to analyze it using SPIN.
Make a Promela model of the system which reflects the synchronization done by the cars at the entry and exit points of the alley. The model should not deal with details of the tile synchronization used to avoid bumping.
Declare one or more process types and instantiate these corresponding to the cars. Use macros/inlines to define the semaphore operations, P(S) and V(S), and mimic the structure of the system by defining enter and leave operations to be used by the cars. Be careful to faithfully represent the (non-)atomicity of the program statements - in particular the counter increments and decrements.
With this model, express an alley safety property which must be satisfied by the system in order to prevent cars from deadlocking in the alley.
The property should avoid using internal variables of the synchronization solution as these may not properly reflect what was intended. Instead you may add your own history variables if needed (cf. the incrit variable in Problem 1).
Explain the alley safety property.
Use SPIN to demonstrate that:
The first error is typically reported as invalid end stete. The second error typically by assertion violation. In the standard safety verification mode of Spin, it will check for both kinds of errors and stop at the first of these it finds. Therefore, in order to identify both kinds, you may try to add -A (no assertion check) or -E (no end state check) to the pan options.
You may also try to verify using breadth-first-search (BFS) instead of the default depth-first-search (DFS). See Lab 2 A.12 how to do this.
Analyze the output and error trails provided by SPIN and describe the essential causes of these errors.
You may find some tips for the SPIN verification on the Spin page.
For this problem, you should hand in a Promela file Man2multi.pml.
Race conditions may be very difficult to reproduce by testing. However, sometimes the scheduling can be guided by inserting various sleep periods in the code so that a particular race condition is likely to occur.
Show how to demonstrate the errors found in Problem 3 by inserting Thread.sleep(...) at various places in MultiAlley.java. The errors should show up within half a minute after the "Start All" button is pressed.
You should make one version MultiAlley1.java demonstrating that the synchronization deadlocks (leaving the cars wait forever outside the alley) [easy] and one version MultiAlley2.java demonstrating that cars may deadlock inside the alley [hard].
The sleeps could be in the order or 0.1-1.0 sec.
Describe your deliberations and hand in the two java files.
Device a new correct synchronization solution for the alley. The solution must be implemented by elaborating the class SafeAlley.java and selecting this in Alley.create()
You may try to mend the given MultiAlley.java solution, or try to invent another solution principle yourself.
[If you cannot find a solution, you may do Problem 5+ instead.]
The solution must be reflected by a Promela model Man2safe.pml which satisfies the alley safety property. You are recommended to start by solving the problem at the model level first.
Describe your solution.
The attendants' coffee room in the hut is situated towards the alley, so to let them have some calm coffee breaks, it has been made possible to apply speed reduction in the alley (by setting the mark called "Slowdown").
You should discuss to which extent the cars may experience starvation in your solution, both with and without the alley speed reduction. However, you are not supposed to make a fair solution (preventing starvation).
For this problem, you should hand in a Man2safe.pml model file and the corresponding SafeAlley.java file.
In this problem, the alley synchronization problem should be solved by applying the technique of passing-the-baton.
Make a (high-level) Promela model of a solution in which the enter and leave opertions are defined as larger atomic actions (cf. [Andrews] Fig 4.11). The actions should record relevant information, e.g. car counts. Some of the actions should be made conditional in such a way that the alley safety property can be verified.
This model must be handed in as Man2coarse.pml
Then systematically implement the atomic actions using passing-the-baton as described in [Andrews 4.4.3] resulting in corresponding Man2baton.pml and a BatonAlley.java files.
Finally you should verify that the solution satisfies the split binary semaphore principle [Andrews 4.2.3] by adding an appropriate property to your model.
For this problem, the Man2coarse.pml and Man2baton.pml model files as well as the final BatonAlley.java must be handed in.
Based on the Promela model for your solution from Problem 5 (or 5+), you should state liveness properties for the alley which corresponds to the obligingness and resolution properties for critical regions. Try to verify these properties. Do they hold as expected?
State a fairness property (for some car) and determine whether it holds for your solution.
Describe your properties and results.
For this problem, you must hand in a Promela file Man2live.pml where the properties are included as LTL formulas.
The assignment should be made in groups of 2-3 students. If you for some reason would prefer to do the assignment on your own, you must get prior permission from the teacher (HHL) (if you have not already done so).
The groups from Assignment 1 are assumed to continue. You may form new groups, but the teacher must be informed about any group changes no later than Thursday October 10.
All groups should do Problems 1, 2, and 3 as well as either Problem 5 or 5+.
Groups of 3 students must do one extra problem.
Doing Problem 5+ instead of 5 counts as one extra. Problems 4 and 6 each count as one extra.
Of course, each group must work on its own. In particular you must not exchange any form of code or texts with other groups.
You are not allowed to let others gain access to your solutions. Therefore the use of public repositories must be avoided.
Use of generative AI is not recommended, but if you do anyhow, it must be declared (for what and how).
The asssignment must be handed in on Inside no later than
The hand-in should comprise the following:
The report should include
Assistance for the assignment will be available on October 10, during the lab session as indicated on the course plan.
In case of amendments or updates, these will appear here. Major updates will be announced on Learn.
Enjoy!
| Hans Henrik Løvengreen, Oct 21, 2024 |