CIS 720 – Advanced Operating Systems Name: _______________________
Quiz #2
Spring 2021
Due: Friday, May 14 by 11:59 pm
Please show all work on the quiz.
(20 points) Consider the following UPPAAL timed automata, Brake and User. They communicate via global channels called tap and release. Brake has a local clock x, User has a local clock y and a location invariant of y<=6.
Templates: Brake User
// Global Declarations:
chan tap;
chan release;
// System Declarations
System Brake, User;
Determine which of the following properties are satisfied for the automata shown above; circle all properties that are satisfied, explain briefly why the properties that are not circled are not satisfied:
A[] (not deadlock)
Brake.Locked --> Brake.Off
Brake.Off –> Brake.Braking
Brake.Braking –> Brake.Locked
E<> (Brake.x==7)
A[] (Brake.Braking imply Brake.x <= 5)
A[] (Brake.Locked imply Brake.x <= 8)
A[] (User.y <= Brake.x)
As these automata have two local clocks, Brake.x and User.y, the reachable state space with respect to the clocks can be viewed as a point in a two-dimensional Cartesian plane, with the x-axis for clock Brake.x and the y-axis for clock User.y. A point (a, b), with non-negative a and b, can be used to denote that clock Brake.x equals a and clock User.y equals b. Determine the reachable state space for these automata; e.g., draw a 2-d graph above.
(20 points) Consider the UPPAAL automata p1 and p2 shown below. They share two global clocks x and y.
Determine which of the following properties are satisfied for the automata described above; circle all properties that are satisfied, explain briefly why the properties that are not circled are not satisfied:
A[] not deadlock
E<> (x==6)
E<> (y==6)
E<> (x==y+6)
A[] ((x-y)<=5)
A[] ((x-y)<=6)
Determine the reachable state space; e.g., draw a 2-d graph above.
(20 points) Consider the following proposed Spin solution (written in Promela) to the counting semaphore problem for the case when the semaphore count is initialized to N = 3; that is, at most three processes should be allowed to enter their critical sections at the same time:
#define N 3
byte cnt = 0;
active [10] proctype user()
{
atomic {cnt