CS计算机代考程序代写 CIS 720 – Advanced Operating Systems Name: _______________________

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